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

[Anthony Clayden]

> 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:
>> Although your papers/Dissertation cite some of S&S's
work,
>> you seem unaware of type disequality guards.

> Of course we were aware of inequality guards. 
> They are a special case of the observation in §2.3
> of the instance chains paper about unifying
> but non-overlapping instances; §7 of that paper and
§7.1 of my
> dissertation discuss extending the formal treatment
> to accept such instances. 

Then I'm sorry Garrett, but if any of those refs
are intended to be talking about inequality guards,
it's so oblique as to have failed to communicate.

In particular, you fail to mention them
in your dissertation §7.1, first bullet. Example:

"The first challenge is to develop a method to represent
 negative syntactic constraints on types.
 For example, in the following instance chain

> instance C (Maybe t)
> else C t 

"the second clause can only apply to types that are not
 of the form Maybeτ for some type τ.
 To pursue this approach, we would need to develop
 representations and proof rules for such limitations
 on the instantiation of type variables."

I would write that non-Maybe instance as:

> instance C t | t /~ (Maybe _)  -- underscore = anonymous

I guess instance chain:

> else C t fails if t == (Maybe tau)
> -- but that must not introduce typevar `tau` to the
environment.

The S&S CHR approach did "develop proof rules"
to type inequalities (according to the 2002 paper).

An explicit inequality guard makes it easy to test
whether two instances are apart.

> My Hackage survey ("Using Hackage
> to inform language design", Haskell 2010)
> discovered that 85% of overlapping instances were
> contained within the same module, ...

Well of course they are!
Putting overlapping instances in separate modules
is disastrous, everybody knows that.
There's a thorough write-up from SPJ here
https://mail.haskell.org/pipermail/haskell-cafe/2010-July/080043.html

That does not prove people _want_ to restrict the instances
to a single module. They have no choice in practice.

So I'm surprised there's as much as 15% of overlapping
instances
in separate modules. I shudder at the incoherence.

If you surveyed a joinery and found 
everything held together with nails,
that would reflect only that there 
were no screwdrivers on the premisses.

> motivating the formalization of that
> usage pattern with instance chains.

No. I would say (to both Instance Chains
and Closed Type Families/Classes): motivating
to support something less restrictive.
Viz the ability to write stand-alone instances,
that can be verified to not overlap (taking guards into
account),
same approach as the classes in the standard libraries.

(Note how the monad transformers library was re-architected,
 to avoid the dangers of importing overlaps.)


AntC