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