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@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