[ new ] explicit polarity annotations by flupe · Pull Request #6385 · agda/agda

flupe · 2022-12-05T10:54:26Z

Joint work from @JorisCeulemans, Malin Altenmüller, @anuyts, @flupe and @jpoiret,
started during the last AIMXXXI. (This draft co-authored by @jpoiret).

This PR introduces explicit polarity annotations, as requested in #570 (and #2411).
It is now possible to specify in function types that a specific variable must be
used strictly-positively (or any other polarity), and this will be enforced during typechecking.

The following (usual) definitions of Mu and Free are now valid:

data Mu (F : @++ Set -> Set) : Set where
  In : F (Mu F) -> Mu F
  
data Free (F : @++ Set -> Set) (@++ A : Set) : Set where
  Pure : A -> Free F A
  Roll : F (Free F A) -> Free F A

For a more complete example, see test/Succeed/PolarityAnnotations.agda.

This PR is purposefully kept minimal, in order to leave the chunk of code to review manageable. The first part of the PR is mostly some bug fixing related to modalities in Agda.

All tests still pass, albeit slightly modified!

Because some modality machinery has been slightly changed, some further testing with actual codebases that use modalities (esp. Cohesion) a lot would ensure that this doesn't break them: we've mostly used tests and simple examples to test until now.

What has been done

A new modal system has been added: polarity. It reuses the Modality abstractions already in place in the code base to handle erasure, cohesion and irrelevance. The possible (endo)modalities for this modal system are @++ (strictly positive), @+ (positive), @- (negative), @mixed (mixed polarity), @unused (parameter is unused). The default polarity for either declarations or binders is @mixed, so that you're able to use them in any way you want.
The typechecker has been modified to account for this new modal system.
In particular, the rule for checking dependent function types divides polarities in the context by @- when checking the domain.
The positivity checker is now aware of the polarity annotations that appear in the types of (datatype and record) parameters (hence why Mu and Free can now be defined).
The (explicit) polarity annotations get priority over what the positivity checker is able to infer.
In particular, some things that the positivity checker could not see as strictly-positive can now be fully annotated, and as long as it typechecks, it can be used as a strictly-positive function later on. (See test/Succeed/PolarityProduct.agda. Without any annotations, the positivity checker alone cannot figure out that n-ary is strictly-positive over X)
The polarity information for a given variable does not contain simply one polarity, but actually 3 polarities:
1. The original polarity assigned to the variable
2. The current polarity of the variable
3. The polarity by which the original one has been divided, i.e the polarity of the context we're in
This was implemented by Joris in order to have more understandable error messages.
Maybe we want to be even more informative about polarity changes, alike the positivity checker's reports, but this is pretty nice already.
Using {-# POLARITY ... #-} on a postulate whose type has already been explicitely annotated with polarities (other than @mixed) will throw an error. We're a bit hesitant to deprecate the POLARITY pragma yet, because it doesn't change the type of the postulate, it merely informs the positivity checker. Until the work on subtyping (see below) has been implemented, it is therefore more flexible than polarity annotations.

Limitations

The internal checker had to be improved a bit, as we have to rely on it to check again the types of constructor arguments with parameters and their assigned polarities in the context. Having to check these twice is a bit unfortunate. But the only way to get access to the telescope of constructors is to first typecheck then reduce, so we don't really have a better solution.
We currently still rely on the positivity checker to decide whether a datatype is strictly-positive.
While it's clear that having @++ List : @++ Set -> Set in the context when checking the types of the arguments of List constructors should be enough to enforce strict-positivity, the situation for mutual datatypes is less clear, see future work below.

Because the semantics of using a polarity modality are still being investigated, we are unsure of the following things and have chosen to either not implement them or specifically forbid them for now:

Splitting on an argument that has a non-mixed polarity: this should be okay if the given argument only has one applicable constructor, with the constructor fields inheriting the annotation. This is probably okay for all modalities as well.
Having non-mixed fields in record types: this should be fine in general for modalities if we're following Modal Type Theory, but we would lose eta-equality or even projections depending on which annotations we choose! In the worst case, they would just because data declarations with one constructor and nothing else.
Annotating indices of datatype declarations with non-mixed polarities: here, we just don't know how that should behave.
So currently we prevent them altogether and throw an error if an annotation was written.
(Therefore indices always get assigned polarity @mixed, as already does the positivity checker)
Subtyping:
Currently we decided to stay away from subtyping to keep things simple. Note that this is also the case for the other modal systems. Figuring out the typing rules
with subtyping is hard. Because of this limitation:
- if you want to use F : @++ Set -> Set where something of type Set -> Set is expected, you'd have to eta-expand manually, as you would for erasure.
- Likewise, people that don't annotate F : Set -> Set can never use it in place of something of type @++ Set -> Set, even if the positivity checker does detect that F is strictly-positive.

To do

Things that may have to be done before merging this PR.

Updating the CHANGELOG. We would appreciate some pointers as to what to write.
Adding a flag to allow the polarity annotations? Add --erased-matches and --erasure #6349 suggests preventing explicit
erasure annotations without --erasure. We may want to do the same for our new annotation. One issue is that polarities can already appear in error messages about modalities, even when they aren't explicitely used.
Updating the user manual.
More tests?

Future work

Refactoring modalities

This will probably be the subject of another issue/PR, but the modal type theorists of the team
seem to think that a refactor of Agda's current handling of modalities is in order,
and would be beneficial in the long term.

Things that could be explored that way would be:

more annotations for record fields;
general rules for splitting on annotated arguments.

Builtin `fmap`

We are now able to define Mu, the least fixed-point of any strictly-positive functor.
However, as of now it is not particularily useful, because you cannot define a generic fold over Mu.
Indeed, to make this possible, you would need fmap readily available for any F : @++ Set -> Set.

We've already discussed this, and think it should be sound to add a new primitive to Agda:

fmap : (F : @++ Set -> Set) -> (A -> B) -> F A -> F B

that internally will have the correct computational behavior and be known to be size-preserving by the
termination checker. It could even be enough to require F positive rather than strictly positive. This would essentially be a directed type theory version of cong combined with directed univalence, so adding that with the proper computational behavior would be quite a feat already.

Typechecking (only) as an alternative to the positivity checker

An interesting direction would be to try and get rid of the positivity checker, and rely solely
on this new polarity modal system and its associated typing rules.

When modifying the positivity-checker to account for our annotations, it became clear that it is
a very intricate beast. There are many edge cases to take care of in its implementation, and any modification can lead to weird bugs. Replacing it with a principled set of typing rules seems like a worthy investigation.

Of course, if we want to stay backwards-compatible (and we do), this means we:

would have to infer the most precise type for every definition i.e have:
```
Id : Set -> Set
Id X = X
```
be inferred to have actual type @++ Set -> Set.

Side note: For this to work, we would need to distinguish between unannotated variables and variables annotated with @mixed so as to run the analysis only for un-annotated variables. Currently there is no distinction.
must have subtyping so that Id : @++ Set -> Set can still be used in place of Set -> Set without requiring manual eta-expansion.
(Users that don't care about annotations shouldn't have to do extra work)
have to figure out the rules when checking a block of mutually-defined datatypes, as discussed above (and the ton of weird datatypes allowed by Agda).
must find a way to not clutter pretty-printing with annotations that the user dit not write but were inferred.

Comments welcome!

jpoiret · 2022-12-05T13:17:51Z

One thing I'm still unsure is whether withVarOcc should be idempotent (a test that's being falsified by quickcheck) when modalities are included in the mix. All the previous modalities were idempotent, but that's not the case here: @- * @- = @+.

plt-amy · 2022-12-05T17:16:55Z

Re. the TODO items:

Updating the CHANGELOG. We would appreciate some pointers as to what to write.

My two cents: Something like "Introduced explicit polarity annotations (user guide link), enabled with the --polarity (or whatever) flag. These allow finer control over the positivity checker by specifying how higher-order parameters use their arguments. For example: [...]" --- with your choice of example.

Yes add a flag, yes add this to the user guide, and please more tests 🙂

I have a question about the actual feature, though, even before looking at the code changes — though I'm not sure my input there will be of any value 😅 Suppose you had something like...

