What is a measure?

I am reading this where I find this:

Measures -- In order to allow Haskell functions to appear in refinement types, we need to lift them to the refinement type level.

And there are other documents asserting that measures are needed to use such function in contract. But I tried this:

{-@ 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

and this works but len is not measure. So what is measure exactly and when I need it?

Another example which does not work without measure:

{-@ measure ln @-}
ln :: [a] -> Int
ln [] = 0
ln (x:y) = 1 + ln y

{-@ conc :: xs : [a] -> ys : [a] -> {zs : [a] | ln zs == ln xs + ln ys} @-}
conc :: [a] -> [a] -> [a]
conc [] ys = ys
conc (x:xs) ys = x : (conc xs ys)

Usage of {-@ measure length @-} like I found in many documents leads to error Cannot extract measure from haskell function (ie. from length).

A measure is just a function that can be run by LiquidHaskell at verification time, to be used in refinements and termination checking. You likely already knew this.

The reason your first example "works" (I think it's incomplete as-is, but I can tell what you were going for) is that len is already defined as a measure in the LiquidHaskell prelude (technically it's a "class measure", which means it's polymorphic, and thus can be used both with [] lists and your custom List). Assuming you've added annotations for Nil and Cons as in this answer from your earlier question, the len used in the refinement for mymap is not your len, but the prelude len, which is already a measure.

In your second example, measure is required because ln is a new symbol in the measure namespace, and doesn't exist unless you make it.

Recommended topics

Hot tags