如何构建具有依赖类型长度的列表？

将我的脚趾浸入依赖类型的水域中，我对规范的“具有静态类型长度的列表”示例进行了破解。

{-# 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

我明白为什么会发生这种情况：返回类型Cons折叠的每次迭代都是不同的 - 这就是重点！但我看不到解决办法，可能是因为我对这个主题的阅读不够深入。 （我无法想象所有这些努力都被投入到一个在实践中不可能使用的类型系统中！）

那么：如何从“正常”简单类型数据构建这种依赖类型数据？

按照@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关于由此产生的SafeList。这种知识的缺乏大致就是存在主义的ASafeList捕获。

这个问题能解决吗？我觉得我可能已经走上了逻辑的死胡同。

永远不要扔掉任何东西。

如果您打算不厌其烦地沿着列表创建一个长度索引列表（在文献中称为“向量”），您最好记住它的长度。

所以，我们有

data Nat = Z | S Nat

data Vec :: Nat -> * -> * where -- old habits die hard
  VNil :: Vec Z a
  VCons :: a -> Vec n a -> Vec (S n) a

但我们也可以为静态长度提供运行时表示。 Richard Eisenberg 的“Singletons”包将为您完成此操作，但基本思想是为静态数字提供一种运行时表示形式。

data Natty :: Nat -> * where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

至关重要的是，如果我们有一个类型值Natty n，然后我们可以询问该值以找出什么n is.

Hasochists 知道运行时可表示性通常非常无聊，甚至机器都可以管理它，因此我们将其隐藏在类型类中

class NATTY (n :: Nat) where
  natty :: Natty n

instance NATTY Z where
  natty = Zy

instance NATTY n => NATTY (S n) where
  natty = Sy natty

现在，我们可以对您从列表中获得的长度进行稍微更具信息性的存在主义处理。

data LenList :: * -> * where
  LenList :: NATTY n => Vec n a -> LenList a

lenList :: [a] -> LenList a
lenList []        = LenList VNil
lenList (x : xs)  = case lenList xs of LenList ys -> LenList (VCons x ys)

您将获得与长度破坏版本相同的代码，但您可以随时获取长度的运行时表示，并且不需要沿着向量爬行来获取它。

当然，如果你希望长度为Nat，这仍然是一个痛苦，你反而有一个Natty n对于一些n.

把口袋弄得乱七八糟是错误的。

Edit我想我应该添加一点，以解决“安全头”的使用问题。

首先，让我添加一个解包器LenList这给了你手中的数字。

unLenList :: LenList a -> (forall n. Natty n -> Vec n a -> t) -> t
unLenList (LenList xs) k = k natty xs

现在假设我定义

vhead :: Vec (S n) a -> a
vhead (VCons a _) = a

强化安全属性。如果我有一个向量长度的运行时表示，我可以查看它是否vhead适用。

headOrBust :: LenList a -> Maybe a
headOrBust lla = unLenList lla $ \ n xs -> case n of
  Zy    -> Nothing
  Sy _  -> Just (vhead xs)

所以你看一件事，并在这样做的过程中了解另一件事。