haskell - 简单的 Liquidhaskell 示例未能达到预期的行为

Question

我最近开始使用 Liquid 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 指定的前提条件，该函数是完整的。

我在这里做错了什么？我本质上只是希望能够对来自 Just 构造函数的 Maybe a 类型的子类型进行推理，但我无法在任何地方找到任何示例正确执行此操作。

Answer 1

抱歉回复晚了!我应该找到一些方法来获得有关问题的通知。好吧，有两件事发生，我们都应该解决!

首先，发生了一些小问题

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

重新定义也许。 这应该不需要，会尽快解决

这样，您的代码就可以按原样工作，例如看这里

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

感谢您指出这一点，将会修复!