Zależnie wpisane „ZipVector” Applicatives

Question

Zrobiłem się za „ZipVector” styl Applicative na skończonych Vector s który wykorzystuje typ suma wektorów do klejenia skończone Unit s który model „infinite” wektory.

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 

Prawdopodobnie będzie to wystarczające dla moich potrzeb, ale bezczynnie chcieliśmy „Fixed Dimensional” one wzorowane na aplikacyjnych przypadkach można uzyskać w sposób zależny wpisywanych „wektor” 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 

gdzie parametr d fantom typu poziomu Nat. Jak mogę (jeśli to możliwe) napisać reifiedDimension w Haskell? Co więcej, ponownie, jeśli to możliwe, biorąc pod uwagę (Point v1) :: Point d1 a i , w jaki sposób mogę uzyskać length v1 == length v2 mogę uzyskać d1 ~ d2?

Answer 1

Jak mogę (jeśli jest to możliwe) napisać reifiedDimension w Haskell?

Korzystanie GHC.TypeLits i ScopedTypeVariables:

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

Zobacz my answer here dla pełnego przykład.

Ponadto ponownie, jeśli to możliwe, biorąc pod uwagę (Point v1) :: Point d1 a i (Point v2) :: Point d2 a jak mogę dostać length v1 == length v2 mogę d1 ~ d2?

Z Data.Vector, nie. Potrzebny jest typ wektorowy, który koduje długość w typie. Najlepsze, co możesz zrobić, to zachować to samodzielnie i obudować je, nie eksportując konstruktora Point.