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

Question

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

{-# 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捕获的.

这个问题可以解决吗？我觉得自己可能走在了一个合乎逻辑的死胡同.

Answer 1

永远不要扔东西.

如果你要煞费苦心地沿着列表来制作一个长度索引列表(在文献中称为"向量"),你也可以记住它的长度.

所以,我们有

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.

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.

把一个人的口袋弄得乱七八糟是个错误.

编辑我以为我会添加一点,以解决"安全头"使用问题.

首先,让我添加一个解包器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)

所以你看一件事,这样做,了解另一件事.

Answer 2

在

fromList :: [a] -> SafeList n a

n是普遍量化的 - 即这个签名声称我们应该能够SafeList从列表中构建任何长度.相反,您希望量化存在性,这只能通过定义新数据类型来完成:

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

然后你的签名应该是

fromList :: [a] -> ASafeList a

您可以通过模式匹配来使用它 ASafeList

useList :: ASafeList a -> ...
useList (ASafeList xs) = ...

在身体中,xs将是一个SafeList n a具有未知(刚性)的类型n.您可能需要添加更多操作才能以任何不平凡的方式使用它.