Hi, This has been discussed before: http://haskell.1045720.n5.nabble.com/Data-Kinds-and-superfluous-in-my-opinion-constraints-contexts-td5689436.html
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 <[email protected]> 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
