Liquid Haskell:证明组合器和谓词精炼类型的错误
Liquid Haskell: Error with Proof Combinators and Types Refined by Predicates
作为我遇到的问题的一个最小示例,这里有一个自然数的定义、一个加倍函数和一个由均匀性谓词细化的类型:
data Nat' = Z | S Nat' deriving Show
{-@ reflect double' @-}
double' :: Nat' -> Nat'
double' Z = Z
double' (S x) = (S (S (double' x)))
{-@ type Even' = {v:Nat' | even' v} @-}
{-@ reflect even' @-}
even' :: Nat' -> Bool
even' Z = True
even' (S Z) = False
even' (S (S x)) = even' x
我想先声明 {-@ double' :: Nat' -> Even' @-}
然后证明这是真的,但我的印象是我必须先写证明然后使用 castWithTheorem
(这本身对我有用)这样:
{-@ even_double :: x:Nat' -> {even' (double' x)} @-}
even_double Z = even' (double' Z)
==. even' Z
==. True
*** QED
even_double (S x) = even' (double' (S x))
==. even' (S (S (double' x)))
==. even' (double' x)
? even_double x
==. True
*** QED
{-@ double :: Nat' -> Even' @-}
double x = castWithTheorem (even_double x) (double' x)
但是,这会产生相当难以辨认的错误,例如:
:1:1-1:1: Error
elaborate solver elabBE 177 "lq_anf$##7205759403792806976##d3tK" {lq_tmp$x##1556 : (GHC.Types.6$6$ (GHC.Prim.TYPE GHC.Types.LiftedRep) (GHC.Prim.TYPE GHC.Types.LiftedRep) bool bool) | [(lq_tmp$x##1556 = GHC.Types.Eq#)]} failed on:
lq_tmp$x##1556 == GHC.Types.Eq#
with error
Cannot unify (GHC.Types.6$6$ (GHC.Prim.TYPE GHC.Types.LiftedRep) (GHC.Prim.TYPE GHC.Types.LiftedRep) bool bool) with func(0 , [(GHC.Prim.6$$ @(42) @(43) @(44) @(45));
(GHC.Types.6$6$ @(42) @(43) @(44) @(45))]) in expression: lq_tmp$x##1556 == GHC.Types.Eq#
because
Elaborate fails on lq_tmp$x##1556 == GHC.Types.Eq#
in environment
GHC.Types.Eq# := func(4 , [(GHC.Prim.6$$ @(0) @(1) @(2) @(3));
(GHC.Types.6$6$ @(0) @(1) @(2) @(3))])
lq_tmp$x##1556 := (GHC.Types.6$6$ (GHC.Prim.TYPE GHC.Types.LiftedRep) (GHC.Prim.TYPE GHC.Types.LiftedRep) bool bool)
我做错了什么?从我的实验来看,这似乎是由于试图证明某些谓词函数对某些参数为真造成的。
问题是我应该使用 NewProofCombinators
而不是 ProofCombinators
。然后将 ==.
替换为 ===
并将 castWithTheorem (even_double x) (double' x)
替换为 (double' x) `withProof` (even_double x)
修复了问题:http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1543595949_5844.hs
我找到的所有在线资源都使用 ProofCombinators
,希望这可以减轻一些人的痛苦。
来源:https://github.com/ucsd-progsys/liquidhaskell/issues/1378#issuecomment-443262472
作为我遇到的问题的一个最小示例,这里有一个自然数的定义、一个加倍函数和一个由均匀性谓词细化的类型:
data Nat' = Z | S Nat' deriving Show
{-@ reflect double' @-}
double' :: Nat' -> Nat'
double' Z = Z
double' (S x) = (S (S (double' x)))
{-@ type Even' = {v:Nat' | even' v} @-}
{-@ reflect even' @-}
even' :: Nat' -> Bool
even' Z = True
even' (S Z) = False
even' (S (S x)) = even' x
我想先声明 {-@ double' :: Nat' -> Even' @-}
然后证明这是真的,但我的印象是我必须先写证明然后使用 castWithTheorem
(这本身对我有用)这样:
{-@ even_double :: x:Nat' -> {even' (double' x)} @-}
even_double Z = even' (double' Z)
==. even' Z
==. True
*** QED
even_double (S x) = even' (double' (S x))
==. even' (S (S (double' x)))
==. even' (double' x)
? even_double x
==. True
*** QED
{-@ double :: Nat' -> Even' @-}
double x = castWithTheorem (even_double x) (double' x)
但是,这会产生相当难以辨认的错误,例如:
:1:1-1:1: Error
elaborate solver elabBE 177 "lq_anf$##7205759403792806976##d3tK" {lq_tmp$x##1556 : (GHC.Types.6$6$ (GHC.Prim.TYPE GHC.Types.LiftedRep) (GHC.Prim.TYPE GHC.Types.LiftedRep) bool bool) | [(lq_tmp$x##1556 = GHC.Types.Eq#)]} failed on:
lq_tmp$x##1556 == GHC.Types.Eq#
with error
Cannot unify (GHC.Types.6$6$ (GHC.Prim.TYPE GHC.Types.LiftedRep) (GHC.Prim.TYPE GHC.Types.LiftedRep) bool bool) with func(0 , [(GHC.Prim.6$$ @(42) @(43) @(44) @(45));
(GHC.Types.6$6$ @(42) @(43) @(44) @(45))]) in expression: lq_tmp$x##1556 == GHC.Types.Eq#
because
Elaborate fails on lq_tmp$x##1556 == GHC.Types.Eq#
in environment
GHC.Types.Eq# := func(4 , [(GHC.Prim.6$$ @(0) @(1) @(2) @(3));
(GHC.Types.6$6$ @(0) @(1) @(2) @(3))])
lq_tmp$x##1556 := (GHC.Types.6$6$ (GHC.Prim.TYPE GHC.Types.LiftedRep) (GHC.Prim.TYPE GHC.Types.LiftedRep) bool bool)
我做错了什么?从我的实验来看,这似乎是由于试图证明某些谓词函数对某些参数为真造成的。
问题是我应该使用 NewProofCombinators
而不是 ProofCombinators
。然后将 ==.
替换为 ===
并将 castWithTheorem (even_double x) (double' x)
替换为 (double' x) `withProof` (even_double x)
修复了问题:http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1543595949_5844.hs
我找到的所有在线资源都使用 ProofCombinators
,希望这可以减轻一些人的痛苦。
来源:https://github.com/ucsd-progsys/liquidhaskell/issues/1378#issuecomment-443262472