Document the meaning of `pattern` without `no-eta-equality` #6066

JasonGross · 2022-08-31T06:06:28Z

The documentation at https://agda.readthedocs.io/en/v2.6.2.2/language/record-types.html?highlight=pattern#recursive-records says:

However, inductive records without η-equality do not support both matching on the record constructor and construction of record elements by copattern matching. It has been discovered that the combination of both leads to loss of subject reduction, i.e., reduction does not preserve typing. For records without η, matching on the record constructor is off by default and construction by copattern matching is on. If you want the converse, you can add the record directive pattern:

As far as I can tell, the documentation does not specify what pattern does when either (or both) of the directives inductive, no-eta-equality are absent, despite the fact that Agda accepts it. I expect this is a no-op (is it?), but I think in any case the behavior should be documented.

The text was updated successfully, but these errors were encountered:

nad · 2022-08-31T10:10:04Z

Perhaps Agda could warn about certain combinations.

andreasabel · 2022-09-30T16:09:31Z

If you explicitly declare eta-equality, you get a warning for pattern:

record D : Set1 where
  eta-equality; pattern; constructor d
  field
    foo : Set

`pattern' attribute ignored for eta record

However, if eta is inferred for the record, you do not get this warning:

record D : Set1 where
  pattern; constructor d
  field
    foo : Set

match : D → Set
match (d A) = A

comatch : Set → D
comatch A .D.foo = A

I suppose we could throw this warning also in the type-checker, after inferring eta-equality for a record type.

andreasabel · 2022-09-30T17:09:38Z

The warning can be thrown when we turn on eta for a record after positivity checking:

agda/src/full/Agda/TypeChecking/Records.hs

Lines 464 to 475 in 7183739

    
           -- | Turn on eta for inductive guarded recursive records. 
        
           --   Projections do not preserve guardedness. 
        
           recursiveRecord :: QName -> TCM () 
        
           recursiveRecord q = do 
        
             ok <- etaEnabled 
        
             modifySignature $ updateDefinition q $ updateTheDef $ \case 
        
               r@Record{ recInduction = ind, recEtaEquality' = eta } -> 
        
                 r { recEtaEquality' = eta' } 
        
                 where 
        
                 eta' | ok, Inferred NoEta{} <- eta, ind /= Just CoInductive = Inferred YesEta 
        
                      | otherwise = eta 
        
               _ -> __IMPOSSIBLE__

agda/src/full/Agda/TypeChecking/Records.hs

Lines 477 to 486 in 7183739

    
           -- | Turn on eta for non-recursive record, unless user declared otherwise. 
        
           nonRecursiveRecord :: QName -> TCM () 
        
           nonRecursiveRecord q = whenM etaEnabled $ do 
        
             -- Do nothing if eta is disabled by option. 
        
             modifySignature $ updateDefinition q $ updateTheDef $ \case 
        
               r@Record{ recInduction = ind, recEtaEquality' = Inferred (NoEta _) } 
        
                 | ind /= Just CoInductive -> 
        
                 r { recEtaEquality' = Inferred YesEta } 
        
               r@Record{} -> r 
        
               _          -> __IMPOSSIBLE__

If my eyes do not deceive me, these two functions do exactly the same!?

They used to be different until e7240e8.

The warning "useless pattern directive" is now extended to records with inferred eta (was only for declared eta). However, to make it correct, we have to remember whether the record constructor was subject to matching before we inferred eta for the record. (Note: the positivity checker runs at the end of the mutual block.) I wonder whether we should rather advice the user to change `pattern` to `eta-equality` in this case. This would also save us the bookkeeping of record constructor matches.

andreasabel · 2022-09-30T19:11:13Z

Ok, there are cases when pattern is needed for records that are later recognized as eta-worthy:

agda/test/Succeed/Issue2308.agda

Lines 13 to 20 in 7183739

    
           mutual -- needed to trigger issue 
        
             record R : Set where  -- needs to be in mutual block 
        
               pattern; constructor wrap 
        
               field f : Unit 
        
             G : R → Set 
        
             G (wrap _) = Unit -- match on wrap needed

This record is classified by Agda as non-recursive.
So we have to keep track of whether pattern has been put to use.

andreasabel · 2022-09-30T19:17:21Z

I am in the process (#6154) of making Agda warn of a redundant pattern directive even when eta for a record is not declared, but inferred. In the case of Issue2308.agda (see above), it is not redundant since eta is inferred to late.

@JasonGross @nad @jespercockx @gallais @UlfNorell : Would you want Agda to recommend to replace pattern by eta-equality in cases like Issue2308.agda where eta is inferred, but too late to enable the match in G? The directive pattern correctly enables pattern matching on the record in the mutual block, but it might also wrongly suggest to the reader that copattern matching isn't available for R---yet which is, after the mutual block when eta has been established.

nad · 2022-10-03T13:24:31Z

I think that the user should declare whether η-equality should hold or not (via the absence or presence of a keyword), I don't think this property should be inferred by Agda.

jespercockx · 2022-10-03T13:33:59Z

"Inferred" is perhaps a strong word here, but I would be fine with there being a simple syntactic rule for when a record has eta-equality. For example, a record has eta-equality unless it has any of the keywords inductive, coinductive, pattern, or no-eta-equality. This is the nicest solution that I can think of that does not break basically all existing Agda code. (If I did not care about breaking existing code at all, I would propose making no-eta-equality the default and only enabling eta when the user requests it explicitly with the eta-equality keyword).

The new implementation separates the query whether an update is necessary from the update. This has to access the signature twice, but skips the update if not needed---rather performing the identity update which produces some garbage that needs to be collected.

andreasabel · 2022-10-05T19:04:58Z

@nad and @jespercockx : Thanks for your opinions. I agree that it would be clearer if eta was not inferred, but declared. I second Jesper's proposal, with some modification:

no directive and inductive default to eta-equality
coinductive and pattern default to no-eta-equality
option --(no-)eta-equality is removed (this might break some code but it is easily fixable)
if eta-equality is not given explicitly but inferred unsafe by the positivity checker, it is switched off with a warning; if it was given explicitly then it is kept with a similar warning unless --safe; with --safe, an error is raised
the pragmas ETA (unsafe) and NOETA are removed

The ETA pragma was kept to allow unsafe eta equality without warning (unless --safe). However, one can also suppress the warning by the usual warning mechanism.

The new implementation separates the query whether an update is necessary from the update. This has to access the signature twice, but skips the update if not needed---rather performing the identity update which produces some garbage that needs to be collected.

nad · 2022-10-06T10:22:56Z

I don't think we should treat things as unsafe only because the type-checker might fail to terminate.

andreasabel · 2022-10-06T21:24:05Z

I don't think we should treat things as unsafe only because the type-checker might fail to terminate.

If I understand Anton @csetzer correctly, eta for coinductive records also breaks subject reduction: https://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedingsCMCS18.pdf

andreasabel added ux: documentation Issues relating to Agda's documentation record constructors Issues involving record constructors. labels Aug 31, 2022

andreasabel added this to the 2.6.3 milestone Sep 1, 2022

andreasabel self-assigned this Sep 30, 2022

andreasabel added the ux: warnings Issues relating to the reporting of warnings label Sep 30, 2022

andreasabel mentioned this issue Sep 30, 2022

Fix #6066: pattern with eta record: document; warn #6154

Closed

andreasabel added the eta η-expansion of metavariables and unification modulo η label Sep 30, 2022

andreasabel added a commit that referenced this issue Oct 5, 2022

Fix #6066: document redundant pattern directives in records

1097d0a

andreasabel mentioned this issue Oct 5, 2022

Fix #6066: documentation for redundant pattern directive in records #6160

Merged

andreasabel closed this as completed in #6160 Oct 6, 2022

andreasabel added a commit that referenced this issue Oct 6, 2022

Fix #6066: document redundant pattern directives in records

3e30dbf

andreasabel mentioned this issue Oct 24, 2022

Release Agda 2.6.3 #6055

Closed

andreasabel changed the title ~~The meaning of pattern without no-eta-equality shoud be documented~~ Document the meaning of pattern without no-eta-equality Oct 24, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Document the meaning of `pattern` without `no-eta-equality` #6066

Document the meaning of `pattern` without `no-eta-equality` #6066

JasonGross commented Aug 31, 2022

nad commented Aug 31, 2022

andreasabel commented Sep 30, 2022

andreasabel commented Sep 30, 2022 •

edited

Loading

andreasabel commented Sep 30, 2022

andreasabel commented Sep 30, 2022 •

edited

Loading

nad commented Oct 3, 2022

jespercockx commented Oct 3, 2022 •

edited

Loading

andreasabel commented Oct 5, 2022

nad commented Oct 6, 2022

andreasabel commented Oct 6, 2022

Document the meaning of pattern without no-eta-equality #6066

Document the meaning of pattern without no-eta-equality #6066

Comments

JasonGross commented Aug 31, 2022

nad commented Aug 31, 2022

andreasabel commented Sep 30, 2022

andreasabel commented Sep 30, 2022 • edited Loading

andreasabel commented Sep 30, 2022

andreasabel commented Sep 30, 2022 • edited Loading

nad commented Oct 3, 2022

jespercockx commented Oct 3, 2022 • edited Loading

andreasabel commented Oct 5, 2022

nad commented Oct 6, 2022

andreasabel commented Oct 6, 2022

Document the meaning of `pattern` without `no-eta-equality` #6066

Document the meaning of `pattern` without `no-eta-equality` #6066

andreasabel commented Sep 30, 2022 •

edited

Loading

andreasabel commented Sep 30, 2022 •

edited

Loading

jespercockx commented Oct 3, 2022 •

edited

Loading