haskell – 如何使用依赖类型的长度构建列表？

{-# 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)
Cons 5 (Cons 3 Nil) :: Num a => SafeList ('S ('S 'Z)) a

ghci> safeHead (Cons 'x' (Cons 'c' Nil))
'x'

ghci> safeHead Nil
Couldn't match type 'Z with 'S n0
Expected type: SafeList ('S n0) a0
  Actual type: SafeList 'Z a0
In the first argument of `safeHead',namely `Nil'
In the expression: safeHead Nil
In an equation for `it': it = safeHead Nil

然而,为了使这个数据类型真正有用,我应该可以从编译时不知道长度的运行时数据构建它.我天真的尝试：

fromList :: [a] -> SafeList n a
fromList = foldr Cons Nil

这无法编译,类型错误：

Couldn't match type 'Z with 'S n
Expected type: a -> SafeList n a -> SafeList n a
  Actual type: a -> SafeList n a -> SafeList ('S n) a
In the first argument of `foldr',namely `Cons'
In the expression: foldr Cons Nil
In an equation for `fromList': fromList = foldr Cons Nil

我明白为什么会发生这种情况：对于每次迭代迭代,缺点的返回类型是不同的 – 这就是整体而言！但是我看不清楚,可能是因为我没有深入阅读这个主题. (我不能想象所有这些努力都被放在一个不可能在实践中使用的类型系统中！)

那么,如何从“普通”简单类型的数据构建这种依赖类型的数据？

以下@ luqui的建议我能够使fromList编译：

data ASafeList a where
    ASafeList :: SafeList n a -> ASafeList a

fromList :: [a] -> ASafeList a
fromList = foldr f (ASafeList Nil)
    where f x (ASafeList xs) = ASafeList (Cons x xs)

这是我尝试解压缩ASafeList并使用它：

getSafeHead :: [a] -> a
getSafeHead xs = case fromList xs of ASafeList ys -> safeHead ys

这会导致另一种类型错误：

Couldn't match type `n' with 'S n0
  `n' is a rigid type variable bound by
      a pattern with constructor
        ASafeList :: forall a (n :: Nat). SafeList n a -> ASafeList a,in a case alternative
      at SafeList.hs:33:22
Expected type: SafeList ('S n0) a
  Actual type: SafeList n a
In the first argument of `safeHead',namely `ys'
In the expression: safeHead ys
In a case alternative: ASafeList ys -> safeHead ys

再次,直观地说,这是无法编译的.我可以用一个空列表调用fromList,所以编译器不能保证我能够在安全列表上调用safeHead.这种缺乏知识大概是存在的ASafeList捕获.

这个问题可以解决吗？我觉得我可能已经走下了一个逻辑的死胡同.