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