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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

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

AntC
[starting a new thread for this topic]

> On Fri Jun 2 17:35:35 UTC 2017, J. Garrett Morris wrote:

>> On Fri, Jun 2, 2017 at 2:34 PM, Anthony Clayden wrote:

>> else f :<: g fails if f :<: g

>> Haskell very strictly doesn't support instance contexts
>> driving selection of instances.

> Haskell instance selection ...
> if you apply the same restriction to instance chains ...

What was confusing me is that there's a fault
in the instance definitions for the Swierstra encoding
as appears in the 2010 Instance Chains paper.
I see in your 2015 paper that's been fixed.

But before I go on to discuss,
is there a typo in the 2015 paper?
Figure 6 line 6 shows a type family equation

>     IsIn f g     = Yep

That's supposed to mirror the Instance Chains solution
Figure 3 line 6:

> else f `In` g  fails

So Figure 6/line 6's `Yep` should be a `Nope`??

Ok what was the fault in the 2010 paper?

It correctly failed `instance f :<: (f :+: f)`,
because that's ambiguous as to whether the wanted `f`
should match left or right of `:+:`.
But it didn't fail `instance f :<: ((f :+: f) :+: f)`,
because from the failure above,
the left operand of the outer `:+:`, viz `(f :+: f)`,
is not an instance.
So `f :<: ((fail) :+: f)` succeeds.

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

You wrote [on the GCD thread]:
>>>>> Of course, you'll have an easier time of it
>>>>> if you limit yourself to only considering type-level
definitions,
>>>>> and not the corresponding method definitions.
>>>>> But doing so rather misses the point of instance
chains.

It seems to me that in the 2010 paper,
the fault arises from considering only the method
definitions
and failing to pay attention to the type-level.

And yes, I want to make an easy time as possible
for the programmer -- both writing and especially reading
code.

The second approach in the 2015 paper using a case-preparing
Type Family seems to me to cleanly impose a phase
distinction
first type-level calculation
then class instance selection/method overloading.

So my end-game is to be able to remove FunDeps
from the language, in favour of class and instance contexts
giving Type Families with Equality constraints.
(By all means, let's encourage those Type Families
 to be Associated within classes,
 per your Partiality paper with Richard.)

To achieve that we need better support for overlaps.
We need to do that in an understandable way for the
programmer.
That is, the 'umble programmer like me,
not needing an advanced PhD in abstruse type theory.

I think Instance Guards help readability
by putting the instance selection criteria
all in the one place at the instance head;
not reliant on the reader scanning through
a prior chain of instances/elses.

> ... there is no reason to imagine that using
> either instance chains or closed type families
> would be any obstacle to implementing them.
[viz extensible variants/co-products]

No I'm not suggesting any lack of capability.
If anything, Instance Chains are _too_ powerful.
I'm working on showing how the Swierstra encoding
could be catered for in Haskell 2010 + MPTCs+TypeEq.
That is, was achievable in GHC 2004.
(I could do with a few extra milli-Olegs of brain power.)

It's a debate about whether/why/how we introduce
syntactic sugar into current capability
vs introducing a heretofore avoided feature
into type inference viz:
type class membership driving instance selection,
as opposed to currently: types driving instance selection.


AntC
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

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

J. Garrett Morris-5
On Sun, Jun 4, 2017 at 1:00 PM, Anthony Clayden
<[hidden email]> wrote:
> Ok what was the fault in the 2010 paper?

You have reiterated a point that is made at length in §3.2 of my 2015
paper, and §3.4.2 of my dissertation.  I shouldn't, however, have
suggested in 2015 that the deduplicated version is necessarily
preferable.  If you omit the deduplication constraints, you simply end
up with Leijen-style scoped rows [Leijen, TFP05] instead of Rémy-Wand
style rows.  Of course, if, as we did in 2010, you use classes instead
of branching to implement elimination on variants, you have no way to
tell the difference between the two models of variants, and so there's
no reason to prefer one or the other.

> I'm working on showing how the Swierstra encoding
> could be catered for in Haskell 2010 + MPTCs+TypeEq.

You keep talking about guarding instances or equations.  Guards are
equivalent to closed type families, so of course they're sufficient to
implement Swierstra's encoding (following any of Bahr or Oliveira et
al. or my approaches), and will require auxiliary definitions and
indirections that would not be required using instance chains.

This conversation having precisely reattained its starting point, I
don't imagine I could contribute further.

 /g

--
Prosperum ac felix scelus virtus vocatur
 -- Seneca
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

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

AntC
In reply to this post by AntC
> 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
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

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

AntC
In reply to this post by AntC
> On Sun Jun 4 13:11:47 UTC 2017, J. Garrett Morris wrote:

