小编ski*_*ati的帖子

我正在试验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) -> …

to_c下面的函数由于在使用GADTs扩展编译时出现类型错误而被拒绝,我希望将其用于此处未显示的无关代码片段.

newtype Church = Church { unC :: forall a. (a -> a) -> a -> a }
to_c :: Int -> Church
to_c 0 = let f0 f c = c in Church f0
to_c n =
    let fn f c = iterate f c !! n in Church fn

错误信息:

Couldn't match type ‘a0’ with ‘a’ because type variable ‘a’ would escape its scope
  This (rigid, skolem) type variable is bound by
    a type expected by the …