我发现我真的很喜欢将GADT与Data Kinds结合使用，因为它为我提供了比以前更多的类型安全性（对于大多数用途，几乎和Coq，Agda等一样好）。可悲的是，模式匹配在最简单的例子上失败了，除了类型类之外，我想不出写函数的方法。 这里的解释我的悲伤的例子： data Nat = Z | S Nat deriving Eq
data Le :: Nat -> Nat -> * where
我一直在教我自己关于类型级编程，并想写一个简单的自然数加法类型的函数。我这工作的第一个版本如下： data Z
data S n
type One = S Z
type Two = S (S Z)
type family Plus m n :: *
type instance Plus Z n = n
type instance Plus (S m) n = S (Plus m n