[Haskell-cafe] Instance Chains selection by class membership [was: [ghc-proposals/cafe] Partially applied type families]

[Anthony Clayden]

[starting a new thread for this topic]

> On Fri Jun 2 17:35:35 UTC 2017, J. Garrett Morris wrote:

>> On Fri, Jun 2, 2017 at 2:34 PM, Anthony Clayden wrote:

>> else f :<: g fails if f :<: g

>> Haskell very strictly doesn't support instance contexts
>> driving selection of instances.

> Haskell instance selection ...
> if you apply the same restriction to instance chains ...

What was confusing me is that there's a fault
in the instance definitions for the Swierstra encoding
as appears in the 2010 Instance Chains paper.
I see in your 2015 paper that's been fixed.

But before I go on to discuss,
is there a typo in the 2015 paper?
Figure 6 line 6 shows a type family equation

>     IsIn f g     = Yep

That's supposed to mirror the Instance Chains solution
Figure 3 line 6:

> else f `In` g  fails

So Figure 6/line 6's `Yep` should be a `Nope`??

Ok what was the fault in the 2010 paper?

It correctly failed `instance f :<: (f :+: f)`,
because that's ambiguous as to whether the wanted `f`
should match left or right of `:+:`.
But it didn't fail `instance f :<: ((f :+: f) :+: f)`,
because from the failure above,
the left operand of the outer `:+:`, viz `(f :+: f)`,
is not an instance.
So `f :<: ((fail) :+: f)` succeeds.

I think this shows that using class instances
to both define methods and drive selection logic
can fail to separate concerns.

You wrote [on the GCD thread]:
>>>>> Of course, you'll have an easier time of it
>>>>> if you limit yourself to only considering type-level
definitions,
>>>>> and not the corresponding method definitions. 
>>>>> But doing so rather misses the point of instance
chains.

It seems to me that in the 2010 paper,
the fault arises from considering only the method
definitions
and failing to pay attention to the type-level.

And yes, I want to make an easy time as possible
for the programmer -- both writing and especially reading
code.

The second approach in the 2015 paper using a case-preparing
Type Family seems to me to cleanly impose a phase
distinction
first type-level calculation
then class instance selection/method overloading.

So my end-game is to be able to remove FunDeps
from the language, in favour of class and instance contexts 
giving Type Families with Equality constraints.
(By all means, let's encourage those Type Families
 to be Associated within classes,
 per your Partiality paper with Richard.)

To achieve that we need better support for overlaps.
We need to do that in an understandable way for the
programmer.
That is, the 'umble programmer like me,
not needing an advanced PhD in abstruse type theory.

I think Instance Guards help readability
by putting the instance selection criteria
all in the one place at the instance head;
not reliant on the reader scanning through
a prior chain of instances/elses.

> ... there is no reason to imagine that using
> either instance chains or closed type families
> would be any obstacle to implementing them.
[viz extensible variants/co-products]

No I'm not suggesting any lack of capability.
If anything, Instance Chains are _too_ powerful.
I'm working on showing how the Swierstra encoding
could be catered for in Haskell 2010 + MPTCs+TypeEq.
That is, was achievable in GHC 2004.
(I could do with a few extra milli-Olegs of brain power.)

It's a debate about whether/why/how we introduce
syntactic sugar into current capability
vs introducing a heretofore avoided feature
into type inference viz:
type class membership driving instance selection,
as opposed to currently: types driving instance selection.


AntC