[Haskell-cafe] class instances for kinds with finite ty constrs, does this make sense?
0slemi0 at gmail.com
Thu Jun 7 20:32:45 CEST 2012
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
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?
More information about the Haskell-Cafe