[Haskell-cafe] [ghc-proposals/cafe] Partially applied type families

[Anthony Clayden]

> On Fri Jun 2 10:26:16 UTC 2017, J. Garrett Morris wrote:

> This conversation has become deeply mysterious to me. 

Hi Garrett, thank you for the opportunity to debate
the ideas in Instance Chains, and correct any 
misunderstandings I might have gained.

The interaction of Overlapping Instances
with other Haskell features has been vexing for a long time.
There have been many approaches.

I find this continuing situation particularly frustrating,
because it seems to me there was an answer in 2002 [1],
whose effectiveness was confirmed by the HList work 2004
[2].

I've been banging this drum for a long time [4].

> I understand that you're revisiting arguments on the
structuring of conditionals ...

No. Until your comment yesterday re Dijkstra (thank you for
the tip),
I was continuing ideas in the Sulzmann and Stuckey
Constraint Handling Rules approach [1].
Although your papers/Dissertation cite some of S&S's work,
you seem unaware of type disequality guards.

I think that's a significant oversight.

> ... that were tried and discarded in the 70s; 

I can see why Dijkstra's ideas might be discarded
for term-level calculation:
* the impossibility of determining whether guards are
mutually exclusive
   (that's a specie of the halting problem)
* the deliberate non-determinacy

But that first objection is not applicable for
instances/guards,
because they have a very simple semantic structure:
pattern-match on the instance head, then type
(dis-)unifiability test.

The second is a definite plus-feature for instance
selection.
(Reflecting how GHC works today.)

So I'm fully up with the programme of the great programmer.

> what I don't understand is why you need
> to repeatedly mischaracterize my work to do so.

If I'm mischaracterising, I apologise.

I note, though, you haven't demurred at my observation
that instance chains need backtracking.
I find backtracking far more unacceptable than
indeterminacy.

>  For one example, I have no idea why you make the
following claim:

>> Nevertheless, I can only write one Instance Chain
>> per class. So I can't (say in another module)
>> introduce a new datatype with instances.

> The instance chains paper is quite explicit in ruling out
this
> interpretation; when introducing the notion of chains, we
wrote:

>    In ilab, a class can be populated by multiple,
non-overlapping
>    instance chains, where each chain may contain multiple
clauses
>    (separated by the keyword else).

Then I apologise. The two chief examples in that paper
(gcd and the Swierstra encoding) both show a final
`else ... fails` branch with a catch-all instance head.
Section 3.2 comments "..., closing the Gcd class."

For the Swierstra encoding in particular, the algorithm
requires the class to be total (it must be closed),
so that the recursive descent test/validation
for go-left/go-right can be determinate.

>  For another, you give a fanciful description of the
problems that
> might arise in implementing instance chains, including:

I reject "fanciful". So I'm going to give citations.

>> There's a persistent problem for the compiler
>> testing for type equality:
>> the usage sites must have the types grounded.
>> It's often more successful to prove disequality.

That's straight out of the HList paper [2],
Section 9 "By chance or by design?".
    "We should point out however groundness issues.
     If TypeEq is to return HTrue, the types must be ground;
     TypeEq can return HFalse even for unground types,
     provided they are instantiated enough to determine
     that they are not equal."

> and also:

>> I suspect that for the compiler,
>> Instance Chains will be as problematic
>> for type inference as with Closed Type Families:
>> CTFs have a lot of searching under the covers
>> to 'look ahead' for equations that can safely match.

That's from Richard, particularly this comment [3].
The whole blog post is relevant here, I think.

> Luckily, both instance chains and closed type families
have
> formalizations that can be checked to evaluate these
claims.

Yes, Overlapping Instances has suffered for too long
from under-/non-formalised semantics.
What I'll be doing for Instance Guards
is giving a translation into Haskell2010 + MPTCs
__without__ overlaps.
(I will need to assume, though, a type-level
 type equality test/total function.
 You've already commented that's easliy produced.)

A serious weakness of Instance Chains, it seems to me,
is it can't be translated to existing Haskell.

>  In neither case do we find either equality limited to
ground types
> or anything that should be construed as 'look ahead'. 

I think the situation has changed with the introduction
of Type Families. They weren't applicable in 2010.
So not relevant to the Instance Chains paper.

"Look ahead" is exactly what Richard is describing
in the bulk of that blog post.
That is, looking down the sequence of instance equations,
to see if any would match and be confluent.
This significantly helps progress in inference.
If Instance Chains aren't going to be doing that,
that's another weakness.

> Perhaps you're trying to refer to the use of
> infinitary unification in checking apartness (but not in
> checking equality) for closed type families?

No, infinitary unification is a whole 'nother
bag of spanners. I am still goggling
at your joint paper with Richard.

> Here again, not only is there no use of or need
> for infinitary unification with instance chains, ...

Good!

> but I discussed this difference and its consequences
> in my 2015 paper.

OK. I've not yet got through that paper.
What I do see in the 2010 paper
 (perhaps this has changed subsequently)
is using typeclass membership
to determine whether a type is a member
of the __same__ class.
This seems to be essential to the Swierstra encoding
such as:

> else f :<: (g :+: h) if f :<: g
> else f :<: (g :+: h) if f :<: h

Gloss: "f is related to (g :+: h), if f is related to g".
And likewise for f related to h.

So:
* this needs look inside the ( :+: ) to see if f is related
to g
   or to h, or to both (fail) or to neither (fail).
   And now you tell me there might be other
   instance chains for `:<:`, so the compiler has to work
through them.
* it breaks down the 'phase distinctions'
  in instance selection. I feel very queazy about a
recursion like that
  at the class level. We can express Russell's paradox:

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

Haskell very strictly doesn't support instance contexts
driving selection of instances.
That is confusing for newbies,
but it's for very good decidability reasons.

>  Finally, you make various claims about what is and is not
a solution
> to the expression problem which have no apparent
relationship to any of
> the existing work on the expression problem or its
encodings. 
> ...  Again, this is all laid out, with examples, in my
2015 paper.

I was being brief. (And this post has gone on plenty long
enough, too.)
I'll come back and debate that point
when I've worked through your 2015 paper.

What's strongly motivating me with Haskell
is getting the type system to cater for extensible/anonymous
records.
(I'm a Relational Theorist by trade.)

Closed instances (be they Chains or Type Families,
 or the proposed Closed Classes)
are just not going to hack it.

Adam G for the Overloaded Records Fields work
has eschewed Type Families in favour of FunDeps.
That's because it needs to create instances 'on the fly'.
Now he hasn't needed overlaps yet (ORF is at an early
stage),
but anonymous/extensible records will.
Just like HList.


AntC


[1] Sulzmann & Stuckey 2002 "A Theory of Overloading",
     esp section 8.2 "Overlapping Definitions"

[2] Kiselyov et al 2004 "Strongly Typed Heterogeneous
Collections"

[3]
https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-families/#comment-131

[4]
https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/DiscussionPage