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>
<div><br></div><div>Paul Visschers</div>