Constraint implication

Discussion:

Ryan Reich

2017-12-27 07:50:18 UTC

The Constraint kind appears to lack an interface to an important capability
that is already part of the type checker: constraint implication. Namely,
the ability to provide a witness for the statement "constraint c1 implies
constraint c2" or, more importantly, "for all a, constraint (c1 a) implies
constraint (c2 a)", where c1 and c2 are now constraint-valued type
functions (and possibly even for constraint functions with multiple
parameters). It seems to me that this can follow the pattern of the
"magic" Coercible type class and the (non-magic) Coercion data type; it
provides the programmer with an analogous value to this example that can be
obtained in apparently no other way.

Edward Kmett

2017-12-27 19:17:36 UTC

Permalink

Just a few old observations I've made from implementing these things into
type systems of my own:

1.) An internal hom for the category of constraints is admissible:

(|-) :: Constraint -> Constraint -> Constraint

models entailment, and effectively brings into scope a local rule, but
global instance resolution isn't lost if this is only produced from
existing instances.

To your point, this is analogous to the (:-) :: Constraint -> Constraint ->
* external hom for the category of constraints provided by my constraints
package, but it is internal, with all of the appropriate CCC operations.

2.) Quantification over constraints is also admissible.

Neither one compromises the "thinness" of the category of constraints that
provides us global coherence of instance resolution

In this case the property that if D is thin, so is [C,D]. forall here can
quantify over any other kind you want.

Unfortunately, neither implemented in Haskell.

You'd need both of them to be able to talk about constraints like (forall
a. Eq a |- Eq (f a)).

Together could eliminate, morally, the entire Data.Functor.Classes mess.
(That said, as implemented those classes are a bit stronger than the
quantified form)

3.) Constraint also admits a sum type, (\/) but it acts more like a least
upper bound than an either.

It is much easier to talk about in the category of constraints using the
first part above.

Given (p |- r, q |- r), (p \/ q) |- r and vice versa.

The key to keeping the category of constraints thin is that you can't case
analyze on it, its more like if you look at, say, Ord [a] \/ Eq a you can
get to any constraint that you could get to given the intersection of both,
not using the particulars of either. e.g. its morally as powerful as Eq [a]
in this case.

Getting this stuff into GHC is the tricky part!

-Edward

Post by Ryan Reich
The Constraint kind appears to lack an interface to an important
capability that is already part of the type checker: constraint
implication. Namely, the ability to provide a witness for the statement
"constraint c1 implies constraint c2" or, more importantly, "for all a,
constraint (c1 a) implies constraint (c2 a)", where c1 and c2 are now
constraint-valued type functions (and possibly even for constraint
functions with multiple parameters). It seems to me that this can follow
the pattern of the "magic" Coercible type class and the (non-magic)
Coercion data type; it provides the programmer with an analogous value to
this example that can be obtained in apparently no other way.
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

Ryan Reich

2017-12-28 07:44:53 UTC

Permalink

Your 1) is a very erudite way of saying "you forgot about my 'constraints'
package" :) Which I did. Although it's just a little more awkward
syntactically to write `(a :- b) -> whatever` instead of `(a |- b) =>
whatever`, which is only possible with a GHC extension, it obviously solves
the problem of using constraints of the form `c1 implies c2`, i.e. 0-ary
constraint functions. If I understand you correctly, you are saying that
an internal entailment operator is consistent with the other workings of
constraints, and pointing out the concepts that need to be handled in
implementing this in GHC?

Re 2): I am probably missing something when I think that `type (c1 :: * ->
Constraint) ::- (c2 :: * -> Constraint) = forall a. (c1 a :- c2 a)` works
for 1-ary entailment; for instance `Sub Dict :: Ord ::- Eq` appears not to
bother ghci.

3) It would be neat, for sure, to have this sum type. Is that the full
extent of boolean logic you can define on Constraint without losing
thinness?

