Hello everyone, 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: > {-# LANGUAGE DataKinds, GADTs, KindSignatures #-} > > import Prelude hiding (repeat) > > data Nat = Zero | Succ Nat > data Vector (n :: Nat) a where > Nil :: Vector Zero a > Cons :: a -> Vector n a -> Vector (Succ n) a > > class VectorRepeat (n :: Nat) where > repeat :: a -> Vector n a > > instance VectorRepeat Zero where > repeat _ = Nil > > instance VectorRepeat n => VectorRepeat (Succ n) where > repeat x = Cons x (repeat x)
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. 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? Paul Visschers
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe