[Haskell-cafe] Instance Chains selection by class membership [was: [ghc-proposals/cafe] Partially applied type families]

[Anthony Clayden]

> On Sun Jun 4 12:00:21 UTC 2017, Anthony Clayden wrote:

> I think this shows that using class instances
> to both define methods and drive selection logic
> can fail to separate concerns.

Richard's been (quite correctly) prodding me
to explain why I want a no-instance in places,
rather than an `instance ,,, fails` or
`instance (TypeError ... ) => ...`

I think Figure 7 in Garrett's 2015 paper
provides a case in point.
I find that `type family Ifi` and its call line 5/6 above
to be more like an exercise in obfuscated type-programming.

`type family Into` doesn't observe kind-hygiene
in the way we'd expect a term-level function
to observe type-hygiene.
Type families `Into` or Ifi` might properly return:
* Refl | L lp | R rp    -- that could be a DataKind
   (where `lp` or `rp` is from a recursive call to `Into`)
* or `Nope` -- which is a Boolean DataKind
             (yeuch)

Yes `Into` does need to chase down the data structure
in order to return the correct L/R accessor.
But it doesn't need to also encode failure in that way.

The frustrating thing (for me as reader)
is `type family IsIn` is looking ahead inside the data
structure
to find `f`. Isn't that enough lookahead and error
detection?

I want there to be no equation for `Into` returning `Nope`. 
So I want no Line 7, nor line 10, 13 in `type family Ifi`.

I think I'd tackle it this way.
Instead of `type family IsIn` returning a Boolean,

> type family CountF f g :: Nat where
>   CountF f f           = (S Z)
>   CountF f (g :+: h) = Plus (CountF f g) (CountF f h)
>   CountF f g         = Z

Then for `Into` I'd use a count-preparing helper function,
(instead of `Ifi`) and avoid those `Nope` returns:

> type family Into f g where
>   Into f f       = Refl
>   Into f (g :+: h) = IntoLR f (g :+: h) (CountF f g)
(CountF f h)
>   -- no fail case needed
>
> type family IntoLR f g (cg :: Nat) (ch :: Nat)
> type instance  Into' f (g :+: h) (S Z) Z     = L (Into f
g)
> type instance  Into' f (g :+: h)  Z  (S Z)    = R (Into f
h)
>   -- no fail case needed, no overlap, so not closed

So if the counts return {Z, Z} or {S Z, S Z} or
{S (S (S Z)), S (S (S (S Z)))}, etc,
there's simply no instance for `IntoLR`.

(If you want a helpful error message,
 of course easy enough to add failure instances.)

For completeness, I'll give the Instance Guard
version for `CountF` and `Into`:

> type family {-# INSTANCEGUARD #-} CountF f g :: Nat
> type instance  CountF f f         = (S Z)
> type instance  CountF f (g :+: h) | f /~ (g :+: h)
>                               = Plus (CountF f g) (CountF
f h)
> type instance  CountF f g  | f /~ g, g /~ (_ :+: _)     =
Z

> type family {#- INSTANCEGUARD -#} Into f g
> type instance  Into f f       = Refl
> type instance  Into f (g :+: h) | f /~ (g :+: h)
>                               = IntoLR f (g :+: h) (CountF
f g) (CountF f h)

Those families/instances could be Associated types,
grounded in the class instances (also guarded).

Now I can see my way to translating this into Haskell 2010.

AntC