[Haskell-cafe] class instances for kinds with finite ty constrs, does this make sense?

[Serguey Zefirov]

2012/6/8 Brent Yorgey <byorgey at seas.upenn.edu>:
> 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-opinion-constraints-contexts-td5689436.html
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe