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

【问题标题】：How to use length annotated lists in Haskell如何在 Haskell 中使用长度注释列表
【发布时间】：2013-11-04 20:33:08
【问题描述】：

显然，通过一些 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

虽然我明白为什么这很有用，但我在实际使用它时遇到了麻烦。

如何创建这样的列表？（除了硬编码到程序中。）

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

您能否指出一些使用这些技术的现有代码？

【问题讨论】：

标签： haskell types static-typing

【解决方案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

它强制连接两个列表的不变量得到一个具有两个长度总和的新列表。

【讨论】：

所以，我有点晚了，但我不知道你将如何实际使用它？ fromList 给出了UList，但您给出的函数示例需要List。您如何从UList 中获得List，以便您可以申请mapList？

【解决方案2】：

您几乎需要对其进行硬编码，因为类型当然是在编译时固定的，并且 GHC 类型检查器的图灵完整性不能被滥用来“自行”生成它们^{1。然而，这并不像听起来那么戏剧化：您基本上只需要编写一次长度注释类型。其余的可以在不提及特定长度的情况下完成，尽管周围有一些看起来很奇怪的类：}

class LOL l where
  lol :: [a] -> l a

instance LOL (List Z) where
  lol _ = Nil

instance (LOL (List n)) => LOL (List (S n)) where
  lol (x:xs) = Cons a $ lol xs
  lol [] = error "Not enough elements given to make requested type length."

然后你可以使用类似的东西

type Four = S(S(S(S Z)))

get4Vect :: Read a => IO (List Four a)
get4Vect = lol . read <$> getLine    -- For input format [1,2,3,4].

¹我不会在这里讨论 Template Haskell，它当然可以很容易地在编译时自动生成任何东西。

【讨论】：

您可能对 GHC 类型检查器如何完成图灵感兴趣：haskell.org/haskellwiki/Type_SK
我当然对此感兴趣！因此，使用 UndecidableInstances 时，Haskell 类型系统本身就可以比 Agda 作为一个整体做更多的事情。诡异...

【解决方案3】：

长度编码在编译期间起作用，因此类型检查器显然无法验证在运行时创建的列表的长度，例如用户输入。这个想法是您将任何运行时列表包装在隐藏长度参数的存在类型中，然后您必须提供有关长度的证明才能使用列表。

例如：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Lists where

data Nat = Z | S Nat

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

data DynList a where
    DynList :: List l a -> DynList a

data Refl a b where
    Refl :: Refl a a

fromList :: [a] -> DynList a
fromList []     = DynList Nil
fromList (x:xs) = cons (fromList xs) where
    cons (DynList rest) = DynList $ Cons x rest

toList :: List l a -> [a]
toList Nil = []
toList (Cons x xs) = x : toList xs

dot :: Num a => List l a -> List l a -> List l a
dot Nil Nil = Nil
dot (Cons x xs) (Cons y ys) = Cons (x*y) (dot xs ys)

haveSameLength :: List l a -> List l' b -> Maybe (Refl l l')
haveSameLength Nil Nil                 = Just Refl
haveSameLength (Cons _ xs) (Cons _ ys) = case haveSameLength xs ys of
    Just Refl -> Just Refl
    Nothing   -> Nothing
haveSameLength _ _                     = Nothing

main :: IO ()
main = do
    dlx :: DynList Double <- fmap (fromList . read) getLine
    dly :: DynList Double <- fmap (fromList . read) getLine

    case (dlx, dly) of
        (DynList xs, DynList ys) -> case haveSameLength xs ys of
            Just Refl -> print $ toList $ dot xs ys
            Nothing   -> putStrLn "list lengths do not match"

这里的DynList 是一个动态长度列表（即长度仅在运行时知道），它包含一个正确键入的List。现在，我们有一个dot 函数，它计算两个具有相同长度的列表的点积，所以如果我们像示例中那样从标准输入读取列表，我们必须提供证据证明这些列表实际上具有长度相同。

这里的“证明”是Refl 构造函数。声明构造函数的方式意味着如果我们可以提供Refl a b 类型的值，那么a 和b 必须是相同的类型。因此，我们使用hasSameLength 来验证生成的Refl 值的类型和模式匹配，这为类型检查器提供了足够的信息，让我们可以在两个运行时列表上调用dot。

所以这本质上意味着类型检查器将强制我们手动验证任何在编译时未知的列表的长度，以便编译代码。

【讨论】：