3

我最近开始玩 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 指定了先决条件。

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

4

1 回答 1

0

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

首先，发生了一些小故障

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

感谢您指出这一点，将解决！

于 2019-11-14T01:09:59.630 回答