如何构建具有依赖类型长度的列表? [英] How do I build a list with a dependently-typed length?

问题描述

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

Dipping my toe into the waters of dependent types, I had a crack at the canonical "list with statically-typed length" example.

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

然而，为了使这种数据类型真正有用，我应该能够从编译时不知道长度的运行时数据中构建它.我幼稚的尝试:

However, in order for this data-type to be actually useful, I should be able to build it from run-time data for which you don't know the length at compile time. My naïve attempt:

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 的返回类型对于折叠的每次迭代都是不同的 - 这就是重点！但我看不到解决方法，可能是因为我对这个主题的阅读不够深入.(我无法想象所有这些努力都被投入到一个在实践中无法使用的类型系统中！)

I understand why this is happening: the return type of Cons is different for each iteration of the fold - that's the whole point! But I can't see a way around it, probably because I've not read deeply enough into the subject. (I can't imagine all this effort is being put into a type system that is impossible to use in practice!)

那么:我怎样才能从正常"的简单类型数据构建这种依赖类型的数据?

So: How can I build this sort of dependently-typed data from 'normal' simply-typed data?

按照@luqui 的建议，我能够编译 fromList:

Following @luqui's advice I was able to make fromList compile:

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 并使用它:

Here's my attempt to unpack the ASafeList and use it:

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

这会导致另一个类型错误:

This causes another type error:

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，因此编译器不能保证我能够在结果 SafeList 上调用 safeHead.这种知识的缺乏大致就是存在的 ASafeList 所捕获的.

Again, intuitively it makes sense that this would fail to compile. I can call fromList with an empty list, so the compiler has no guarantee that I'll be able to call safeHead on the resulting SafeList. This lack of knowledge is roughly what the existential ASafeList captures.

这个问题能解决吗?我觉得我可能已经走到了一个合乎逻辑的死胡同.

Can this problem be solved? I feel like I might have walked down a logical dead-end.

推荐答案

永远不要扔掉任何东西.

Never throw anything away.

如果您要不厌其烦地沿着一个列表制作一个长度索引列表(在文献中称为向量")，您最好记住它的长度.

If you're going to take the trouble to crank along a list to make a length-indexed list (known in the literature as a "vector"), you may as well remember its length.

所以，我们有

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) 的单身人士"包将为您完成此操作，但基本思想是为静态数字提供一种运行时表示.

but we can also give a run time representation to static lengths. Richard Eisenberg's "Singletons" package will do this for you, but the basic idea is to give a type of run time representations for static numbers.

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

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

Crucially, if we have a value of type Natty n, then we can interrogate that value to find out what n is.

Hasochists 知道运行时的可表示性通常很无聊，连机器都可以管理它，所以我们将它隐藏在一个类型类中

Hasochists know that run time representability is often so boring that even a machine can manage it, so we hide it inside a type class

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

instance NATTY Z where
  natty = Zy

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

现在，我们可以对您从列表中获得的长度进行更丰富的存在主义处理.

Now we can give a slightly more informative existential treatment of the length you get from your lists.

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)

您获得的代码与破坏长度的版本相同，但您可以随时获取长度的运行时表示，而无需沿着向量爬行来获取它.

You get the same code as the length-destroying version, but you can grab a run time representation of the length anytime you like, and you don't need to crawl along the vector to get it.

当然，如果你希望长度是一个Nat，你仍然很痛苦，因为你有一个Natty n来代替一些n>.

Of course, if you want the length to be a Nat, it's still a pain that you instead have a Natty n for some n.

把口袋弄乱是错误的.

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

Edit I thought I'd add a little, to address the "safe head" usage issue.

首先，让我为 LenList 添加一个解包器，它会给出你手中的数字.

First, let me add an unpacker for LenList which gives you the number in your hand.

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 是否适用.

enforcing the safety property. If I have a run time representation of the length of a vector, I can look at it to see if vhead applies.

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

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

So you look at one thing, and in doing so, learn about another.

这篇关于如何构建具有依赖类型长度的列表?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！