我发现我真的很喜欢将 GADT 与 Data Kinds 结合使用,因为它为我提供了比以前更多的类型安全性(对于大多数用途,几乎与 Coq、Agda 等人一样好)。可悲的是,模式匹配在最简单的示例上失败了,除了类型类之外,我想不出其他方法来编写我的函数。
这是一个解释我悲伤的例子:
data Nat = Z | S Nat deriving Eq
data Le :: Nat -> Nat -> * where
Le_base :: Le a a
Le_S :: Le a b -> Le a (S b)
class ReformOp n m where
reform :: Le (S n) (S m) -> Le n m
instance ReformOp a a where
reform Le_base = Le_base
instance ReformOp a b => ReformOp a (S b) where
reform (Le_S p) = Le_S $ reform p
class TransThm a b c where
trans :: Le a b -> Le b c -> Le a c
instance TransThm a a a where
trans = const
instance TransThm a a b => TransThm a a (S b) where
trans Le_base (Le_S p) = Le_S $ trans Le_base p
instance (TransThm a b c, ReformOp b c) => TransThm a (S b) (S c) where
trans (Le_S p) q = Le_S $ trans p $ reform q
我们有 2 个类型类(一个用于定理,一个用于实用程序操作)和 5 个实例 - 仅用于一个微不足道的定理。理想情况下,Haskell 可以查看这个函数:
-- not working, I understand why
trans :: Le a b -> Le b c -> Le a c
trans Le_base Le_base = Le_base
trans Le_base (Le_S p) = Le_S $ trans Le_base p
trans (Le_S p) q = Le_S $ trans p $ reform q
并对每个子句单独进行类型检查,并在每次调用时决定哪些情况是可能的(因此值得尝试匹配),哪些情况不是,所以在调用
trans Le_base Le_base
时Haskell 会注意到只有第一种情况允许三个变量相同,并且只尝试匹配第一个子句。
最佳答案
我看不到您对 trans
的模式匹配定义如何。将在 Agda 或 Coq 中工作。
如果您改为编写以下内容,则它可以工作:
reform :: Le (S n) (S m) -> Le n m
reform Le_base = Le_base
reform (Le_S Le_base) = Le_S Le_base
reform (Le_S (Le_S p)) = Le_S (reform (Le_S p))
trans :: Le a b -> Le b c -> Le a c
trans Le_base q = q
trans (Le_S p) Le_base = Le_S p
trans (Le_S p) (Le_S q) = Le_S (trans p (reform (Le_S q)))
当然,你也可以更直接地定义:
trans :: Le a b -> Le b c -> Le a c
trans p Le_base = p
trans p (Le_S q) = Le_S (trans p q)
关于具有数据种类的 GADT 上的 Haskell 模式匹配,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/12067503/