Dependently typed 'ZipVector' Applicatives

Question

I've made myself a "ZipVector" style Applicative on finite Vectors which uses a sum type to glue finite vectors to Units 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. How can I (if it's possible) write reifiedDimension in Haskell? 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?

Answer 1

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.