Dependently typed 'ZipVector' Applicatives

Question

I've made myself a "`ZipVector`" style `Applicative` on finite `Vector`s which uses a sum type to glue finite vectors to `Unit`s which model "infinite" vectors. ``` 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 ``` This will probably be sufficient for my needs, but I idly wanted a "Fixed Dimensional" one modeled on the applicative instances you can get with dependently typed "Vector"s. ``` 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 ``` where the `d` phantom parameter is a type-level `Nat`…

Accepted Answer

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

Using `GHC.TypeLits` and `ScopedTypeVariables`:

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

See my answer here for a full example.

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`?

With `Data.Vector`, no. You'd need a vector type that encodes the length in the type. The best you can do is to maintain this yourself and encapsulate it by not exporting the `Point` constructor.

Dependently typed 'ZipVector' Applicatives

Solution

Problem