Dipendentemente digitato 'ZipVector' applicativi

Question

ho fatto io stesso un "ZipVector" stile Applicative sulla finite Vector s che utilizza un tipo di somma da incollare vettori finiti a Unit s quale modello vettori "infinito".

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 

Questo sarà probabilmente sufficiente per le mie esigenze, ma io volevo una pigramente "Fixed Dimensional" uno sul modello delle istanze applicative che si possono ottenere con la s "Vector" dipendente digitati.

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 

dove il parametro d fantasma è un tipo di livello Nat. Come posso (se possibile) scrivere reifiedDimension in Haskell? Inoltre, sempre se possibile, dato (Point v1) :: Point d1 a e (Point v2) :: Point d2 a come posso ottenere length v1 == length v2 posso ottenere d1 ~ d2?

Answer 1

Come posso (se possibile) scrivere reifiedDimension in Haskell?

Utilizzando GHC.TypeLits e ScopedTypeVariables:

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

Vedi my answer here per un esempio completo.

Inoltre, sempre se possibile, data (Point v1) :: Point d1 a e (Point v2) :: Point d2 a come posso ottenere length v1 == length v2 posso ottenere d1 ~ d2?

Con Data.Vector, n. Avresti bisogno di un tipo di vettore che codifichi la lunghezza nel tipo. Il meglio che puoi fare è di mantenerlo da solo e incapsularlo non esportando il costruttore Point.