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

[J. Garrett Morris]

On Fri, Jun 2, 2017 at 2:34 PM, Anthony Clayden
<anthony_clayden at clear.net.nz> 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.  My Hackage survey ("Using Hackage to inform language
design", Haskell 2010) discovered that 85% of overlapping instances were
contained within the same module, motivating the formalization of that
usage pattern with instance chains.

> We can express Russell's paradox:
>
>> else f :<: g fails if f :<: g

This is not Russell's paradox, as the lack of set comprehensions in the
near vicinity might have suggested.  At best, it highlights an
incompleteness in the deduction algorithm given in the 2010 paper (from
a ⇒ ¬a, we would hope to conclude ¬a).  But then, I never claimed
completeness.

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

Haskell instance selection is decidable by induction on the number of
type constructors in an entailment; if you apply the same restriction to
instance chains (i.e., that there be more constructors in the conclusion
of an instance than in its hypotheses), you get exactly the same
decidability results.  There are, of course, less restrictive conditions
that would also guarantee decidability, but that is not the point.

 /g

-- 
Prosperum ac felix scelus virtus vocatur
 -- Seneca