如何在Haskell中使用长度注释列表

Question

显然,通过一些GHC扩展,可以定义一种类型的列表,其长度在类型中编码,如下所示:

{-# LANGUAGE GADTs, EmptyDataDecls #-}

data Z
data S a

data List l a where
  Nil  :: List Z a
  Cons :: a -> List l a -> List (S l) a

虽然我知道为什么这会有用,但我实际上使用它时遇到了麻烦.

如何创建这样的列表？(除了将其硬编码到程序中.)

假设有人想创建一个程序,从终端读取两个这样的列表并计算它们的点积.虽然很容易实现实际的乘法函数,但程序如何读取数据呢？

你能指点一些使用这些技术的现有代码吗？

Answer 1

您不必对列表的长度进行硬编码；相反，您可以定义以下类型：

data UList a where
    UList :: Nat n => List n a -> UList a

在哪里

class Nat n where
    asInt :: n -> Int

instance Nat Z where
    asInt _ = 0

instance Nat n => Nat (S n) where
    asInt x = 1 + asInt (pred x)
      where
        pred = undefined :: S n -> n

我们还有

fromList :: [a] -> UList a
fromList [] = UList Nil
fromList (x:rest) =
    case fromList rest of
        UList xs -> UList (Cons x xs)

此设置允许您创建其长度在编译时未知的列表；您可以通过执行模式匹配从存在包装器中提取类型来访问长度case，然后使用该类Nat将类型转换为整数。

您可能想知道拥有一个在编译时不知道其值的类型有什么好处？答案是，尽管您不知道类型是什么，但您仍然可以强制执行不变量。例如，以下代码保证不会更改列表的长度：

mapList :: (a -> b) -> List n a -> List n b

如果我们使用名为 的类型族进行类型加法Add，那么我们可以写

concatList :: List m a -> List n a -> List (Add m n) a

这强制了连接两个列表会得到一个具有两个长度之和的新列表的不变式。