pre-RFC: pretty printer option for numeric literal types

Stream: lean4

[Kyle Miller]

In the Lean 3 community edition, we had the option pp.numeralTypes that would cause numeric literals to pretty print as (2 : Nat) or (2 : Real). This is useful when working with heterogenous operators like ^, since you can see at a glance why a lemma might not apply to a term such as x ^ 2 (is it x ^ (2 : Nat) or x ^ (2 : Real)?)

1. What should the Lean 4 name of the option be? "Numeral" isn't a word used to describe numeric literals, so it might not be discoverable. Some options are pp.numTypes, pp.numLitTypes, and pp.numericTypes.
2. What should be the scope of a "number"? While we could pretty print only @OfNat.ofNat X 2 _ as (2 : X), for clarity we could take a wider notion of "number". Following norm_num, we could have a "number" be a natural number, integer, or rational number literal (a natural number is an OfNat.ofNat literal, an integer is either a natural number or negative of one, and a rational is an integer or a quotient of an integer and a natural). This way, we could see (-2 : Int) and (5/4 : Rat), rather than -(2 : Int) and (5 : Rat) / (4 : Rat).
3. Should raw natural number literals be affected? I'm thinking "no". Perhaps we could have pp.natLit to pretty print them as nat_lit 2.
4. Should the option have more than two settings? A third setting could be to pretty print types for everything but Nat. That way we get (2 : Fin 5) rather than (2 : Fin (5 : Nat)). We rejected this sort of complexity in the community edition, and I'm leaning toward "no" for a first version.
5. The community edition also had a feature where you could mark types with the pp_numeral_type attribute. That way, you could for example do attribute [local pp_numeral_type] Fin to cause Fin literals to print with a type ascription. That way, you get (2 : Fin 5) rather than (2 : Fin (5 : Nat)). This does not need to be part of the RFC however since it can be implemented by users easily enough as a custom delaborator (e.g., it could be implemented in std or mathlib)

[Patrick Massot]

I think all names in 1. are equally discoverable since I will use auto-completion starting with pp.num in all cases. So I would go for the most explicit description pp.numericTypes. 2. I like (-2 : Int) and (5/4 : Rat) (especially the second one). 3. I think I should never see a raw literal, so I like nat_lit 2 that clearly shows the issue. 4. (2 : Fin (5 : Nat)) brings nothing, right? 5. No opinion

[Kyle Miller]

It would be cool if there were a way to detect whether we were pretty printing something that's in a polymorphic context or not. That way we could print Fin 2 rather than Fin (2 : Nat) since the argument to Fin is always Nat. I believe this could be implemented by having the app delaborator set pp.numericTypes to false for such arguments, but this would add complexity for not too much benefit.

[Mac Malone]

I think the best name for (1) depends on how (2) and (5) are resolved. If it is just pretty printing ofNat, a name like pp.numLitTypes makes more sense. If it also doing (2) -- which I think would be wonderful -- then pp.numericTypes sounds better.

[Eric Wieser]

Was this supposed to be handled automatically by pp.analyze?

[Mario Carneiro]

pp.analyze does not use type ascriptions, it would pass implicits if necessary

[Eric Wieser]

pp.ofNat.withType true to match pp.proofs.withType?

[Mac Malone]

@Eric Wieser A wrinkle is that pp.ofNat is not an option that this is modifying unlike with pp.proofs.

[Thomas Murrills]

Maybe it would be simpler to create a generic attribute-based means of deciding when to add type ascriptions. This would allow us to offload the number-specific infrastructure from core to std4 and mathlib4, and also enable it to be extensible to new notions of numbers.

One way to do it would be to have a pp.types group, and then register options in this group. The core functionality would consist of looking for options in this group, checking the extension, and applying whatever functions it found to the data at hand. A possible API might consist of writing something like @[type_ascription numeric] def shouldAnnotate (e eType : Expr) (headAndPriorArgs : Option (Expr × Array Expr)) : DelabM Bool := ...; when pp.types.numeric was true, the core delaborators would pass {the expression at hand, its type, the head of the expression it appeared within (if there was one) and any prior arguments to that head} to shouldAnnotate and any other functions tagged with @[type_ascription numeric]. If any of them returned true, we'd annotate it with the type. (It would do this for all registered options in the pp.types group.)

The implementation in core would be generic and simple, and all of the specific maintenance and design choices could be performed outside of core.

[Thomas Murrills]

(Btw, in this version, I'm imagining that an implementation could use the headAndPriorArgs to detect polymorphism if we wanted to. This would open up type ascriptions in other contexts down the road, like annotating only certain things, e.g. Rings: we could detect if any of the prior args were instances of Ring R, and if eType were R, we could annotate it. Maybe there's a better implementation than passing the head and prior args—not too familiar with what info is available in DelabM—but just wanted to introduce the shape of the idea.)

[Kyle Miller]

One of the features I would like pp.numericTypes to have is that we would see (-2 : Int) and (5 / 4 : Rat), which I don't see this system being able to support.

However, this does point toward a way to implement another feature that I want. The pretty printing for Exists doesn't show binder types, unlike in foralls. The underlying problem is that Exists uses an app_unexpander, and so it relies on binder types being included for funs. If there were a @[pre_delab] attribute that could give "pre-delaborators" a chance to look at an expression and annotate it with pretty printing options (including inserting mdata expressions), then there could be a pre-delaborator that annotates the last argument to Exists with pp.funBinderTypes. This concept of pre-delaborators seems to also be a way to implement your idea.

Something else this could be useful for is to solve the problem that affects overapplied functions that have app_unexpanders, since the pre-delaborator could take f x1 ... xm y1 ... yn and wrap f x1 ... xm in a mdata expression, which would let the app_unexpander see a function with exactly m arguments and then let the standard app delaborator handle the remaining n.

[Kyle Miller]

This has some overlap with pp.analyze, but I'm imagining pre-delaborators to act locally, right before a sub-expression is actually delaborated.

[Kyle Miller]

Mathlib features such as pp_univ could be implemented using pre-delaborators. This delaborator could be one too.

[Thomas Murrills]

Kyle Miller said:

One of the features I would like pp.numericTypes to have is that we would see (-2 : Int) and (5 / 4 : Rat), which I don't see this system being able to support.

Why would it not be able to support this? If we saw an expression like 5 / 4 of type Rat, shouldAnnotate would return true, and we would simply insert a type annotation, right?

[Thomas Murrills]

(Separately, I do like the notion of pre-delaborators inserting mdata, though. :) )

[Eric Wieser]

You also have to not mark the 5 and 4 inside as suitable for annotation

[Thomas Murrills]

That seems doable, I think, seeing as we would have full access to the expression we’re inside via headAndPriorArgs, right? And so we could tell whether we were viewing a natural number inside one of these expressions. (Does the DelabM state tell us about the expression we’re in too? Note that shouldAnnotate lands in DelabM Bool.)

[Kyle Miller]

This is now an RFC: #3021

The pp.numericTypes is like what we discussed here, but I added pp.natLit for pretty printing raw natural number literals with the nat_lit prefix. If pp.natLit is not set, then setting pp.numericTypes enables pp.natLit.

[Eric Wieser]

lean4#3021

[Eric Wieser]

should natLit just be on by default?