class instances for kinds with finite ty constrs, does this make sense?
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
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
On Thu, Jun 07, 2012 at 07:32:45PM +0100, ex falso wrote:
we always have to put the class restriction (TupleLength l) there, even though all possible type constructors of [*] have a TupleLength instance defined!
Yes, and this is a feature, for at least two reasons. First: to the extent that Haskell's type system corresponds to a logic, it corresponds to a constructive one. Types/propositions are inhabited/proved by explicit terms/evidence. But this request (and [1]) essentially boil down to a desire for double negation elimination: if there *can't* *not* be a certain instance, then the compiler should infer that there *is* one. This seems weird to me (though perhaps I've just drunk too much of the constructivism kool-aid). Second, on a more practical level, the ability to omit class constraints like this would make reasoning about types much more non-local and difficult, since a type like foo :: Bar a -> Baz may or may not implicitly expand to something like foo :: SomeClass a => Bar a -> Baz (which could have important implications for things like inlining, sharing, etc. -- cf the monomorphism restriction), but figuring out whether it does or not requires knowing (a) the definition of Bar and all the instances that are in scope, and (b) whether or not SomeClass's methods ever get called from foo (or anything it calls, recursively). I'd much rather explicitly write the SomeClass constraint if I want it, and be guaranteed that it won't be added if I don't. In summary, these constraints may be "superfluous" in a strictly logical sense, but (a) not in the kind of logic that Haskell uses, and (b) the pain and suffering caused by removing them would far outweigh the tiny bit of typing that would be saved. -Brent [1] http://haskell.1045720.n5.nabble.com/Data-Kinds-and-superfluous-in-my-opinio...
2012/6/8 Brent Yorgey
On Thu, Jun 07, 2012 at 07:32:45PM +0100, ex falso wrote:
we always have to put the class restriction (TupleLength l) there, even though all possible type constructors of [*] have a TupleLength instance defined!
Yes, and this is a feature, for at least two reasons.
First: to the extent that Haskell's type system corresponds to a logic, it corresponds to a constructive one. Types/propositions are inhabited/proved by explicit terms/evidence. But this request (and [1]) essentially boil down to a desire for double negation elimination: if there *can't* *not* be a certain instance, then the compiler should infer that there *is* one. This seems weird to me (though perhaps I've just drunk too much of the constructivism kool-aid).
While I more or less agree with that (still not convinced completely)...
Second, on a more practical level, the ability to omit class constraints like this would make reasoning about types much more non-local and difficult, since a type like
foo :: Bar a -> Baz
may or may not implicitly expand to something like
foo :: SomeClass a => Bar a -> Baz
...this argument is irrelevant in my opinion. You will be forced by GHC type checking to specify which promoted type is an argument. So foo will have type "foo :: Bar (a :: Doh) -> Baz" and constraint will be "SomeClass (a :: Doh)".
(which could have important implications for things like inlining, sharing, etc. -- cf the monomorphism restriction), but figuring out whether it does or not requires knowing (a) the definition of Bar and all the instances that are in scope, and (b) whether or not SomeClass's methods ever get called from foo (or anything it calls, recursively). I'd much rather explicitly write the SomeClass constraint if I want it, and be guaranteed that it won't be added if I don't.
In summary, these constraints may be "superfluous" in a strictly logical sense, but (a) not in the kind of logic that Haskell uses, and (b) the pain and suffering caused by removing them would far outweigh the tiny bit of typing that would be saved.
I would like to suffer that removal. Bring the pain of it! Because right now there's no incentive to drop usual types and use the promoted ones. At least, in the concrete use case of type-level arithmetic (with variables, of course).
-Brent
[1] http://haskell.1045720.n5.nabble.com/Data-Kinds-and-superfluous-in-my-opinio...
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (4)
-
Brent Yorgey -
ex falso -
José Pedro Magalhães -
Serguey Zefirov