5

我在有限s 上为自己创建了一个“ ZipVector”样式，它使用 sum 类型将有限向量粘合到模拟“无限”向量的 s 上。ApplicativeVectorUnit

data ZipVector a = Unit a | ZipVector (Vector a)
             deriving (Show, Eq)

instance Functor ZipVector where
  fmap f (Unit a)  = Unit (f a)
  fmap f (ZipVector va) = ZipVector (fmap f va)

instance Applicative ZipVector where
  pure = Unit
  Unit f   <*> p        = fmap f p
  pf       <*> Unit x   = fmap ($ x) pf
  ZipVector vf <*> ZipVector vx = ZipVector $ V.zipWith ($) vf vx

这可能足以满足我的需求，但我很想有一个“固定维度”模型，它以应用实例为模型，您可以通过依赖类型的“向量”获得。

data Point d a = Point (Vector a) deriving (Show, Eq)

instance Functor (Point d) where
  fmap f (Point va) = Point (fmap f va)

instance Applicative Point where
  pure = Vector.replicate reifiedDimension
  Point vf <*> Point vx = Point $ V.zipWith ($) vf vx

其中dphantom 参数是 type-level Nat。我如何（如果可能）用reifiedDimensionHaskell 编写代码？此外，如果可能的话，再次给定(Point v1) :: Point d1 a，(Point v2) :: Point d2 a我怎么能length v1 == length v2得到d1 ~ d2？

4

1 回答 1

4

我如何（如果可能）用reifiedDimensionHaskell 编写代码？

使用GHC.TypeLits和ScopedTypeVariables：

instance SingI d => Applicative (Point d) where
  pure = Point . Vector.replicate reifiedDimension
    where reifiedDimension = fromInteger $ fromSing (sing :: Sing d)
  ...

有关完整示例，请参见我的答案。

此外，如果可能的话，再次给定(Point v1) :: Point d1 a，(Point v2) :: Point d2 a我怎么能length v1 == length v2得到d1 ~ d2？

与Data.Vector，没有。您需要一个向量类型来编码类型中的长度。你能做的最好的就是自己维护它并通过不导出Point构造函数来封装它。

于 2013-04-24T00:52:50.253 回答