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

[Anthony Clayden]

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

> Lots to respond to!
> 
Thanks Richard, phew! yes.
Let's break it down a bit.

> I do think think there's one overarching question/theme
> here: Do we want functional dependencies or type-level
> functions? Behind AntC's arguments, I see a thrust toward
> functional dependencies. (Not necessarily their *syntax*,
> but the idea of type improvement and flexible -- that is,
> multidirectional -- type-level reasoning.) My dependent
> types work pushes me toward type-level functions.

Yes there is an overarching question.
I don't think it's specifically FunDeps vs Type Functions.
(Although I disagree the **Functional** Dependencies
 are somehow not "functional".
 Yes Mark Jones got the idea from Relational database
theory.
 Where did Ted Codd get the idea from?
 Mathematical (binary) "relations",
 which are a set-theoretic account of, um, functions.)

"Multidirectional type-level reasoning" is what all
functional languages do: from Robinson's unification
to Hindley-Milner to OutsideIn(X)
to System F-subscript-superscript.

There's been an example in Haskell's Prelude
since ~1991: the `read` method's return type
is 'demand-pulled' from context,
not 'supply-pushed' from its parameter.

Similarly if I write:

> x :: Int
> x = a + (b * c)

We infer a, b, c must all be Int.

Perhaps in another universe,
Haskell had explicit type application from day 1, 
and insisted on giving type signatures
for all vars (like nearly all procedural/OO languages).
But we aren't in that universe,
and I love Haskell/FP for being both type-safe
and not pernickety in that way.

> ... [big snip - I'll reply separately]
> 
> I expect AntC would prefer disequality guards 
> over closed classes.

Oh yes! I was about to say (repeating my earlier message):
if we're going to ground type family instances in classes,
then we need a way to distribute type instances
as associated types, unless ...
you're going to suggest something daft like closed classes.
And then you did.


> I would be interested to hear more from the
> community on this choice -- they're really the same as
> ordered equations under the hood, and it's just a choice
> of syntax. Maybe we can even have both.
>

Yes please all chip in. There were strong views expressed
5~8 years ago. My two-penn'orth:

I think we can mechanically translate closed equations
to guards (equality and 'apart' tests).
The example in my earlier post
tried to show how.

For class instances (with overlaps),
I think there's also a mechanical translation,
but only for 'well-behaved' sets of instances.
(For Incoherent sets we don't have a chance.)
And of course as soon as some imported instance overlaps,
we have to start again to assess well-behavedness.

 
> Now, on to individual points:
> 
> ...the Hard Thought in order to be
> backward compatible. (This backward compatibility
> necessity is one of the reasons I love working with
> Haskell. When adding a feature to the language, we just
> can't take easy ways out!)
> 

The backwards-compatibility I particularly
want to preserve is "distributed instances".
That is, putting the instance code
close to type decls and other functions that 
build or consume that type.

I also want to put explicitly *in the instance decl* 
the restraints on what types that instance applies for.
Not implicit from where it appears in a closed
but lengthy/voluminous sequence of equations.

Yes there must be global coherence
for the class/type instances.
That's a mechanical check which compilers are good at,
but humans not so much.


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

I'd argue it's simpler to understand each instance
on its own grounds.
Although a bunch of guards can get quite complex.
(There was Andy A-M's example back in 2013.)
The cumulative effect of the preceeding equations
in the closed family is more complex. IMO.

> 
> In retrospect, it would have been nice to have the
> proposals process active when designing closed type
> families; we might have come up with a better design.
>

There was a huge and rather repetitive (unfortunately)
discussion
in several rounds 2009~2012,
somewhat prompted by trying to 'fix' the Haskell 2010
standard.
So that we could include MPTCs in the standard.
But you can't have MPTCs without FunDeps or Type Families,
or without agreeing a position on overlaps. (good luck with
that!)
So although MPTCs were in both GHC and Hugs before 1998,
they're still not 'official'  >sigh<.

MPTC's omission for Haskell2010 is what I meant by: 
> > we've lost 7~8 years of opportunity.
> 
>  My recollection at the time [of developing closed
Families]
> is that other approaches were
> more functional-dependency-like in character. (To wit:
> instance chains.)

I wish Martin Sulzmann could have been more active at the
time.
(He occasionally expresses the intention of getting back
into Haskell.)
Instance guards are really a continuation of the CHR
approach.
So fit nicely into whole-of-program inference with type
improvement.

[I dislike the non-distributivity of instance chains
 for the same reason I dislike closed families.
 Although instance chains do have some nice features.
 Instance guards give me that feature more directly.
 Whereas closed type families don't give that feature at
all.]

> When I did the closed type family work,
> I was thinking that type families were better than
> functional dependencies; now, my view is much more nuanced
> (leaning strongly toward fundeps instead of partial type
> families).
> 

I'm a little unsure what you mean at the top of the post
about the "idea" of FunDeps vs their specific syntax.
I can simulate FunDeps with superclass constraints
using Type Funs and Equality constraints.
This even achieves multi-directional improvement.
Is that what you want to include?

It took me a long time to realise this works out better
than the FunDeps arrow business, especially with overlaps.
The dreaded "Instances inconsistent with FunDeps" error
is a devil to fiddle with.
And often ends up breaking the coverage condition.
[As Iavor frequently points out.]
Martin pointed out that breaking coverage
(using UndecidableInstances) is not as 'safe'
as SPJ had been assuming.

> 
> > I don't see what's so hard [about non-unifiability].
> 
> It's not nearly as hard from a fundep point of view. ...

> ... [another big snip: thanks for the pointer to the
paper.]

> 
> I do have to say all this talk has made me think more
> about apartness constraints in FC, at least. They might be
> a touch simpler than the current story.
> 

I think apartness is the criterion that's always applied
to resolve instance selection under overlaps.
The trouble is that the semantics for overlap
has never been spelled out.
(Nor, I suspect the criterion for
 a 'well-behaved' set of instances.
 I can volunteer that for you.)
Apartness does not intrude inside
constraints in the class/instance contexts,
nor inside the body of a class instance/methods.
It might help with instance selection
wrt the rhs of type instance equations.


AntC