[Haskell-cafe] Type-directed functions with data kinds

[Iavor Diatchki]

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.loeh at 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121025/36920098/attachment.htm>