Post by Edward Kmett
Just a few old observations I've made from implementing these things into
(|-) :: Constraint -> Constraint -> Constraint
models entailment, and effectively brings into scope a local rule, but
global instance resolution isn't lost if this is only produced from
existing instances.
To your point, this is analogous to the (:-) :: Constraint -> Constraint
-> * external hom for the category of constraints provided by my
constraints package, but it is internal, with all of the appropriate CCC
operations.
2.) Quantification over constraints is also admissible.
Neither one compromises the "thinness" of the category of constraints that
provides us global coherence of instance resolution
In this case the property that if D is thin, so is [C,D]. forall here can
quantify over any other kind you want.
Unfortunately, neither implemented in Haskell.
You'd need both of them to be able to talk about constraints like (forall
a. Eq a |- Eq (f a)).
Together could eliminate, morally, the entire Data.Functor.Classes mess.
(That said, as implemented those classes are a bit stronger than the
quantified form)
3.) Constraint also admits a sum type, (\/) but it acts more like a least
upper bound than an either.
It is much easier to talk about in the category of constraints using the
first part above.
Given (p |- r, q |- r), (p \/ q) |- r and vice versa.
The key to keeping the category of constraints thin is that you can't case
analyze on it, its more like if you look at, say, Ord [a] \/ Eq a you can
get to any constraint that you could get to given the intersection of both,
not using the particulars of either. e.g. its morally as powerful as Eq [a]
in this case.
Getting this stuff into GHC is the tricky part!
-Edward

Edward Kmett

2017-12-28 22:19:03 UTC

Permalink

Post by Ryan Reich
Your 1) is a very erudite way of saying "you forgot about my 'constraints'
package" :) Which I did.

Not exactly. The constraints package can construct

(:-) :: Constraint -> Constraint -> *

but

(|-) :: Constraint -> Constraint -> Constraint

would really need compiler support to work correctly. That said, it might
be able to be written as a GHC plugin, now that I think about it. (3) could
also most likely be handled that way.

