Judgment Role Notation Generator Breaks Original Syntax

[rappatoni]

MMT-constants can either be called by name or by using a previously specified notation.

In the context of embeddings such as judgements-as-types it is often advantageous to omit arguments that can be inferred by the type checker in the notation so as to render use of the formalization as close to the target formalism as possible. For example, the judgement-operator (usually ded : prop ⟶ type or similar) normally allows to omit the props in inference rules such as ModuPonens: {A:prop,B:prop} ⊦ A ⇒ B ⟶ ⊦ A ⟶ ⊦ B through a notation such as e.g. # MP 3 4. Given α:⊦ A and β:⊦ B this allows the user to write MP α β instead of MP A B α β which is more natural and faithful to the target formalism.

One might want to unburden the user from having to specify these notations manually for every inference rule declaration. For this reason in many formalizations (e.g. LATIN 2) the ded-operator is given a role "Judgment". This role comes with a notation generator: for every function inf_rule that returns a ⊦_ , the notation generator generates a notation # inf_rule %I1 %I2 ... indicating that the prop-arguments in the dependent type operator {...} are left implicit.

However, this comes with a significant downside: the original (and syntactically and semantically correct!) notation inf_rule 1 2 ... is now unusable. This happens unless the user explicitly assigns a notation to inf_rule that overwrites the auto-generated notation.

For users unfamiliar with the Judgment role's workings, this can lead to counterintuitive results as the following code illustrates:

theory judgments : ur:?LF =
prop : type ❙
some: prop ⟶ type ❘ role Judgment❙
other: prop ⟶ type ❙
inconsistent_some: type ❘= {x} some x❙
inconsistent_other: type ❘= {x} other x❙
some_inc : {x} some x ❙
other_inc : {x} other x ❙
inctest_some : inconsistent_some ❘ = some_inc ❙ // Why does this not type-check? ❙
inctest_some_2 : inconsistent_some ❘ = [z:prop] some_inc ❙ //Why does this type-check? ❙
inctest_other : inconsistent_other ❘ = other_inc ❙ // Why then this? ❙
inctest_other_2 : inconsistent_other ❘ = [z:prop] other_inc ❙ // And this not? ❙

❚

As roles are not specified in MMT-surface syntax and there is no way in figuring out what they do without looking at the underlying Scala code. This makes it hard to debug the above code within MMT (the autogenerated notation is shown in the document tree, but it is difficult to figure out that the problem has anything to do with notation in the first place).

Especially in libraries intended for reuse (such as LATIN 2) such obscure features are problematic as they make them much harder to use.

As this behavior of the Judgement role does not appear to be documented at the moment, I will add some lines here.

Beyond that I suggest the following design principle:

Syntactic sugar - especially if autogenerated - should never break the original underlying syntax.

I would suggest that either the notation generator creates a different notation, e.g. inf_rule 1 2 ... => inf_rule_gen 1 2 ...; or better the parser/type-checker disambiguate and allow usage of both the syntactic sugar and the original syntax (@Jazzpirate tells me the latter impossible in the present architecture).

Edit: To give a little bit of context: I ran into this problem when trying to define a logic with two judgement-operators (one for proofs, one for disproofs), trying to build on propositional logic as implemented in LATIN 2. Defeasible logic e.g. has four judgement operators.

[rappatoni]

I updated the documentation here. Would be grateful if somebody could double-check if what I have written is correct.

[florian-rabe]

Explicitly providing the implicit arguments even though a notation is present makes sense in principle. (This is not restricted to the generated notations but applies in general.)
But it has never been important - usually no one wants to give the implicit arguments.

There may be some workaround if it's absolutely needed, e.g., bracketing the rule name or attributing a type. I've never tried those.

[Jazzpirate]

@florian-rabe you're somewhat missing the point. The problem is that the notation generator silently jumps into action and overrides the default notation without a user noticing, and isn't documented, resulting in unexpected failures that are difficult to debug unless one knows exactly what to look for.

There are ways around the implicit arguments if one is aware that the generated notation is the issue, but that's a really big if ;)

[ComFreek]

I got just bitten by this, too. I am not sure whether the notation generator does more good than harm on average 😄

[florian-rabe]

Whatever the drawbacks, LF is unusable for power users without a mechanism like this.

Any remedy would have to focus on remedying the drawbacks (better documentation, make it more optional, ...?).

[Jazzpirate]

I'm guessing there is a distinction between no notation (a: A ❙) and empty notation (a: A ❘ # ❙)? Would me make sense to use the latter to activate the notation generator?

(I strongly suggest that empty notation should activate rather than deactivate, since the main problem is unexpected behavior for people who don't know or think about the notation generator and its behavior - so while easily deactivating it would be an improvement, it doesn't solve the initial problem)

[jfschaefer]

Alternative suggestion: Add a suffix to the generated notation. E.g. for andI : ... introduce the notation andI# or andI'.

That's not much more work for power users and inexperienced users get the expected behaviour.

Also, it might be a nice side-effect that power users still can use the original andI directly.

[ComFreek]

(Florian above:) But it has never been important - usually no one wants to give the implicit arguments.

Lately, I am forced to give more and more implicit arguments since they often cannot be inferred in my use cases.
Would it make sense (worth the time) to report failures of implicit inferrences?

(rappatoni above:) or better the parser/type-checker disambiguate and allow usage of both the syntactic sugar and the original syntax

How would you disambiguate op x y in the context A: type❙ op: A ⟶ A ⟶ A ❘ # 3 ∘ 2❙? It could either refer to the original syntax or to the notation.
In fact, I have seen notations reversing argument order in some MMT archives -- so this case may very well happen. (One could argue that the notation generator will never generate such "contrived" notations. But handling this special casing would complicate everything even more for users.)

@Jazzpirate How about the MMT IntelliJ plugin highlighting notations in a special way? Say we have the term hello (a + world). It's clear that + is a notation, but unclear for alphanumeric strings like hello, a and world. If any of these words refers to a notation, the plugin could highlight it, say in italics. Not sure how much effort this would be.