为类型安全的向量实现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或Zero ?

我该如何补救?

Answer 1

采用以下模式:

zipWith _ as bs = Nil

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

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

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的最佳知识，给定您的模式匹配的构造函数)。