[Haskell-cafe] Type-directed functions with data kinds
Paul Visschers
mail at paulvisschers.net
Thu Oct 25 17:22:24 CEST 2012
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?
Paul Visschers
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121025/4d0c41d9/attachment.htm>
More information about the Haskell-Cafe
mailing list