Что такое мера?

Question

Я читаю это, где я нахожу это:

Меры - чтобы позволить функциям Haskell появляться в типах уточнения, нам необходимо поднять их до уровня типа уточнения.

И есть другие документы, утверждающие, что необходимы меры для использования такой функции в контракте. Но я попробовал это:

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

и это работает, но len это не мера. Так что же такое мера и когда она мне нужна?

---

Еще один пример, который не работает без 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)

Использование {-@ measure length @-} как я нашел во многих документах, приводит к ошибке Cannot extract measure from haskell function (т.е. из length).

Answer 1

Мера - это просто функция, которая может быть запущена LiquidHaskell во время проверки для использования при уточнениях и проверке завершения. Вы, вероятно, уже знали это.

Причина, по которой ваш первый пример "работает" (я думаю, что он неполон как есть, но я могу сказать, для чего вы шли) состоит в том, что len уже определено как мера в прелюдии LiquidHaskell (технически это "мера класса", что означает, что она полиморфна, и, следовательно, может использоваться как с [] списки и ваш обычай List). Предполагая, что вы добавили аннотации для Nil а также Cons как и в этом ответе на ваш предыдущий вопрос, len используется в уточнении для mymap не твой lenно прелюдия len, который уже является мерой.

Во втором примере measure требуется, потому что ln является новым символом в пространстве имен меры и не существует, пока вы его не сделаете.