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

Question

我们可以定义函数f,g像这样:

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

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

双方f并g采取两个列表作为参数,并返回一个新的列表,但它们是不同的:f返回一个列表较长,其长度的输入的总和,同时g处理列出与相同的长度.如何计算出Haskell？

Answer 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

这清楚地区分了列表长度会发生什么.

另请参见类型算术.