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

[J. Garrett Morris]

Hi Anthony,

This conversation has become deeply mysterious to me.  I understand that
you're revisiting arguments on the structuring of conditionals that were
tried and discarded in the 70s; what I don't understand is why you need
to repeatedly mischaracterize my work to do so.

  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).

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

> 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.

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.

Luckily, both instance chains and closed type families have
formalizations that can be checked to evaluate these claims.  In neither
case do we find either equality limited to ground types or anything that
should be construed as 'look ahead'.  Perhaps you're trying to refer to
the use of infinitary unification in checking apartness (but not in
checking equality) for closed type families?  Here again, not only
is there no use of or need for infinitary unification with instance
chains, but I discussed this difference and its consequences in my 2015
paper.

  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.  The point
of Swierstra's encoding is that you can give a complete definition of
the interpretation of (right-recursive) coproducts, and that doing so is
sufficient to encode extensible variants.  The downside to his approach
is that each new elimination of an extensible variant must itself be
defined via a new type class.  Subsequent work by Bahr, Oliveira et al.,
and myself, has lifted this restriction in various ways.  At no point in
any of these encodings is it in any sense necessary or desirable to
extend existing instances for the coproduct, and so there is no reason
to imagine that using either instance chains or closed type families
would be any obstacle to implementing them.  Again, this is all laid
out, with examples, in my 2015 paper.

  /g