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

[Richard Eisenberg]

> On May 24, 2017, at 3:13 AM, Anthony Clayden <anthony_clayden at clear.net.nz> wrote:
> 
> Then I guess I remain to be convinced
> of the value of dependent typing within Haskell.

The existing dependently typed languages (I'm thinking of Coq, Adga, and Idris -- just not as familiar with F* and perhaps others) do type inference on a best-effort basis, with very little that I have found in the literature describing the type inference process. One of the major challenges of dependent types in Haskell is to continue Haskell's tradition of predictable, describable type inference. In other words, adding dependent types needn't take anything away from the fragment of Haskell you wish to work in. Indeed, the lack of injectivity for type families is the same kind of problem that exists in those other languages, so Haskell has already paid this price.
> 
> I'd like term-level functions to be more like instances.
> That is, with the equations distributed, see your example
> below.
> (Yes the set of equations must be coherent overall.
> That's something the compiler can check for me.)

I think it depends on the function. Some functions are defined by an ordered set of equations. Some (that is, class methods) are defined by an unordered set of equations, perhaps distributed across modules. Both models are useful.

> 
> There was some doubt whether there could be a type-level
> disequality test.

And indeed this was hard! See "apartness".
> 
>> ... [equality constraints and equality guards are] different, but I think the equality guard is
> useless
> 
> I see two main uses/benefits:
> 1. avoids the need for non-linear patterns in the head

Agreed that it would do this. But why is that important?

> 2. visually points up the 'non-apartness' vs an, um.
> "apartness guard"
> 
> (When I was figuring out Andy A-M's 2013 example,
> I rewrote the non-linear patterns with ~ guards,
> so I could figure out the apartness guards
> esp for the semi-apart instances.
> I posted the later workings to your blog

Somehow, this is more convincing. But I'm still not convinced on this point. Happily, you don't need to convince me -- put in the proposal what you like and then we can debate a concrete design.

>> [except as a type-level "let", I suppose].) 
> 
> No, they're not doing that:
> deliberately I don't allow guards
> to introduce new type vars.

They would work as "let", I think:

> instance Either a a | a ~ SomethingBigAndUgly where ...

Note that the `a` is not introduced in the guard.

> Ok thanks, yes [TypeError] helps.
> Nevertheless it seems disergonomic
> to write an instance for a type-equal case,
> even with a helpful error message;
> when what you want is: no such instance.

You could always view

> instance TypeError ... => C Int Bool

as sugar for

> instance C Int Bool fails

The first declaration isn't so bad, I think, that it warrants introducing new concrete syntax.
> 
> What I can see will be awkward is backwards compatibility:
> can a class/type family with guards
> coexist with CTFs and with classes using overlap?

Sure. There would be no problem with this. The new idea is just that: new. I don't see it as getting rid of anything we already have. Perhaps some day we could think about removing OverlappingInstances, but we certainly don't have to do that at the same time as introducing instance guards. (I do like that name, too.)

> 
>> Next step: write a ghc-proposal. I'll support it. If I had
>> the time, I'd even implement it.
> 
> I'll have a crack at the proposal.

Great. Thanks!

Richard