>> On Sun, Jun 4, 2017 at 1:00 PM, Anthony Clayden wrote:
>> ...
> You have reiterated a point that is made at length ...

Good, so we're agreed that the 2010 paper is inconsistent
to reject `(f :+: f)` but accept `((f :+: f) :+: f)`.

> I shouldn't, however, have suggested in 2015 that
> the deduplicated version is necessarily preferable.

I don't follow. The 2015 version is consistent.

>  If you omit the deduplication constraints, you simply end
> up with Leijen-style scoped rows [Leijen, TFP05] ...

Ouch! Its "A novel aspect of this work is that
 records can contain duplicate labels, " is about the most
blood-chilling claim I've seen in the many papers on records
systems.
It is true, though, compared to what you seem to suggest
"effectively introducing a form of scoping over the labels.
"

If `((f :+: g) :+: (h :+: f))` is to be supported,
what's the basis for preferring `f` to the left or right?


> ... Of course, if, as we did in 2010, you use classes
instead
> of branching to implement elimination on variants, you
have no way to
> tell the difference between the two models of variants,
..

Is the only point I was wanting to make:
using a single class fails to separate concerns,
in this example.

>> I'm working on showing how the Swierstra encoding
>> could be catered for in Haskell 2010 + MPTCs+TypeEq.

> You keep talking about guarding instances or equations.
> Guards are equivalent to closed type families,

I think not. They're somewhere between CTFs and Instance
Chains.
In that guarded instances are not closed.
Which also appears to be your claim wrt Instance Chains.

> ... so of course they're sufficient to implement
> Swierstra's encoding (following any of ...),

(I was specifically aiming to implement
 using Haskell as at 2010, but let it pass ...)

Yes any of these approaches are "sufficient".
That's not in debate.

> and will require auxiliary definitions and indirections

Yes, see code I posted subsequent to your message.

> that would not be required using instance chains.

Huh? Your 2015 paper uses auxiliaries class `In`
Figure 3 in the Instance Chains version.

True that the 2010 paper uses no auxiliaries,
but it thereby ends up inconsistent.

What is "wrong" with using auxiliaries?
(Again, in terms of readability.)



AntC
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

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

AntC
In reply to this post by AntC
> > On Sun Jun 4 13:11:47 UTC 2017, J. Garrett Morris wrote:
> > ...
> > You keep talking about guarding instances or equations.
> > Guards are equivalent to closed type families,
>
> I think not. They're somewhere between CTFs and Instance
> Chains.
> In that guarded instances are not closed.
> Which also appears to be your claim wrt Instance Chains.
>

A further difference is wrt class instances and FunDeps.
AFAICT, the closed class instances/Partiality paper
is expecting no FunDeps, but using Assoc types
within the class to achieve the same effect.
I agree with that long-term aim,
so the following applies to both
guarded class instances and guarded type instances.

The dreaded "Instances inconsistent with FunDeps" error
can be boiled down to:

> class TypeEq a b p | a b -> p
> instance TypeEq a a HTrue
> instance TypeEq a b HFalse

The check for FunDep consistency
unifies the class parameters on LHS of FunDep,
yielding subsititution { a ~ b }.
Then applies that substitution to rhs. yielding
{ HTrue ~ HFalse } doesn't hold, so inconsistency.

GHC allows you to put this instead:

> instance TypeEq a a HTrue   -- same
> instance (p ~ HFalse) => TypeEq a b p

The consistency test compares { p ~ HTrue },
and apparently sees those as unifiable,
despite the (~ HFalse) constraint.

There are those [for example, Iavor],
who think this should still count as inconsistent.

So it works (and has consistently since 2004),
but seems iffy.
Furthermore the bare typevar `p` breaks the Coverage
Conditions,
(again despite the (~ HFalse) constraint grr!
So you need UndecidableInstances, which apparently
is not as benign as heretofore thought.

With InstanceGuards it goes like this:

class {-# INSTANCEGUARDS #-} TypeEq a b p | a b -> p
instance TypeEq a a HTrue   -- same
instance TypeEq a b HFalse | a /~ b

Now the consistency check:
unifies the class parameters on lhs of FunDep,
yielding { a ~ b } as before;
then substitutes into the guard,
yielding { a /~ a } -- a contradiction.
So it doesn't need to check the consistency of the result.
Because the 'arguments' to the FunDep are apart.

Notice the side-benefit:
by putting explicit HFalse,
we haven't broken the Coverage Conditions,
so don't need UndecidableInstances.

The guarded type family goes likewise:

> type family {-# INSTANCEGUARDS #-}  Equals a b :: Bool
> type instance Equals a a = True
> type instance Equals a b | a /~ b = False


AntC


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.