[Haskell-cafe] Type Instance Partiality [was: [ghc-proposals/cafe] Partially applied type families]

[Anthony Clayden]

> On Mon May 15 16:20:09 UTC 2017, Richard Eisenberg wrote:

> ...

> See my recent draft paper (expanding on the "What are type
families" blog post) here:
>
http://cs.brynmawr.edu/~rae/papers/2017/partiality/partiality.pdf
..
> it's really proposing dropping type families in favor of
functional dependencies
> -- but only for partial type families. ...

Thanks for the paper - hard going for me!

Yes I can see the sense in grounding type family instances
with class instances as Associated Types.

I'm not finding it helpful to bring in Functional
Dependencies. 
Your paper only mentions them towards the end [Related
Work];
 it might be "inspired by" FunDeps, but they don't appear in
the paper as such.

I'm also not finding it helpful to bring in Instance Chains
[despite Garrett's involvement]. 
There's one major attractive feature of Instance Chains that
you kinda mention 
["negations" in Related Work], but which closed classes
can't support. 
I see this as a major weakness of your proposal.


> The key observation is this: partiality in types is
bizarre, and we don't want it. ...

Huh? Nearly all type families (and class instances) are
partial. 
You perhaps mean "don't want it" as purist
type-theoreticians(?) 
As a developer of applications I definitely do want it: 
I want to write instances only for 'sensible' patterns, 
and have the compiler catch usages not supported by declared
instances.

Your examples include many from HList: all of those are
partial. 
I mean there's instances (eliding some details):

> instance HOccurs e (HCons e l')  -- found the element
> instance (HOccurs e l')          -- search the tail
>       => HOccurs e (HCons e' l') -- not this element

There's deliberately not:

> -- instance HOccurs e HNil       -- Fail: not found

Let alone:

> -- instance HOccurs e (Maybe a)  -- not an HList!

Even if we rewrite to DataKinds, GHC has no knowledge that 
there's a closed set of type constructors.

The only type family that usually is total is the type
equality test 
(yielding a type-level Boolean), 
and your Introduction tells me that's problematic. sheesh


> So, any time we use a partial type family,
> you need to have a class constraint around. 
> The class constraint ensures that we evaluate the type
family
> only within its defined domain.

OK. Good.

> Now tied to classes, partial type families are more like
> convenient syntax for functional dependencies.

You perhaps mean the effect achieved by declaring 

> class (F a b ~ c) => C a b c where ...

constraints with Type Families on a class context? 
OK yes that achieves the effect of FunDeps. 
And it's more convenient syntax.


> There is also treatment of partial closed type families
> via a new construct, closed classes
> (somewhat like instance chains but weaker).

As you predicted, I dislike closed classes even more than
closed families. 
Let me explain what feature of Instance Chains you've left
out. 
[Section 3.1.2 "Explicit Failure" of the 2010 paper] 
Sometimes I deliberately want there to be no instance
 for some specific pattern. 
I typically can't achieve that with Overlapping Instances.
So:

* Instance Chains have an explicit `Fail` case. [good]
* HList has an instance with a Fail constraint. [clumsy]
  (I.e. an instance constraint to a class with no instance.
   See HOccursNot with class Fail in the HList paper
   section 6 at "Static look-up")
* Type family instances (currently) don't have constraints,
  so this is hard work to arrange.

IOW what's going on is _deliberately_ a partial type
function.

>
> I expect AntC would prefer disequality guards over closed
classes.

Yes. Because I can 'precision control' which instances are
available. 
Take HOccursNot (validates an HList to make sure
 some element does not occur, typically in combo with
 making sure the list has exactly one occurrence):

> class HOccursNot e l -- no methods! use for constraint
only
> instance HOccursNot e HNil
> -- instance omitted, see below
> instance (HOccursNot e l') 
>       => HOccursNot e (HCons e' l') | e /~ e'  -- guarded

Without disequality guards, the HList paper has to insert 
a bogus overlapping instance for a matched element type:

> instance (Fail (TypeFound e))
        => HOccursNot a (HCons e l')


> ... The big problem with branched instances is that it was
> awkward to describe the overlap between two branched
instances.
> AntC might argue that, if we just had disequality guards,
> it would all be much simpler. He might be right.

This is an important point; we must be careful. 
The rule for instances with guards is: no overlaps! 
(That is, after taking guards into account.) 
That is how "to describe the overlap between two branched
instances": 
there is no overlap. The heads might overlap, but the guards
force them apart.


Any sort of attempt to control overlap can be stymied by
imports. 
A closed set of instances avoids that. 
(I would say at cost of needing to read all preceding
instances
 to understand the conditions for a later instance.)

With guards, I can attach all the conditions to the instance
itself. 
And then compare to each other instance to validate no
overlaps
 -- even for imports.

How would I describe the semantics, within the formalism in
your partiality paper? Section 6.3:

"we use axioms [xi] to witness type family reductions.
 That is, if there is an equation `type F Int = Bool` in
scope,
 then we have an axiom [xi] that proves `F Int ∼
Bool`."

Ok for in scope

> type F a | a /~ Int = Char

we get an axiom:  (F a ~ Char <=> a /~ Int)   --
bi-implication.
[Unashamedly stolen from the CHR work.]
This axiom system is coherent providing there are no other
equations for `F`.

Note also with disequalities we get an inference rule:

  a /~ b, b ~ c ===> a /~ c


AntC