[Haskell-cafe] Type-directed functions with data kinds

Paul Visschers mail at paulvisschers.net
Sat Oct 27 10:22:42 CEST 2012

Thanks for all the replies. I guess I'll keep using my type class for now.


On Fri, Oct 26, 2012 at 9:25 AM, Adam Gundry <adam.gundry at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121027/736a0822/attachment.htm>

More information about the Haskell-Cafe mailing list