Thanks for all the replies. I guess I'll keep using my type class for now. Paul
On Fri, Oct 26, 2012 at 9:25 AM, Adam Gundry <adam.gun...@strath.ac.uk>wrote: > 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