5

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

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

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

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

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

4

3 回答 3

3

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

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

它强制连接两个列表为您提供一个具有两个长度总和的新列表的不变量。

于 2013-11-05T01:53:10.697 回答
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].

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

于 2013-11-04T20:59:13.843 回答
2

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

例如：

{-# 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两个运行时列表。

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

于 2013-11-05T06:58:41.980 回答