haskell - 为类型安全向量实现 zipWith

Question

我正在尝试编写一个具有类型安全长度的向量库，这意味着添加两个不同长度的向量将不会成功。

我目前的实现大致是:

data Natural where
  Zero :: Natural
  Succ :: Natural -> Natural

type One   = Succ Zero
type Two   = Succ One
type Three = Succ Two
type Four  = Succ Three

data Vector n e where
  Nil  :: Vector Zero e
  (:|) :: e -> Vector n e -> Vector (Succ n) e

infixr :|

我现在正在尝试实现 zipWith，因为它将有助于实现 dot 产品和 Num 类型类等内容。

我已经走到这一步了

zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipWith f (a :| as) (b :| bs) = f a b :| zipWith f as bs
zipWith _ _ _ = Nil

但我收到错误

Couldn't match type `n' with 'Zero
      `n' is a rigid type variable bound by
          the type signature for
            zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
          at LinearAlgebra.hs:51:12
    Expected type: Vector n c
      Actual type: Vector 'Zero c
    In the expression: Nil
    In an equation for `zipWith': zipWith _ _ _ = Nil

我认为原因是变量 n 只能取一个值 - Succ 或 0？

我该如何解决这个问题？

Answer 1

采用以下模式:

zipWith _ as bs = Nil

这里GHC只知道as的类型是Vector n a，bs的类型是Vector n b >，来自函数的签名。此外，签名表明右侧必须具有类型 Vector n c，其中 n 与中的其他 n-s 相同。左手边。对于任意 x，Nil 的类型为 Vector Zero x。

类型不匹配，因为左侧的长度参数是未知的任意n，而右侧的长度零。参数的模式匹配会带来必要的附加信息:

zipWith _ Nil Nil = Nil 
-- "zipWith _ as Nil" also works, because now "as" is constrained to also have Zero length

如果您有 GHC 7.8.x，则可以编写以下内容:

zipWith f as bs = _

GHC 将为您提供有关孔的预期类型和范围内变量类型的非常有用的消息(根据 GHC 的最佳知识，考虑到您已进行模式匹配的构造函数)。