Простой пример liquidhaskell не соответствует ожидаемому поведению - PullRequest
Новая
       29

Простой пример liquidhaskell не соответствует ожидаемому поведению

3 голосов
/ 07 октября 2019

Я недавно начал играть с жидким haskell, и из всех уроков, которые я смог найти, я не смог найти никаких примеров, подобных следующему. 

data MaybePerson = MaybePerson {                                                                        
  name' :: Maybe String,                                                                                
  age'  :: Maybe Int                                                                                    
}                                                                                                       

data Person = Person {                                                                                  
  name :: String,                                                                                       
  age  :: Int                                                                                           
}                                                                                                       

{-@ measure p :: MaybePerson -> Bool @-}                                                                
p (MaybePerson (Just _) (Just _)) = True                                                                
p _ = False                                                                                             

{-@ type JustPerson = {x:MaybePerson | p x} @-}                                                 

-- Attempts to instantiate a maybe person into a concrete Person                                    
{-@ getPerson :: JustPerson -> Person @-}                                               
getPerson (MaybePerson (Just name) (Just age)) = Person name age                             
getPerson _ = undefined

Если я попробую следующее, мой модуль не выполнит проверку типа, как ожидалось: 

test = getPerson (MaybePerson Nothing Nothing)

Однако по какой-то причине следующее все равно не проверяет тип: 

test2 = getPerson (MaybePerson (Just "bob") (Just 25))

и я получаю ошибку 

Error: Liquid Type Mismatch

 36 | test2 = getPerson (MaybePerson (Just "bob") (Just 25))
                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : MaybePerson | v == ?a}

   not a subtype of Required type
     VV : {VV : MaybePerson | Blank.p VV}

   In Context
     ?a : MaybePerson

Более того, если я опускаю строку getPerson _ = undefined, я получаю 

Your function is not total: not all patterns are defined.

Даже если эта функция явноявляется полным из-за предусловия, указанного в liquidhaskell.

Что я здесь не так делаю? По сути, я просто хочу иметь возможность рассуждать с подтипами типа Maybe a, которые приходят из конструктора Just, но я нигде не смог найти примеров того, где это сделать правильно.

1 Ответ

0 голосов
/ 14 ноября 2019

извините за поздний ответ! Я должен найти способ получить уведомление о вопросах. Хорошо, происходит две вещи, обе из которых мы должны исправить!

Во-первых, происходит что-то сбойное с 

{-@ measure p :: MaybePerson -> Bool @-}

Правильный синтаксис просто 

{-@ measure p @-}
p :: MaybePerson -> Bool

Но сообщения об ошибке не было, поэтому у вас нет возможности узнать!

Во-вторых, когда я изменяю вышеприведенное, я все еще получаю странную ошибку о GHC.Maybe - я не могу вспомнитьТочная проблема прямо сейчас, будет исправлена ​​на моем ноутбуке, но для иллюстрации я подправил ваш код: 

{-@ LIQUID "--exact-data-cons" @-}

import Prelude hiding (Maybe (..))

data Maybe a = Just a | Nothing

Чтобы переопределить Maybe. Это не нужно, мы найдем исправление КАК МОЖНО СКОРЕЕ

При этом ваш код работает как есть, например, см. Здесь

http://goto.ucsd.edu/liquid/index.html#?demo=permalink%2F1573693313_399.hs

Теперь вы можете определить 

{-@ getPerson :: JustPerson -> Person @-}                                               
getPerson (MaybePerson (Just name) (Just age)) = Person name age

и просто удалить уравнение для других случаев. Кроме того, 

test1 = getPerson (MaybePerson Nothing Nothing)         -- error

приводит к ошибке типа, но приведенное ниже безопасно 

test2 = getPerson (MaybePerson (Just "bob") (Just 25))  -- ok

Спасибо за указание на это, исправим!

...