小编ber*_*gey的帖子

我正在试验Haskell的类型系统,并希望编写一个类型安全的附加功能.这个函数应该接受两个表示数字的单身证人,并返回一个数字的单身证人,其类型带有证明它确实是参数的总和.这是代码:

{-# language TypeFamilies, KindSignatures, DataKinds, PolyKinds, UndecidableInstances, GADTs #-}

data Nat = Zero | Succ Nat deriving Show
type family Add (m :: Nat) (n :: Nat) :: Nat where
  Add Zero n = n
  Add (Succ m) n = Add m (Succ n)

data SNat :: Nat -> * where
  Zy :: SNat Zero
  Suc :: SNat m -> SNat (Succ m)

data Bounded' m = B m

sum' :: Bounded' (SNat m) -> Bounded' (SNat n) -> …