相关疑难解决方法(0)

把我的脚趾浸入依赖类型的水域,我在规范的"静态类型长度列表"示例中有一个裂缝.

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

-- a kind declaration
data Nat = Z | S Nat

data SafeList :: (Nat -> * -> *) where
    Nil :: SafeList Z a
    Cons :: a -> SafeList n a -> SafeList (S n) a

-- the type signature ensures that the input list has at least one element
safeHead :: SafeList (S n) a -> a
safeHead (Cons x xs) = x

这似乎有效:

ghci> :t Cons 5 (Cons 3 Nil) …