Hello, Sorry, I made a mistake, the version of 'repeat :: Proxy n -> a -> Vector n a' won't work either, as Andres noticed, because `Proxy` still won't give you information about how many times to repeat. You'd have to use a structured singleton family, where the values are linked to the types:
data SNat :: Nat -> * where SZero :: SNat Zero SSucc :: SNat n -> SNat (Succ n) repeat :: SNat n -> a -> Vector n a Apologies for the confusion, -Iavor On Thu, Oct 25, 2012 at 9:03 AM, Andres Löh <andres.l...@gmail.com> wrote: > Hi Iavor. > > > If you don't want to use the class system, you could write `repeat` with > a > > type like this: > > > > repeat :: Proxy n -> a -> Vector n a > > > > (`Proxy` is the singleton family 'data Proxy n = Proxy`). > > How is the polymorphism becoming any less parametric by using this > particular Proxy type? > > Cheers, > Andres >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
