Что такое мера? - PullRequest
Новая
       24

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

10 голосов
/ 30 мая 2019

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

Меры - чтобы позволить функциям 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).

1 Ответ

7 голосов
/ 30 мая 2019

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

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

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

...