Hi, This has been discussed before: http://haskell.1045720.n5.nabble.com/Data-Kinds-and-superfluous-in-my-opinio... Feel free to open a feature request for this. I think it's something we should consider addressing, but at the moment it's not immediately clear how to do it. Cheers, Pedro On Thu, Jun 7, 2012 at 7:32 PM, ex falso <0slemi0@gmail.com> wrote:
Hi, i've been using DataKinds for a while and there seems to be a recurring annoyance that could be possibly eliminated with a language extension. It goes something like this:
data Tuple (l :: [*]) where Unit :: Tuple '[] Comma :: a -> Tuple as -> Tuple (a ': as)
data Proxy k = Proxy
class TupleLength (l :: [*]) where tupleLength :: Proxy l -> Integer instance TupleLength '[] where tupleLength _ = 0 instance (TupleLength as) => TupleLength '(a : as) where tupleLength _ = 1 + tupleLength (Proxy :: Proxy as)
so far so good. but now if we want to use TupleLength:
printLength :: (TupleLength l) => Tuple l -> IO () printLength t = print $ tupleLength t
we always have to put the class restriction (TupleLength l) there, even though all possible type constructors of [*] have a TupleLength instance defined!
If we had a way to signal that all ty constrs are catered for then the compiler could check this, and deduce that l::[*] is always an instance. Well that's the hypothesis. Of course this would only make sense for kinds with finite no. of ty constructors, namely DataKinds-lifted types.
Does this make sense? ex
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe