<div dir="ltr">Hello,<div><br></div><div>I am working on a Vector class, heavily based on the paper "Faking It: Simulating Dependent Types in Haskell" by Connor McBride.</div><div><br></div><div>Here is a stripped down version of my code:</div><div><br></div><div>---</div><div><br></div><div><div>{-# LANGUAGE RankNTypes #-}</div><div>                           </div><div>import Control.Applicative</div><div>import Data.Functor</div><div><br></div><div>infixr 5 :.</div><div>data Cons u t = (:.) t (u t) deriving (Show)</div><div><br></div><div>data Nil t = Nil deriving (Show)</div><div><br></div><div>class (Applicative v, Functor v) => Vector v where</div><div>  wrap :: (forall u. Vector u => s -> f (u t) -> f (Cons u t)) -> f (Nil t) -> v s -> f (v t)</div><div><br></div><div>instance (Vector u) => Vector (Cons u) where</div><div>  wrap f n (x:.xs) = f x (wrap f n xs)</div><div><br></div><div>instance Vector Nil where</div><div>  wrap _ n Nil = n</div><div><br></div><div>instance (Applicative u) => Applicative (Cons u) where</div><div>  pure x = x:.(pure x)</div><div>  (f:.fs) <*> (x:.xs) = (f x):.(fs <*> xs)</div><div><br></div><div>instance Applicative Nil where</div><div>  pure _ = Nil</div><div>  _ <*> _ = Nil</div><div><br></div><div>instance (Functor u) => Functor (Cons u) where</div><div>  fmap f (x:.xs) = (f x):.(fmap f xs)</div><div><br></div><div>instance Functor Nil where</div><div>  fmap _ Nil = Nil</div><div><br></div><div>transpose :: (Vector w, Vector u) => w (u t) -> u (w t)</div><div>transpose v = wrap (\x xs -> (:.) <$> x <*> xs) (pure Nil) v</div></div><div><br></div><div>---</div><div><br></div><div>I am having trouble understanding the type signature of 'wrap'. This is how I interpret it:</div><div>(function that takes an 's' and container of 'u t' and returns a container of 'Cons u t') -> </div><div>(container of 'Nil') -> </div><div>(a vector of 's') -> </div><div>(a container with the same type as the container of Nil, but containing v t instead)</div><div><br></div><div>What doesn't make sense to me is how the signature seems to imply that the structure of the container in the return type is the same as the structure of the container holding the Nils, but in 'transpose' the container holding Nil seems to be infinite.</div><div><br></div><div>Can someone help me to understand what is going on here?</div><div><br></div><div>Thanks,</div><div>Ben</div></div>