Hi Paul,<br><br><div class="gmail_quote">On Thu, Oct 25, 2012 at 4:22 PM, Paul Visschers <span dir="ltr"><<a href="mailto:mail@paulvisschers.net" target="_blank">mail@paulvisschers.net</a>></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'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>> {-# LANGUAGE DataKinds, GADTs, KindSignatures #-}</div>
<div>> </div><div>> import Prelude hiding (repeat)</div><div>> </div><div>> data Nat = Zero | Succ Nat</div><div>> data Vector (n :: Nat) a where</div><div>> Nil :: Vector Zero a</div><div>> Cons :: a -> Vector n a -> Vector (Succ n) a</div>
<div>> </div><div>> class VectorRepeat (n :: Nat) where</div><div>> repeat :: a -> Vector n a</div><div>> </div><div>> instance VectorRepeat Zero where</div><div>> repeat _ = Nil</div><div>> </div>
<div>> instance VectorRepeat n => VectorRepeat (Succ n) where</div><div>> 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 'repeat :: a -> Vector n a', yet it is 'repeat :: VectorRepeat n => a -> Vector n a'. As far as I can tell, this class constraint should no longer be necessary, as all possible values for 'n' 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 'repeat :: a -> Vector n a' that I've missed? If not, is this just because it isn't implemented or are there conceptual caveats?</div>
</blockquote><div><br>There are conceptual caveats; see <a href="http://hackage.haskell.org/trac/ghc/ticket/6074">http://hackage.haskell.org/trac/ghc/ticket/6074</a> (particularly the comments).<br>This would require fundamentally changing the way in which constraints are elaborated into core code.<br>
<br><br>Cheers,<br>Pedro<br> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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>