Hello Paul, If you don't want to use the class system, you could write `repeat` with a type like this:
repeat :: Proxy n -> a -> Vector n a (`Proxy` is the singleton family 'data Proxy n = Proxy`). You can't really do it with a function of type `a -> Vector n a` because there is no way for the function to know how many elements to generate. 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. 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. 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. I hope this helps, -Iavor On Thu, Oct 25, 2012 at 8:22 AM, Paul Visschers <m...@paulvisschers.net>wrote: > 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 > >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe