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

[José Pedro Magalhães]

Hi Paul,

On Thu, Oct 25, 2012 at 4:22 PM, Paul Visschers <mail at 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?
>

There are conceptual caveats; see
http://hackage.haskell.org/trac/ghc/ticket/6074 (particularly the comments).
This would require fundamentally changing the way in which constraints are
elaborated into core code.


Cheers,
Pedro


>
> Paul Visschers
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121025/cc49a548/attachment.htm>