Haskell中Measure的定义、适用场景及相关代码疑问

Great question! Let's break this down step by step—since the line between when you need a measure and when you don't can feel confusing at first with Liquid Haskell.

Why Your First Example Works Without a measure #

Your len function is a user-defined, structurally recursive, pure function operating on your custom List ADT. Liquid Haskell is smart enough to automatically infer that this function has the properties needed to be used in refinement types: it’s total (defined for all List values), has no side effects, and its behavior directly maps to the structure of the List type.

Even without the {-@ measure @-} annotation, Liquid can inductively reason about how len works with Nil and Cons to verify the refinement in mymap (that input and output lists have the same length). For simple, user-defined ADTs and their companion recursive functions, Liquid often doesn’t need explicit measure hints.

What Exactly Is a measure? #

A measure is an explicit annotation that tells Liquid Haskell:

"This function is a pure, well-behaved metric that I want you to treat as a first-class citizen in the refinement type system."

Measures have strict requirements to be valid:

• They must be total (defined for every possible input of their argument type)
• They must use structural recursion (only recurse on direct sub-components of the input data structure)
• They can’t have side effects, non-determinism, or depend on external state
• They return a basic type like Int, Bool, or Nat

When you mark a function as a measure, Liquid doesn’t just treat it as a regular Haskell function—it pre-computes and tracks its logical properties (like how it interacts with data constructors) to make refinement checks faster and more reliable, especially for complex contracts.

When Do You Need to Use measure? #

Your second example highlights one key scenario: working with built-in Haskell data types (like the standard [] list). Liquid doesn’t automatically infer measures for custom functions operating on built-in types the same way it does for user-defined ADTs. For the standard list type [], you need to explicitly mark your length function (ln) as a measure so Liquid can track how it interacts with [] and (:) constructors—this is critical to verifying the conc contract (that the concatenated list’s length equals the sum of the input lengths).

Other cases where measure is required:

• If your metric function has complex logic that Liquid can’t automatically infer is pure/structural (e.g., a function counting specific elements in a list)
• When reusing the metric across multiple refinement contracts and needing consistent enforcement of its properties
• When using the function as a boolean predicate in refinements (e.g., { xs : [a] | ln xs > 0 })

Why Can’t You Use {-@ measure length @-}? #

The error Cannot extract measure from haskell function (ie. from length) happens because the standard library’s length isn’t implemented in a way Liquid can recognize as a valid measure. The standard length may include optimizations (like strictness annotations or internal helper functions) that break the structural recursion requirement Liquid needs to extract a measure.

To use a length metric for standard lists, you have two solid options:

1. Define your own explicit measure function like your ln (exactly what you did in the second example)
2. Use Liquid’s built-in measures for standard types—Liquid provides a pre-defined len measure for lists that you can use directly!

Recap of Your Examples #

Example 1: No measure Needed (Custom ADT) #

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

This works because len is a simple structural recursive function on your custom List ADT—Liquid infers its properties automatically.

Example 2: measure Required (Built-in List) #

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

Here, ln operates on the built-in [] type, so we need to explicitly mark it as a measure for Liquid to verify the concatenation length contract.

内容的提问来源于stack exchange，提问作者RandomB