我最近开始使用 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
类型的子类型进行推理,但我无法在任何地方找到任何示例正确执行此操作。
最佳答案
抱歉回复晚了!我应该找到一些方法来获得有关问题的通知。好吧,有两件事发生,我们都应该解决!
首先,发生了一些小问题
{-@ 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
感谢您指出这一点,将会修复!
关于haskell - 简单的 Liquidhaskell 示例未能达到预期的行为,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/58275592/