Hello,<div><br></div><div>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.</div>
<div>You'd have to use a structured singleton family, where the values are linked to the types:</div><div><br></div><div>data SNat :: Nat -> * where</div><div> SZero :: SNat Zero</div><div> SSucc :: SNat n -> SNat (Succ n)</div>
<div><br></div><div>repeat :: SNat n -> a -> Vector n a </div><div><br></div><div>Apologies for the confusion,</div><div>-Iavor</div><div><br></div><div><br></div><div><br></div><div><br><br><div class="gmail_quote">
On Thu, Oct 25, 2012 at 9:03 AM, Andres Löh <span dir="ltr"><<a href="mailto:andres.loeh@gmail.com" target="_blank">andres.loeh@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Iavor.<br>
<div class="im"><br>
> If you don't want to use the class system, you could write `repeat` with a<br>
> type like this:<br>
><br>
> repeat :: Proxy n -> a -> Vector n a<br>
><br>
> (`Proxy` is the singleton family 'data Proxy n = Proxy`).<br>
<br>
</div>How is the polymorphism becoming any less parametric by using this<br>
particular Proxy type?<br>
<br>
Cheers,<br>
Andres<br>
</blockquote></div><br></div>