8

I am trying to solve some exercise from LiquidHaskell tutorial. So, I wrote this:

data List a = Nil | Cons a (List a) deriving (Show)                                                                                  
infixr 5 `Cons`

{-@ len :: List a -> Nat @-}
len :: List a -> Int
len Nil           = 0
len (x `Cons` xs) = 1 + len xs

{-@ mymap :: (a -> b) -> xs : List a -> { ys : List b | len xs == len ys } @-}
mymap :: (a -> b) -> List a -> List b
mymap _ Nil           = Nil
mymap f (x `Cons` xs) = f x `Cons` mymap f xs

But I'm getting an error (excuse, pls, this formatting, it's the original LH error format):

53 | mymap f (x `Cons` xs) = f x `Cons` mymap f xs                                                                                  
                              ^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : (Main.List a) | Main.Cons##lqdc##$select v == ?a
                               && Main.Cons##lqdc##$select v == ds_d35c x
                               && v == Main.Cons (ds_d35c x) ?a}

   not a subtype of Required type
     VV : {VV : (Main.List a) | len ?b == len VV}

   In Context
     xs : (Main.List a)

     ?b : (Main.List a)

     x : a

     ?a : {?a : (Main.List a) | len xs == len ?a}

What is the right "contract" of mymap? How to fix this error? And how should be read/treated messages like Main.Cons##lqdc##$select v == ds_d35c x?

RandomB
  • 3,367
  • 19
  • 30

1 Answers1

6

I had to explicitly annotate the constructors. After that, it compiles with LiquidHaskell.

data List a = Nil | Cons a (List a) deriving (Show)                                                                                  
infixr 5 `Cons`

{-@ len :: List a -> Nat @-}
len :: List a -> Int
len Nil           = 0
len (x `Cons` xs) = 1 + len xs

{-@ Nil   ::  { ys : List a | len ys == 0 } @-}
{-@ Cons  ::  a -> xs : List a -> { ys : List a | len ys == 1 + len xs } @-}

{-@ mymap :: (a -> b) -> xs : List a -> { ys : List b | len xs == len ys } / [ len xs ] @-}
mymap :: (a -> b) -> List a -> List b
mymap _ Nil           = Nil
mymap f (x `Cons` xs) = f x `Cons` mymap f xs
chi
  • 111,837
  • 3
  • 133
  • 218
  • 2
    I added contracts for `Nil` and `Cons` from your answer and it works now. But without this tail: ` / [ len xs ]`. What does it mean? Is it mandatory? – RandomB May 27 '19 at 13:34
  • 1
    @Paul-AG That tail suggests the induction metric for that goal. "Prove this type is correct by induction on the length of `xs`". Perhaps it is not needed, after all. – chi May 27 '19 at 17:47
  • Simple measures can often be inferred correctly. You likely would need an explicit measure for non-trivial structures. – Thomas M. DuBuisson Jun 18 '19 at 21:31