Hi Paul, On 25/10/12 16:22, Paul Visschers 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: > [...] > 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?
As Iavor, Andres and Pedro have collectively pointed out, the type forall a (n :: Nat) . a -> Vector n a is uninhabited, because there is no way for the function's runtime behaviour to depend on the value of `n', and hence produce a vector of the correct length. Morally, this function requires a dependent product (Pi-type), rather than an intersection (forall), so we would like to write something like this: repeat :: forall a . pi (n :: Nat) . a -> Vector n a repeat Zero _ = Nil repeat (Succ n) x = Cons x (repeat n x) Notice that Pi-types bind a type variable (like forall) but also allow pattern-matching at the term level. Your `VectorRepeat' type class and Iavor's `SNat' singleton family are both ways of encoding Pi-types, at the cost of duplicated definitions, by linking a term-level witness (the dictionary or singleton data constructor) with a type-level Nat. As you can see, things get a lot neater with proper Pi; unfortunately it is not yet implemented in GHC, and it's probably still a way off. I'm working on a story about adding Pi to System FC, which hopefully might bring it closer. (Shameless plug: for an unprincipled hack that does some of this, check out <https://github.com/adamgundry/inch/>.) Cheers, Adam _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