{-# OPTIONS --without-K #-}

data Id {l} {A : Set l} (x : A) : A → Set l where
  refl : Id x x

-- for example:
precast : ∀ {l l'} {A B : Set l} {C : Set l'} → @++ Id A B → (A → C) → (B → C)
precast refl f = f

-- or even generically:
subst : ∀ {l l'} {A : Set l} {B : A → Set l'} {x y : A} → @++ Id x y → B x → B y
subst refl x = x

Is this code modality-correct? No, right? Is that enforced right now?

flupe · 2022-12-05T17:59:01Z

Is this code modality-correct? No, right? Is that enforced right now?

Right now it is forbidden, precisely because we don't know yet what semantics to give to pattern-matching on arguments annotated with polarity != mixed.

The error is the following:

Cannot pattern match against strictly positive argument of type
Id A B
when checking that the pattern refl has type Id A B

We really only know the semantics for annotated variables of type Set, for which pattern-matching is not a concern, but indeed for the rest there is a choice to be made (and careful thinking).

I'll let the modal theorists of the team decide whether this is modality-correct, to my naive eye this is... fine?

As for tests, documentation and changelog, very good, on it, thanks!

jpoiret · 2022-12-05T18:03:07Z

Is this code modality-correct? No, right? Is that enforced right now?

So two things:

This doesn't type-check for now, because we explicitely disallow splitting on non-mixed arguments, which is the case here;
We think it should be ok as long as there is only one constructor. Your example doesn't introduce a "directed" Id type, it just introduces a plain old undirected type, which you then try to use strictly positively, which seems fine to me here. In the future, we could allow the above code.

plt-amy · 2022-12-05T18:19:33Z

Right, I'm okay with having all matching on non-@mixed forbidden for now. The reason I thought the above code would (should) be disallowed is that it desugars to something like

precast p f = transp (λ i → p i → C) i0 f

and the occurrence of p there is.. negative, right?

anuyts · 2022-12-05T18:53:14Z

@plt-amy I think the occurrence of p there is parametric/natural, which I would say is expressed by the @unused polarity (which is not to say that it is erased). One way to see this is that if we have a function h i : p i -> q i for all i, then precast p f : p i1 -> C is heterogeneously equal to precast q g : q i1 - C along h i1 provided that f is heterogeneously equal to g along h i0.

Strict positivity escapes me but for all the other modalities I would be ok to allow pattern matching even for multiple constructors, even for the @unused modality which I read as parametricity/naturality/isovariance and you can pattern match on parametric variables in ParamDTT/RelDTT. But I guess it's a good precaution to forbid it while we don't have a precise model.

An example where positive pattern matching is useful, is when creating covariant functions from Set + Set. Then when we try to be natural w.r.t. such a positive type-level function, we need to pattern match again on an unused variable of type Set + Set.

nad · 2022-12-12T11:35:18Z

The internal checker had to be improved a bit, as we have to rely on it to check again the types of constructor arguments with parameters and their assigned polarities in the context. Having to check these twice is a bit unfortunate. But the only way to get access to the telescope of constructors is to first typecheck then reduce, so we don't really have a better solution.

Is it necessary to check the full type again, or would it suffice to check the polarity annotations? Or could the polarity annotations be checked the first time?

Currently we decided to stay away from subtyping to keep things simple.

Given how much trouble subtyping seems to cause for meta-variable unification I am skeptical towards adding more subtyping to Agda.

Adding a flag to allow the polarity annotations?

I think there should be a flag called something like --polarity.

An interesting direction would be to try and get rid of the positivity checker, and rely solely on this new polarity modal system and its associated typing rules.

Have you thought about how you would handle induction-recursion?

must find a way to not clutter pretty-printing with annotations that the user dit not write but were inferred.

agda/src/full/Agda/Syntax/Common.hs

Lines 619 to 624 in b5105f4

    
           -- | Origin of 'Quantity0'. 
        
           data Q0Origin 
        
             = Q0Inferred       -- ^ User wrote nothing. 
        
             | Q0       Range   -- ^ User wrote "@0". 
        
             | Q0Erased Range   -- ^ User wrote "@erased". 
        
             deriving (Show, Generic, Eq, Ord)

jpoiret · 2022-12-13T20:50:31Z

Is it necessary to check the full type again, or would it suffice to check the polarity annotations? Or could the polarity annotations be checked the first time?

It's not strictly necessary to check the full type, we could also get away with a specialized function that traverses types in the telescope and only checked polarity annotations, however that would probably end up duplicating a lot of code down the line. This approach seems more robust to me, although the internal checker doesn't completely re-check everything, for example the other modalities. Checking the polarity annotations the first time wouldn't really be possible: what we actually want to do is check that the fields of each constructor use the parameters with the proper polarities, but the types of the constructors themselves don't have to respect the polarities of the parameters. Here's an example, and an explanation why:
in

data Ex (@++ A : Set) : Set where
  cons : A → Ex A

A appears to the left of an arrow in the type-signature of cons. That's actually okay, because cons's type signature is (@++ A : Set) → A → Ex A, and in the codomain of the first Π-type we introduce A : Set with mixed annotation, because that's the rule for Π-types.

However, Ex can also be interpreted as Ex = λ (@++ A : Set) → μ (λ _ → A), and when going in the body of the lambda, A this time appears in the context with the @++ annotation. Interpreting datatype declarations using this second method gives a nice intuition IMHO.

All of that wall of text to say that no, we unfortunately need to extract the telescope before being able to type-check.

Given how much trouble subtyping seems to cause for meta-variable unification I am skeptical towards adding more subtyping to Agda.
[..]
I think there should be a flag called something like --polarity.

Right. We'll try to follow what you implemented for erasure on that front.

An interesting direction would be to try and get rid of the positivity checker, and rely solely on this new polarity modal system and its associated typing rules.

Have you thought about how you would handle induction-recursion?

No, not yet. The first roadblock we encountered was for indexed datatypes, for which we don't have a satisfiying answer yet. Induction-recursion is still off the table for now.

must find a way to not clutter pretty-printing with annotations that the user dit not write but were inferred.

agda/src/full/Agda/Syntax/Common.hs

Lines 619 to 624 in b5105f4

-- | Origin of 'Quantity0'.

data Q0Origin

= Q0Inferred -- ^ User wrote nothing.

| Q0 Range -- ^ User wrote "@0".

| Q0Erased Range -- ^ User wrote "@erased".

deriving (Show, Generic, Eq, Ord)

Maybe this could be refactored into a generic solution for all modalities, instead of being specific to quantity. To display better error messages for polarities, we already do something similar where the polarity modality actually carries the original polarity the user specified as well as the currently used polarity. That could also be done for other modalities.

Apart from that, did anyone have a chance at trying out the interface?

nad · 2022-12-14T14:17:20Z

It's not strictly necessary to check the full type, we could also get away with a specialized function that traverses types in the telescope and only checked polarity annotations, however that would probably end up duplicating a lot of code down the line.

What are the performance implications of your choice? If it currently takes a lot of time to type-check a given constructor declaration, does it take twice as much time if your commits are applied? I think constructor declarations rarely take a lot of time to type-check, so perhaps this is not a major problem. However, I think this choice and the performance implications should at least be documented clearly in the source code.

Maybe this could be refactored into a generic solution for all modalities, instead of being specific to quantity.

The Agda source code contains other Origin types as well (search for data.*Origin), that pattern is not only used for modalities.

flupe · 2022-12-14T14:34:17Z

However, I think this choice and the performance implications should at least be documented clearly in the source code.

I definitely agree and we will document it. I also think the impact on performance should be insignificant, but is there any documented way to test this out? Is the Agda CI benchmarking the test suite (or any suite) and tracking performance degradation between versions? How should we go about this, in a more principled manner than just using time locally?

The Agda source code contains other Origin types as well (search for data.*Origin), that pattern is not only used for modalities.

Right, I think Josselin was specifically talking about modalities here. It can become fairly annoying to wrap this information inside every modality constructor, and perhaps if each modality currently implemented has to keep track of where it comes from (inferred or explicitely annotated, and where), maybe it would be good to think about moving this out of constructors for each modality and into a bundle carried along with modality information, or something.

Given how much trouble subtyping seems to cause for meta-variable unification I am skeptical towards adding more subtyping to Agda.

Definitely, which is why we stayed out of it. Although precisely because Agda doesn't have subtyping for function types with modalities, users really don't rip the benefits that using them more often could provide. When you start using them, you have to redefine everything, which can grow tiresome. Perhaps a reliable solution doesn't exist, but it looks like subtyping is the key requirement to make their use practical, for some meaning of practical.

jpoiret · 2022-12-20T13:10:11Z

I just rebased on top of your recent erasure changes @nad. I also added some documentation, although it is pretty terse for now, and fixed some failing tests (among them, all/Succeed/ImportWarnings does not output the warnings in the same order on my machine and on CI, reliably, which is weird).

As for a possible --polarity flag, I'd rather wait until #6350 gets merged, so that we can re-use the same code and not implement it again (I wish GitHub could manage dependent PRs though).

Regarding tracking whether the user had explicitely annotated a variable or not, it could be doable, but I haven't found in practice that polarities show up unless actually used.

doc/user-manual/language/polarity.lagda.rst

jpoiret · 2022-12-21T17:04:30Z

So I'm investigating the test failure of all/LibSucceed/SizeInconsistentMeta4, it has to do with the size solver. The part that is causing an issue now seems to be the additional size constraints introduced by the internal check of the telescope of constructors.

From my limited understanding, that new check introduces new size constraints. If we comment out the rechecking, we get a cluster with

_z_75 =< z : Size
_z_75 =< z : Size
_z_82 =< z : Size
_z_75 =< _z_82 : Size
_z_83 =< z : Size
_z_75 =< _z_83 : Size

and with the rechecking, we get the additional

_z_75 {z = z} {n₁ = n₁} =< z : Size
_z_75 {z = z} {n₁ = n₁} =< z : Size

In the first case, after converting the size constraints to a common context, everything seems fine, but in the second case, _z_82 and _z_83 don't appear anymore, and thus they get set to ∞ by default, causing the error. I don't really know much about the implementation of sized types, but what seems fishy is that the new constraints don't look exactly like the old ones, which could be a deficiency of the internal checker. I'll keep digging but if anyone has any ideas on that front, I would gladly take them.

jespercockx · 2023-01-03T14:58:49Z

Could someone summarize the current state of this PR and make a todo list of what still needs to be done to bring it into a mergable state?

jpoiret · 2023-01-04T18:12:09Z

Could someone summarize the current state of this PR and make a todo list of what still needs to be done to bring it into a mergable state?

Sure, let me try: we should have the basic functionality ready, with the omission of some that we don't have a good justification for, highlighted in the top post.

Here is the state of the todo list, ordered by rough priority:

fix the remaining tests: this is the hard part. I've outlined above some issue I have with the sized types, but I don't understand the implementation of the solver enough to debug what could be wrong, and I'd appreciate some pointers for it. Let's say that the comments around some of the solver functions aren't helping diving into it. I think it's the last failing test, apart from the documentation missing an annotation which I'll fix with the next push.
"hide" the feature behind a flag --polarity, like at Added --erased-matches and --erasure #6350. I was waiting for that PR to get merged to re-use its more generic code. That flag could also control whether we re-check datatype constructors and other expensive operations we might be doing.
add an entry to the changelog. This should be easy enough, unless there are some specific hoops to jump through, but we still need to do it.
update the user manual. There is some preliminary documentation that you can check out at https://agda--6385.org.readthedocs.build/en/6385/language/polarity.html, but it still needs to be expanded upon/clarified a bit more.
add some tests. I think we have enough of them now, with an interesting use-case being one of them (you can check out https://github.com/flupe/agda/blob/polarity-cleaned/test/Succeed/PolarityAnnotations.agda).

jpoiret · 2023-01-09T18:21:54Z

So I think I've completed the above todo list, but some questions remain: by adding the --polarity flag, I also resolved the failing test with sized types because now the re-checking of constructors is only done when the flag is enabled. Still, this means that using sized types with polarities will sometimes cause the size solver to fail, and so it would be better to also understand and fix that error, but it seems to be out of my league.

In other news, I've added an entry to the changelog and updated the manual a bit to clarify and expand on what was there before, as well as mention the new option. I chose not to explain what polarity is in general and assume that the reader already knows, so that might make it a bit unintelligible, feedback welcome.

WDYT?

nad · 2023-01-09T21:21:52Z

Please add the flag --polarity to two lists in the user manual:

agda/doc/user-manual/tools/command-line-options.rst

Lines 1106 to 1108 in 1c5a4e9

    
           An *infective* option is an option that if used in one module, must be 
        
           used in all modules that depend on this module. The following options 
        
           are infective:

agda/doc/user-manual/tools/command-line-options.rst

Lines 1145 to 1147 in 1c5a4e9

    
           Agda records the options used when generating an interface file. If 
        
           any of the following options differ when trying to load the interface 
        
           again, the source file is re-typechecked instead:

nad · 2023-01-09T21:23:48Z

If the problem with sized types is only that some meta-variables get eagerly instantiated to ∞, then I think you can ignore that problem, the size solver is known to be broken in this way.

doc/user-manual/language/polarity.lagda.rst

jpoiret · 2023-01-10T13:31:54Z

Thanks @jespercockx for the review! I realised this morning with @anuyts that we actually have some problems with polarities and modules. The following type-checks:

module _ where

data ⊤ : Set where
  tt : ⊤

module _ (@- A : Set) where
  @- test : Set
  test = A → ⊤

  test2 : Set
  test2 = test → ⊤

We know exactly why this happens, but it'll need some work to fix it. Basically, I wanted to get a minimal version working without changing too much and thus was following the quantity/relevance modalities implementation closely, but some particularities of these modalities let them get away with some lazy checking of definition annotations that we can't mirror. So, the plan is to rather follow the more morally correct cohesion modality. This will require some pretty annoying changes (which I had already done before but stashed somewhere else), such as having different default annotations for binders and for definitions...

Sorry to have wasted your time, although the documentation part will surely not change too much and so the comments will definitely still be applicable!

Co-authored-by: Joris Ceulemans <joris.ceulemans@kuleuven.be>

Co-authored-by: flupe <lucas@escot.me>

We also need to remove a part of a test that relied on a non-normalizable type in a postulate, since we normalize postulate types to get their argument polarities. Co-authored-by: Malin Altenmüller <malin.altenmueller@gmail.com>

This mitigates unwanted performance issues when re-checking constructors of datatypes when polarities are not used at all.

Co-authored-by: flupe <lucas@escot.me>

jespercockx · 2024-12-12T10:22:47Z

I did some interactive rebasing so now the resolution of the import cycle comes before all the other commits in this PR. That way the individual commits should remain buildable (as an early Christmas gift for @andreasabel).

I also added the new warning to the user manual.

flupe · 2024-12-12T17:06:42Z

I added a short explanation on the likely performance impact of running the internal checker when checking constructors with the --polarity flag enabled, as requested by @nad a while ago.

jespercockx · 2024-12-13T12:45:19Z

This (finally) looks like it's in a good enough state to be merged into master. Thank you @flupe and all other people who contributed to this PR!

@nad

…Occurrences The deep-strictness of argOccurrences computed by the positivity checker was lost in PR #6385. (See 32e8c29#r173041607.) On the std-lib-test, the restored strictness is not significant in the workload sharing between Positivity and Polarity, but @nad has an example with a very large mutual block (and thus positivity graph) where it matters.

jpoiret force-pushed the polarity-cleaned branch from 4b5b41c to 63fad8e Compare December 5, 2022 11:01

jespercockx requested a review from andreasabel December 5, 2022 11:02

jpoiret force-pushed the polarity-cleaned branch from 63fad8e to 58907f1 Compare December 5, 2022 13:13

jpoiret force-pushed the polarity-cleaned branch from 58907f1 to 1df02df Compare December 5, 2022 13:38

nad mentioned this pull request Dec 7, 2022

Add --erased-matches and --erasure #6349

Closed

jpoiret mentioned this pull request Dec 9, 2022

Reflection: cannot reduce type because variable is erased #6124

Closed

jpoiret force-pushed the polarity-cleaned branch from 1df02df to 6cbeca4 Compare December 20, 2022 13:05

flupe commented Dec 20, 2022

View reviewed changes

doc/user-manual/language/polarity.lagda.rst Outdated Show resolved Hide resolved

mio-19 mentioned this pull request Dec 26, 2022

Positivity check is incorrectly implemented aya-prover/aya-dev#849

Open

jpoiret force-pushed the polarity-cleaned branch 2 times, most recently from f89d377 to 4eeb2db Compare January 9, 2023 18:16

jespercockx reviewed Jan 10, 2023

View reviewed changes

jpoiret and others added 20 commits December 12, 2024 11:17

Add polarity annotations to interactive use

bf40a4e

Co-authored-by: Joris Ceulemans <joris.ceulemans@kuleuven.be>

Make lambda bindings preserve polarity annotations

af08cdc

Only split on mixed polarity

79f2a49

Co-authored-by: Joris Ceulemans <joris.ceulemans@kuleuven.be>

Check polarity of dom while converting functions

33ce001

Add polarity checking for parameters of data/record types

19cdf1b

Co-authored-by: flupe <lucas@escot.me>

Added error for using polarity pragma with explicit annotations

a047f2c

Prevent polarity annotations on datatype indices

2983056

Forbid non-mixed polarity annotations for record fields

af3e894

Make occurrences from annotations take priority in positivity check

25d9d08

Add --polarity and only re-check constructors if enabled.

58ba058

This mitigates unwanted performance issues when re-checking constructors of datatypes when polarities are not used at all.

Add some polarity tests

f5e99f4

Co-authored-by: flupe <lucas@escot.me>

Add documentation for polarity

38022a9

fix merging of occurrences in addConstant

0942277

Update error messages

645ea51

Add tests to cover all polarity errors

bd04f29

Display polarity when necessary

13b2c86

throw an error warning for toplevel polarity annotations

ccae269

only apply polarity to context when option is enabled

a361280

only fetch occurences in types if polarity option enabled

f99227c

jespercockx force-pushed the polarity-cleaned branch from 0a3ba43 to f99227c Compare December 12, 2024 10:18

Document TopLevelPolarity warning

ace2dcb

add comment on performance for polarity constructor check

20ca4e8

jespercockx merged commit 09188ff into agda:master Dec 13, 2024

nad mentioned this pull request Apr 9, 2025

Polarity annotation ignored by positivity checker? #7795

Closed

andreasabel mentioned this pull request Dec 17, 2025

Separately benchmark Polarity from Positivity; restore forcing of argOccurrences #8292

Merged

Conversation

flupe commented Dec 5, 2022 • edited by jespercockx Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What has been done

Limitations

To do

Future work

Refactoring modalities

Builtin fmap

Typechecking (only) as an alternative to the positivity checker

Uh oh!

jpoiret commented Dec 5, 2022

Uh oh!

plt-amy commented Dec 5, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

flupe commented Dec 5, 2022

Uh oh!

jpoiret commented Dec 5, 2022

Uh oh!

plt-amy commented Dec 5, 2022

Uh oh!

anuyts commented Dec 5, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nad commented Dec 12, 2022

Uh oh!

jpoiret commented Dec 13, 2022

Uh oh!

nad commented Dec 14, 2022

Uh oh!

flupe commented Dec 14, 2022

Uh oh!

jpoiret commented Dec 20, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

jpoiret commented Dec 21, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jespercockx commented Jan 3, 2023

Uh oh!

jpoiret commented Jan 4, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jpoiret commented Jan 9, 2023

Uh oh!

nad commented Jan 9, 2023

Uh oh!

nad commented Jan 9, 2023

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jpoiret commented Jan 10, 2023

Uh oh!

jespercockx commented Dec 12, 2024

Uh oh!

flupe commented Dec 12, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jespercockx commented Dec 13, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

12 participants

flupe commented Dec 5, 2022 •

edited by jespercockx

Loading

Builtin `fmap`

plt-amy commented Dec 5, 2022 •

edited

Loading

anuyts commented Dec 5, 2022 •

edited

Loading

jpoiret commented Dec 20, 2022 •

edited

Loading

jpoiret commented Dec 21, 2022 •

edited

Loading

jpoiret commented Jan 4, 2023 •

edited

Loading

flupe commented Dec 12, 2024 •

edited

Loading