Post by Ryan Reich
Although it's just a little more awkward syntactically to write `(a :- b)
-> whatever` instead of `(a |- b) => whatever`, which is only possible with
a GHC extension, it obviously solves the problem of using constraints of
the form `c1 implies c2`, i.e. 0-ary constraint functions. If I understand
you correctly, you are saying that an internal entailment operator is
consistent with the other workings of constraints, and pointing out the
concepts that need to be handled in implementing this in GHC?

Yep.

Post by Ryan Reich
Re 2): I am probably missing something when I think that `type (c1 :: * ->
Constraint) ::- (c2 :: * -> Constraint) = forall a. (c1 a :- c2 a)` works
for 1-ary entailment; for instance `Sub Dict :: Ord ::- Eq` appears not to
bother ghci.

data Jet f a = a :- Jet f (f a)

is an example of a data type for which show, (==), compare, etc. are a pain
in the neck to write.

For that you really want something like

instance (Ord a, forall x. Ord x |- Ord (f x)) => Ord (Jet f a)

In the constraints vocabulary today this particular usecase can sort of be
faked by using Lifting:

instance (Lifting Ord f, Ord a) => Ord (Jet f a)

but GHC doesn't know enough to automatically bring the right stuff into
scope to make it automatically work, you have to write a crapload of manual
Lifting instances you might not expect, and you have to open the dictionary
from Lifting by hand, and its generally a mess to use.

3) It would be neat, for sure, to have this sum type. Is that the full

Post by Ryan Reich
extent of boolean logic you can define on Constraint without losing
thinness?

Technically it is a Heyting algebra. You can go a bit crazier with the type
theory for the category of constraints and show that its locally cartesian
closed, which seems to admit some funny interpretations of MLTT in it as
well.

-Edward

Post by Ryan Reich

Post by Edward Kmett
Just a few old observations I've made from implementing these things into
(|-) :: Constraint -> Constraint -> Constraint
models entailment, and effectively brings into scope a local rule, but
global instance resolution isn't lost if this is only produced from
existing instances.
To your point, this is analogous to the (:-) :: Constraint -> Constraint
-> * external hom for the category of constraints provided by my
constraints package, but it is internal, with all of the appropriate CCC
operations.
2.) Quantification over constraints is also admissible.
Neither one compromises the "thinness" of the category of constraints
that provides us global coherence of instance resolution
In this case the property that if D is thin, so is [C,D]. forall here can
quantify over any other kind you want.
Unfortunately, neither implemented in Haskell.
You'd need both of them to be able to talk about constraints like (forall
a. Eq a |- Eq (f a)).
Together could eliminate, morally, the entire Data.Functor.Classes mess.
(That said, as implemented those classes are a bit stronger than the
quantified form)
3.) Constraint also admits a sum type, (\/) but it acts more like a least
upper bound than an either.
It is much easier to talk about in the category of constraints using the
first part above.
Given (p |- r, q |- r), (p \/ q) |- r and vice versa.
The key to keeping the category of constraints thin is that you can't
case analyze on it, its more like if you look at, say, Ord [a] \/ Eq a you
can get to any constraint that you could get to given the intersection of
both, not using the particulars of either. e.g. its morally as powerful as
Eq [a] in this case.
Getting this stuff into GHC is the tricky part!
-Edward

David Feuer

2018-01-02 10:41:28 UTC

Permalink

For whatever it's worth, it seems to me that the two next steps, in no
particular order, should likely be

1. Add quantified contexts. These should obsolete Data.Constraint.Forall by
offering a much nicer API (without needing to use `inst`, etc., manually).

2. Add the ability to at least express constraint implication at the
constraint level, and propagate some of that information automatically.
Trying to be too clever seems to run into backtracking, so it's not clear
that we should try to jump straight to a full constraint implication
system. If we could even get a version that requires manual guidance to use
(like Data.Constraint.Forall does today), we'd surely be making some
progress.

On Jan 2, 2018 5:08 AM, "Simon Peyton Jones via Libraries" <

Post by Edward Kmett
Getting this stuff into GHC is the tricky part!
IndeedâŠ but step 1 is to articulate a well-formed specification. Iâm not
close enough to this conversation to understand all the details, let alone
form a specification. But perhaps some of you are.
I think (2) is described here: https://ghc.haskell.org/trac/
ghc/wiki/QuantifiedContexts. I have been keen on this proposal for
years, just lacking time to execute on it.
Simon
Kmett
*Sent:* 27 December 2017 19:18
*Subject:* Re: Constraint implication
Just a few old observations I've made from implementing these things into
(|-) :: Constraint -> Constraint -> Constraint
models entailment, and effectively brings into scope a local rule, but
global instance resolution isn't lost if this is only produced from
existing instances.
To your point, this is analogous to the (:-) :: Constraint -> Constraint
-> * external hom for the category of constraints provided by my
constraints package, but it is internal, with all of the appropriate CCC
operations.
2.) Quantification over constraints is also admissible.
Neither one compromises the "thinness" of the category of constraints that
provides us global coherence of instance resolution
In this case the property that if D is thin, so is [C,D]. forall here can
quantify over any other kind you want.
Unfortunately, neither implemented in Haskell.
You'd need both of them to be able to talk about constraints like (forall
a. Eq a |- Eq (f a)).
Together could eliminate, morally, the entire Data.Functor.Classes mess.
(That said, as implemented those classes are a bit stronger than the
quantified form)
3.) Constraint also admits a sum type, (\/) but it acts more like a least
upper bound than an either.
It is much easier to talk about in the category of constraints using the
first part above.
Given (p |- r, q |- r), (p \/ q) |- r and vice versa.
The key to keeping the category of constraints thin is that you can't case
analyze on it, its more like if you look at, say, Ord [a] \/ Eq a you can
get to any constraint that you could get to given the intersection of both,
not using the particulars of either. e.g. its morally as powerful as Eq [a]
in this case.
Getting this stuff into GHC is the tricky part!
-Edward
The Constraint kind appears to lack an interface to an important
capability that is already part of the type checker: constraint
implication. Namely, the ability to provide a witness for the statement
"constraint c1 implies constraint c2" or, more importantly, "for all a,
constraint (c1 a) implies constraint (c2 a)", where c1 and c2 are now
constraint-valued type functions (and possibly even for constraint
functions with multiple parameters). It seems to me that this can follow
the pattern of the "magic" Coercible type class and the (non-magic)
Coercion data type; it provides the programmer with an analogous value to
this example that can be obtained in apparently no other way.
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Flibraries&data=04%7C01%7Csimonpj%40microsoft.com%7C8f41822fa9ff4b253ea808d54d5e9adc%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636499991092450873%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwifQ%3D%3D%7C-1&sdata=QquaudC3jd%2FHr33l6N3e0OCRRK8%2F2qhYX7p5m3uSyAc%3D&reserved=0>
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

Andrew Martin

2017-12-28 14:56:24 UTC

Permalink

I agree that this would be cool. Here is some other discussion of this
topic:

- A research paper proving its soundness:
http://i.cs.hku.hk/~bruno/papers/hs2017.pdf
- Responses on reddit:
https://www.reddit.com/r/haskell/comments/6me3sv/quantified_class_constraints_pdf/
- A very dated GHC issue: https://ghc.haskell.org/trac/ghc/ticket/2893

Many people seem to want this, but to my knowledge, no one has any plans to
work on it any time soon. I would not be surprised if it actually ended up
getting implemented one day. It could replace everything in
Data.Functor.Classes as well as half of the stuff from Data.Exists in my
`quantification` package.

--
-Andrew Thaddeus Martin