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

[Anthony Clayden]

> On Fri Jun 2 13:20:13 UTC 2017, Richard Eisenberg wrote:

> > On Jun 2, 2017, at 3:22 AM, Anthony Clayden wrote: 
> >> I hereby pronounce 
> >>> instance TypeError ... => C Int Bool
> >> 
> >> as "not an instance". ...
> > 
> > Hmm. I'd be interested how you're going to stop
> > the compiler matching some usage site to it.
> 
> That's what TypeError does. When the compiler matches a
> use site, it issues an error. I would imagine that's the
> behavior you want.

No. I want to leave the class open,
so I can add other instances (possibly in a different
module).
If I protect instances in this module with guards,
the compiler can satisfy itself that 
the other modules' instances do not overlap.

> Can you write a concrete example of something you'd like
> to do that the current machinery doesn't? 
> 

OK let's recap the Expression Problem first. There are two
legs:

* We want to freely add methods over a set of datatypes.
  (Problematic in OOP, because
   the methods are embedded in the objects.)
  In Haskell we can declare a new class with new method(s),
  and give instances over those datatypes.
* We want to freely add constructors,
  and expand existing classes/methods to cover.
  That's not so easy in Haskell.
  The usual work-round is to make each constructor a new
datatype.
  Then we can use the instance mechanism to extend
classes/methods.
  ("Usual" for example with DSL's to expand the AST.)

If you have closed type families/classes (esp in an
imported/library module), 
you're blocked from extending it for new datatypes.
Now apparently Instance Chains don't suffer this,
the `fails` triggers a search for other instances in other
chains.
Garrett in an earlier message quoted section 3.1.1 of the
paper
"a class can be populated by multiple, non-overlapping
 instance chains, where each chain may contain multiple
clauses".
Unfortunately I can find no examples of using this feature,
so I'm a bit unsure how it goes.

We'd know the chains are non-overlapping
because they'd chain over distinct datatypes, I imagine.

And I thought that's what we were getting with CTFs,
but the implementation fell short of my expectations.
I wanted (when I suggested the `where`-style syntax):

> module A
>   type family F a b          -- full stop!
>   type instance F (T1 a) b where
>     ...     -- overlapping equations within T1
>
> module B
>   type instance F (T2 c) d where
>     ...    -- overlapping equations within T2

Those closed instances in distinct modules
are provably non-overlapping,
because of the different type constructor.
(By the same rules as currently,
 for apartness of instance heads.
 All equations within the where-group
 must unify with the instance head.)

So then this (current) syntax would be a shorthand:
>   type family G  e f where
>     ...  -- total equations for G

for the author of `G` who deliberately wanted
to prevent anybody expanding the family.
i.e shorthand for

>   type family G e f
>   type instance G e f where
>     ...

Fair enough, that's a common requirement.
But all we got in the implementation
was that blitz-all style. (I'm grumpy.)
And according to Garrett's survey,
15% of Hackage would be grumpy too.

OK, concrete example: within the HList framework

> data HNil = HNil
> data HList e l = HList e l
> -- deliberately not using DataKinds

the Hlist paper discusses various approaches
for indexing the payloads `e` within the list.

Suppose (eliding a lot of detail) I choose Type-Indexed
Products like

> newtype PersonId = PersonId Int
> newtype PersonName = PersonName String
> ...
> me = HCons (PersonId 41) $ HCons (PersonName "AntC") HNil

And type indexed `Has` predicate needing overlaps:

> class Has e l ...
> -- no instance for HNil
> instance Has e (HCons e l) ...
> instance (Has e l') => Has e (HCons e' l') ...

That's standard HList TIP, let's assume it's in a
library/module.

Another style of carrying the payload is type labels.
To mix these styles, I need a way to cons a labelled
element:

> data AstroSign = AstroSign
> ...
> data HConsLab lab e l = HConsLab lab e l
>
> me2 = HConsLab AstroSign 12 me

This deliberately allows the payload to be an ad-hoc type.
Now I need a Has instance:

> instance Has lab (HConsLab lab e l) ...
> instance (Has lab l') => Has lab (HConsLab lab' e' l') ...

Again relies on overlap.
No danger of clashing with the vanilla HCons style,
because labels are a distinct set of types.
IOW this is fine:

> you = HCons (PersonId 73) $ HCons (PersonName "rae")
>           $ HConsLab AstroSIgn 7 HNil
> -- instances for the type of `you`
> --  (Has you PersonId, Has you PersonName, Has you
AstroSign)

I can do all this now with stand-alone instances.
But I have to be careful to keep my overlaps well-behaved.
With closed Type Families/the proposed Classes,
I can't add those HConsLab instances.

I want to continue current support for freely adding
instances,
but provide a mechanism to enforce no-overlaps.
And I think guards achieve that with relatively lightweight
syntax,
avoiding hard-to-follow sequences of `else` ...


AntC