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