如何强制 Haskell 检查列表的长度？答案

【问题标题】：How to force Haskell to check lengths of lists?如何强制 Haskell 检查列表的长度？
【发布时间】：2013-12-30 22:32:21
【问题描述】：

我们可以像这样定义函数f和g：

f :: [a] -> [a] -> [a]
f = (++)

g :: [a] -> [a] -> [a]
g = zipWith (+)

f 和 g 都将两个列表作为参数并返回一个新列表，但它们不同：f 返回一个较长的列表，其长度是输入的总和，同时g 处理列表具有相同的长度。如何向 Haskell 弄清楚这一点？

【问题讨论】：

实际上g 将具有Num a => [a] -> [a] -> [a] 类型，因此它不适用于任意列表，仅适用于数字列表。另外，能否请您澄清一下您的问题？
@chris 好的，我可以强制f :: Num a => [a] -> [a] -> [a]，所以这两种类型声明没有区别。我的观点是，Haskell 不会同时抱怨f (g [1..10] [11..20]) [21..30] 和g (f [1..10] [11..20]) [21..30]，但我希望 Haskell 可以对后者给出警告或错误（编译时，而不是运行时）。
@SaltyEgg 这需要跟踪类型中的长度参数。可以在 Haskell 中笨拙地做到这一点，但是您对此有一个相当严格的限制，因为只有最现代的 GHC 才具有类型级计算的开始，例如整数加法。您更有可能想要这样做的是 Idris 或 Agda。
@chris 认为它是zipWith (,)。

标签： haskell types type-level-computation

【解决方案1】：

您想要的是将列表的长度编码到类型系统中。换句话说，在类型系统中编码自然数并对其进行操作。这是可能的，尽管它涉及一些类型的诡计。有一些库可以实现这一点，其中之一是tagged-list。 TaggedList 的长度被标记为类型级自然数。那么你的函数类型看起来像

import Data.List.Tagged as T
import TypeLevel.NaturalNumber.Operations (Plus)

f :: TaggedList n a -> TaggedList m a -> TaggedList (Plus n m) a
f = T.append

g :: (Num a) => TaggedList n a -> TaggedList n a -> TaggedList n a
g x = T.zipf (T.map (+) x) -- apparently the Tagged library lacks zipWith
                           -- so we implement it ourselves

这清楚地区分了列表长度所发生的情况。

另见Type arithmetic。

【讨论】：

【解决方案2】：

据我所知，您希望您的g 在执行操作之前先检查列表的长度是否相同。这相对容易：

-- Correct type signature as @chris mentioned
g :: Num a => [a] -> [a] -> [a]
g xs ys = if length xs == length ys then zipWith (+) xs ys else error "Incompatible lists"

但是，这是一种非常糟糕的抛出错误的方法，最好使用 Maybe monad：

g :: Num a => [a] -> [a] -> Maybe [a]
g xs ys = if length xs == length ys then Just $ zipWith (+) xs ys else Nothing

【讨论】：

我认为 OP 希望长度以 Idris Vectors 之类的类型表示，而不仅仅是在运行时检查。
@Lee 是的，如果我误用g，希望Haskell在编译代码时能投诉。
@SaltyEgg Haskell 不能那样工作，它怎么可能知道你是否在编译时传入了不同大小的列表？我的大部分数据来自外部硬件或在程序编译时甚至不一定存在的大文件，因此它无法检查这样的代码。 Haskell 列表不是向量，它们更像是链表，所以也许您可以尝试查看 Repa 库中的向量？我相信它们的大小已编码到类型中，但我可能是错的。
我检查过，Repa 对向量的形状（1D、2D、3D 等）进行编码，而不是大小。您可以使用类型级别Nats，但这会变得丑陋且速度很快。通常最好不要使用类型系统来进行计算，有更优雅的方式来表达您想要对运行时错误处理执行的操作。
您说得对，因此我不会投反对票，但是 OP 对自己的问题的了解比您少，因此他可能也没有想到其他列表类型。