Hello Paul,<div><br></div><div>If you don&#39;t want to use the class system, you could write `repeat` with a type like this:</div><div><br></div><div>    repeat :: Proxy n -&gt; a -&gt; Vector n a</div><div><br></div><div>
(`Proxy` is the singleton family &#39;data Proxy n = Proxy`).</div><div><br></div><div>You can&#39;t really do it with a function of type `a -&gt; Vector n a` because there is no way for the function to know how many elements to generate. </div>
<div>You cannot determine the length from the type `n` because polymorphism in Haskell is _parametric_, which means that the function needs to behave uniformly for all types.</div><div>This is nice because it makes reasoning about programs easier, but also, it allows for efficient implementation---there is no need to pass type-representations at run-time.</div>
<div>In contrast, overloaded values may behave differently depending on their type, just like your implementation of `repeat` below.  This is perfectly OK, and it is clearly marked in the type.</div><div><br></div><div><br>
</div><div>I hope this helps,</div><div>-Iavor</div><div><br></div><div><br></div><div><br><div class="gmail_quote">On Thu, Oct 25, 2012 at 8:22 AM, Paul Visschers <span dir="ltr">&lt;<a href="mailto:mail@paulvisschers.net" target="_blank">mail@paulvisschers.net</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello everyone,<div><br></div><div>I&#39;ve been playing around with the data kinds extension to implement vectors that have a known length at compile time. Some simple code to illustrate:</div>
<div><div>&gt; {-# LANGUAGE DataKinds, GADTs, KindSignatures #-}</div>
<div>&gt; </div><div>&gt; import Prelude hiding (repeat)</div><div>&gt; </div><div>&gt; data Nat = Zero | Succ Nat</div><div>&gt; data Vector (n :: Nat) a where</div><div>&gt;   Nil :: Vector Zero a</div><div>&gt;   Cons :: a -&gt; Vector n a -&gt; Vector (Succ n) a</div>

<div>&gt; </div><div>&gt; class VectorRepeat (n :: Nat) where</div><div>&gt;   repeat :: a -&gt; Vector n a</div><div>&gt; </div><div>&gt; instance VectorRepeat Zero where</div><div>&gt;   repeat _ = Nil</div><div>&gt; </div>

<div>&gt; instance VectorRepeat n =&gt; VectorRepeat (Succ n) where</div><div>&gt;   repeat x = Cons x (repeat x)</div></div><div><br></div><div>In this code I have defined a repeat function that works in a similar way to the one in the prelude, except that the length of the resulting vector is determined by the type of the result. I would have hoped that its type would become &#39;repeat :: a -&gt; Vector n a&#39;, yet it is &#39;repeat :: VectorRepeat n =&gt; a -&gt; Vector n a&#39;. As far as I can tell, this class constraint should no longer be necessary, as all possible values for &#39;n&#39; are an instance of this class. I actually really just want to define a closed type-directed function and would rather not (ab)use the type class system at all.</div>

<div><br></div><div>Is there a way to write the repeat function so that it has the type &#39;repeat :: a -&gt; Vector n a&#39; that I&#39;ve missed? If not, is this just because it isn&#39;t implemented or are there conceptual caveats?</div>
<span class="HOEnZb"><font color="#888888">
<div><br></div><div>Paul Visschers</div>
</font></span><br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>