haskell – 依赖键入’ZipVector’应用程序

我已经使自己成为“ZipVector”风格应用于有限向量,它使用和类型将有限向量粘合到模拟“无限”向量的单元.

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

这可能足以满足我的需求,但是我想要一个“固定维度”模型,可以通过依赖键入的“Vector”获得的应用实例建模.

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

其中d幻影参数是类型级别的Nat.我怎么能(如果可能的话)在Haskell中编写reifiedDimension？此外,如果可能的话,给定(点v1)::点d1 a和(点v2)::点d2 a我怎样才能得到长度v1 ==长度v2我能得到d1~d2？

How can I (if it’s possible) write reifiedDimension in Haskell?

使用GHC.TypeLits和ScopedTypeVariables：

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

有关完整示例,请参见my answer here.

Moreover, again if possible, given (Point v1) :: Point d1 a and (Point v2) :: Point d2 a how can I get length v1 == length v2 can I get d1 ~ d2?

使用Data.Vector,没有.您需要一个矢量类型来编码类型中的长度.您可以做的最好的事情就是自己维护它并通过不导出Point构造函数来封装它.