[ draft ] Refactor Dec to use constructive negation#3065
Conversation
Now that v3.0 is being worked on, I think it is the right time for me to push us to rethink our approach to Dec. Historically Dec was just a datatype with yes/no constructors choosing between A and (¬ A). In agda#929 we entered the era of Reflects and the idea that we could separately compute the Bool telling us the outcome of the decision procedure from the actual proof that comes from its correctness. In this draft, I'd like to shed the commitment to ¬_ in favour of a solution offering constructive notions of negation. This is based on @bobatkey's work: * https://bentnib.org/posts/2023-01-15-datatypes-with-negation.html * https://bentnib.org/posts/2023-11-02-more-data-types-with-negation.html and @jfdm has been porting some of these ideas to Idris. --- The core of the design behind this specific incarnation is that we start by describing what it means for two types to be orthogonal with respect to a (vocabulary influenced by realisability) "pole" P. We say these types are P-orthogonal. A type is always P-orthogonal to its literal negation but there may be more constructive notions of negation e.g. _≤_ is orthogonal to _>_, (A × B) is orthogonal to (¬A ⊎ ¬B), or even (¬A ⊎ (A × ¬B)) if we record the left-biased nature of the decision procedure in the type. The pole idea gives us the ability to decide how strict the orthogonality should be. ⊥-orthogonality is the usual "not both at the same time" whereas ⊤-orthogonality is always trivially true of any pair of types. The orthogonality combinators allow us to build a type of constructive orthogonals to types built out of the standard type constructors. Once we have our orthogonal types, we introduce Choice as the generalisation of Reflects. Choice is a Boolean-indexed decision between two orthogonal types. This covers: 1. the usual strong decidability Dec by having a choice between a type and its negation 2. a variant with constructive negation by simply demanding two ⊥-orthogonal types 3. weak decidability by letting the pole be ⊤ and writing a choice function between A and ⊤
|
Interesting! Let me rephrase the above in slightly less judgmental/prejudicial terms:
|
|
Are there any other values that might get used as the pole in interesting situations? |
|
A typed reduction relation and the progress lemma, perhaps? |
Unfortunately both branches of an |
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
Seems really nice. I'm a huge fan of "positive evidence for negative properties", so I'm sure I would become a user of this kit.
| -- Two types are orthogonal with respect to a pole P when assuming | ||
| -- that both are inhabited leads to a proof of P. | ||
| -- In particular, when the pole is the empty set this amounts to | ||
| -- saying that one is a (more or less constructive) notiong of |
There was a problem hiding this comment.
| -- saying that one is a (more or less constructive) notiong of | |
| -- saying that one is a (more or less constructive) notion of |
| negation A .orthogonal = contradiction | ||
|
|
||
| -- If our notion of orthogonality is with respect to ⊤ then any | ||
| -- two things are related |
There was a problem hiding this comment.
| -- two things are related | |
| -- two things are orthogonal |
| ------------------------------------------------------------------------ | ||
| -- `Choice` idiom. | ||
|
|
||
| -- The choice between A and B is reflected by a boolean value. |
There was a problem hiding this comment.
Your comments are about a version of Choice that does not have P explicit, which contrasts with the code.
|
As a comment, 'tis great to see this PR and happy to comment when/if I can. I have some thoughts and ideas about how constructive negation works in practise for engineering programs with dependent types, and that would be good to share if I ever get the paper finished ;-) |
6 participants
Now that v3.0 is being worked on, I think it is the
right time for me to push us to rethink our approach
to Dec.
Historically Dec was just a datatype with yes/no
constructors choosing between
Aand¬ A.In #929 we entered the era of Reflects and the idea
that we could separately compute the
Booltellingus the outcome of the decision procedure from the
actual proof that comes from its correctness.
In this draft, I'd like to shed the commitment to
¬_in favour of a solution offering constructive notions
of negation.
This is based on @bobatkey's work:
and @jfdm has been porting some of these ideas to Idris.
I am opening this PR so that we can discuss the design
before I push my experiment further.
The core of the design behind this specific incarnation is
that we start by describing what it means for two types
to be orthogonal with respect to a (vocabulary influenced by
realisability) "pole"
P. We say these types areP-orthogonal.A type is always
P-orthogonal to its literal negation butthere may be more constructive notions of negation e.g.
_≤_is orthogonal to_>_,(A × B)is orthogonal to(¬A ⊎ ¬B),or even
(¬A ⊎ (A × ¬B))if we record the left-biased natureof the decision procedure in the type.
The pole idea gives us the ability to decide how strict the
orthogonality should be.
⊥-orthogonality is the usual "notboth at the same time" whereas
⊤-orthogonality is alwaystrivially true of any pair of types.
The orthogonality combinators allow us to build a type of
constructive orthogonals to types built out of the standard
type constructors.
Once we have our orthogonal types, we introduce Choice as
the generalisation of Reflects. Choice is a Boolean-indexed
decision between two orthogonal types.
This covers:
the usual strong decidability
Decby having a choicebetween a type and its negation
a variant with constructive negation by simply demanding
two
⊥-orthogonal typesweak decidability by letting the pole be
⊤and writinga choice function between
Aand⊤