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

[Anthony Clayden]

> On Mon Jun 5 03:15:32 UTC 2017, Richard Eisenberg wrote:
 
> > On Jun 4, 2017, at 4:06 AM, Anthony Clayden wrote: 

> ... I find these examples are clearest when they
> include code that you want to write, but can't;

Haskellers are a bright bunch.
If there's code they want to write but can't,
they'll find a work-round; bless it as an 'idiom';
publish a couple of papers; and make a virtue out of
necessity.

Looking at the HList library as is today.
It's almost unrecognisable compared to the 2004 paper.
It is in fact using the same techniques,
but they're entirely obscured in work-rounds.
There's no longer overlapping instances
except in one class/in its own module.
viz the type-level type equality test, returning Boolean.

> ... I was expecting an example of how today's
> TypeError doesn't work for you. 

The classic place in HList where TypeError
(used to be) unavoidable is the `Lacks` predicate.
Validate that an HList does _not_ contain element type `e`:

> class HLacks e l
> instance HLacks e HNil
> instance (TypeError e) => HLacks e (HCons e l')
> instance (HLacks e l') => HLacks e (HCons e' l')

The sole purpose of that type-equal/TypeError instance,
is to 'shadow' the type-different instance.
That's nowadays avoidable:

> -- class and HNil instance same
> instance (TypeEq e e' b, HLacksCase b e l')
>       => HLacks e (HCons e' l')  -- catch-all HCons
> class HLacksCase b e l'
> instance (HLacks e l') => HLacksCase False e l'
> instance (TypeError e) => HLacksCase True e l'   -- this
now optional

So every class in the HList library
now has a catch-all HCons instance,
with a call to the type equality test,
and a case-despatching auxiliary class.

It is semantically robust. I suppose you get used to the
idiom.
But in terms of helping type-level programming
look like term-level programming, it's obtuse.

(All that InstanceGuards are aimed at
 is blessing this idiom with some syntax sugar,
 so it looks like term-level guards.)

And HList is working one element at a time,
as it recursively descends into the list.
The TypeError technique doesn't scale.

What I really want to do is use 'flat' tuples
as type-indexed anonymous/extensible records,
putting newtypes to label the payloads:

> me = (PersonId 41, PersonName "AntC")

Again we must prevent repeated types:

> notme = (PersonId 41, PersonName "AntC", PersonId 72)

> class TIPle t -- Type Indexed Product tuples
> instance TIPle (e1, e2)   -- I just want e1 /~ e2, so:
> instance (TypeError e1) => (e1, e1)   -- exclude repeats

This approach doesn't scale. Take the threeple:

> instance (TypeError e1) => TIPle (e1, e1, e3)
> instance (TypeError e1) => TIPle (e1, e2, e1)
> instance (TypeError e2) => TIPle (e1, e2, e2)
> instance TIPle (e1, e2, e3)   -- OK, elements distinct by
elimination

Arguably I should also have
> instance (TypeError e1) => (e1, e1, e1)

The fourple case needs 6, arguably 9 exclusionary instances.

I could use the nowadays HList idiom:

> instance (TypeEq e1 e2 b1, TypeEq e1 e3 b2, TypeEq e2 e3
b3,
>           TIPleCase (b1, b2, b3) (e1, e2, e3) )
>        => TIPle (e1, e2, e3)
> instance TIPleCase (False, False, False) (e1, e2, e3)
> -- TypeError instance(s) optional

Perhaps I could use a type family with (~) constraint

> instance (Equal e1 e2 ~ False, Equal e1 e3 ~ False, Equal
e2 e3 ~ False)
>       => TIPle (e1, e2, e3)

Note I've only talked so far about validating a TIPle,
we want a whole bunch of methods for extending/projecting/
merging and comparing TIPles, 
and the classic record subtype relationship.
With classes over two TIPLes there's a combinatorial
explosion.

So what you do is convert tuples to HLists,
do all the operations on the HList,
convert the result back to tuple.


> > OK, concrete example:
> 
> I'm afraid I don't see the concrete example.
> But it looks like the example you give is one
> motivating instance guards...

It was trying to show:
with CTFs (and presumably closed classes)
there's an explicit or implicit TypeError catch-all instance
at the end of the chain of `else`s.
(It seems InstanceChain `fails` doesn't suffer this.)

So the example showed I _didn't_ want that behaviour.


AntC