Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[ #4560 ] pattern attribute for no-eta-equality inductive records #4611

Closed
wants to merge 3 commits into from
Closed

[ #4560 ] pattern attribute for no-eta-equality inductive records #4611

wants to merge 3 commits into from

Conversation

andreasabel
Copy link
Member

@andreasabel andreasabel commented Apr 19, 2020 •
edited

[ fixed #4560 ] pattern attribute no-eta-equality inductive records.

Having both pattern and copattern matching for records without eta-equality breaks subject reduction.

If you want to pattern match on the constructor for a no-eta record, you have to declare it 'pattern'. The default is copattern matching.

The attribute 'pattern' is ignored for 'coinductive' or 'eta-equality' records. Recursive records might be declared as no-eta by the positivity checker; thus, we need to remember the attribute 'pattern' until the positivity checker has run. It is stored in the new field

  recPatternMatching :: PatternOrCopattern

of the Record alternative of TCM.Defn. Ultimately, the choice of PatternMatching or CopatternMatching is integrated in the field

  recEtaEquality' :: HasEta

This change to Agda affects a dozen test cases and also the standard library at some places.

TODO:

  • fix standard library
  • CHANGELOG
  • documentation

@andreasabel andreasabel added pattern matching Top-level pattern matching definitions, pattern matching in lets eta η-expansion of metavariables and unification modulo η records Record declarations, literals, constructors and updates copatterns Definitions by copattern matching: projections on the LHS labels Apr 19, 2020
@andreasabel andreasabel added this to the 2.6.2 milestone Apr 19, 2020
@andreasabel andreasabel added the status: work-in-progress Do not merge ATM label Apr 19, 2020
@andreasabel andreasabel self-assigned this Apr 19, 2020
@andreasabel andreasabel mentioned this pull request Apr 19, 2020
Closed
@andreasabel
[ fix ] cut-and-paste error in Serialize.Common
97de6dd 
This error seems to have no semantic effect.
@andreasabel
[ refactor for #4560 ] forbid split on codata right away
2501b3f 
The old noPatternMatchingOnCodata was a separate pass after splitting
was done.  We can more eagerly disallow splits on coinductive
constructors.  We do so for other types of disallowed splits already.

This refactoring saves an extra traversal on the internal patterns.

In connection with this refactoring, I split Syntax.Common.DataOrRecord
into its different uses:

1. Syntax.Scope.Base.DataOrRecordModule
2. TypeChecking.DataTypes.DataOrRecord
3. TypeChecking.Rules.LHS.DataOrRecord with extra information
andreasabel added a commit to agda/agda-stdlib that referenced this pull request Apr 20, 2020
@andreasabel
[ agda/agda#4560 ] keyword 'pattern' needed now
00ff208 
The fix of agda/agda#4560 in PR agda/agda#4611 requires the record
directive 'pattern' if you want to pattern match on a record constructor
that does not have eta-equality.  Eta-equality is automatically turned
off for some recursive records, such as the present one.

Alternatively, we could add 'eta-equality' instead of 'pattern'.
andreasabel added a commit to agda/agda-stdlib that referenced this pull request Apr 20, 2020
@andreasabel
[ agda/agda#4560 ] 'eta-equality' or 'pattern' needed now
776b3e0 
The fix of agda/agda#4560 in PR agda/agda#4611 requires the record
directive 'pattern' if you want to pattern match on a record constructor
that does not have eta-equality.  Eta-equality is automatically turned
off for some recursive records, such as the present one.
Here, we turn eta on to be compatible with Agda without the PR.

Alternatively, we could add 'pattern' instead of 'eta-equality'.
@andreasabel andreasabel removed the status: work-in-progress Do not merge ATM label Apr 20, 2020
@andreasabel
[ fixed #4560 ] pattern attribute no-eta-equality inductive records
a5cd3e3 
Having both pattern and copattern matching for records without
eta-equality breaks subject reduction.

If you want to pattern match on the constructor for a no-eta record, you
have to declare it 'pattern'.  The default is copattern matching.

The attribute 'pattern' is ignored for 'coinductive' or 'eta-equality'
records.  Recursive records might be declared as no-eta by the
positivity checker; thus, we need to remember the attribute 'pattern'
until the positivity checker has run.  It is stored in the new field

  recPatternMatching :: PatternOrCopattern

of the Record alternative of TCM.Defn.  Ultimately, the choice of
PatternMatching or CopatternMatching is integrated in the field

  recEtaEquality' :: HasEta

This change to Agda affects a dozen test cases and also the standard
library at one place.  The standard library has been patched to be
compatible with this commit.
@andreasabel andreasabel added language change Changes to the language which can be observed by Agda's userbase record constructors Issues involving record constructors. labels Apr 20, 2020
Saizan
Saizan approved these changes Apr 21, 2020
View reviewed changes
Copy link
Contributor

@Saizan Saizan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would be good to have tests for copatterns being allowed with a no-eta-equality record.

@andreasabel
Copy link
Member Author

Would be good to have tests for copatterns being allowed with a no-eta-equality record.

Such tests already exist, e.g.

agda/test/Succeed/Issue2968.agda

Lines 7 to 30 in c0b4c61

record Category {o h} : Set (lsuc (o ⊔ h)) where
no-eta-equality
constructor con
field
Obj : Set o
Hom : Obj → Obj → Set h
field
id : ∀ {X : Obj} → Hom X X
comp : ∀ {X Y Z} → Hom Y Z → Hom X Y → Hom X Z
id-left : ∀ {X Y} (f : Hom X Y) → comp id f ≡ f
open Category
postulate
isSet : ∀ {l} → (X : Set l) → Set l
hSets : (o : Level) → Category
hSets o .Obj = Σ (Set o) isSet
hSets o .Hom (A , _) (B , _) = A → B
hSets o .id = \ x → x
hSets o .comp f g = \ x → f (g x)
hSets o .id-left f = refl

gallais
gallais approved these changes Apr 21, 2020
View reviewed changes
Copy link
Member

@gallais gallais left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm happy with the design that came out of the discussion!

src/full/Agda/TypeChecking/Monad/Base.hs Show resolved Hide resolved
src/full/Agda/TypeChecking/Serialise/Instances/Common.hs Show resolved Hide resolved
@andreasabel
Copy link
Member Author

Pushed to master.

andreasabel added a commit that referenced this pull request Apr 22, 2020
@andreasabel
[ #4560 ] gallais' suggestions on PR #4611
f8bbd78
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Saizan Saizan Saizan approved these changes

@gallais gallais gallais approved these changes

@nad nad Awaiting requested review from nad

@UlfNorell UlfNorell Awaiting requested review from UlfNorell

@jespercockx jespercockx Awaiting requested review from jespercockx

Assignees

@andreasabel andreasabel

Labels
copatterns Definitions by copattern matching: projections on the LHS eta η-expansion of metavariables and unification modulo η language change Changes to the language which can be observed by Agda's userbase pattern matching Top-level pattern matching definitions, pattern matching in lets record constructors Issues involving record constructors. records Record declarations, literals, constructors and updates
Projects
None yet
Milestone
2.6.2
Development

Successfully merging this pull request may close these issues.

Loss of canonicity with no-eta record and copatterns.
3 participants
@andreasabel @Saizan @gallais