lean
lean copied to clipboard
leanprover-community
feat(frontends/lean/pp): use forall notation for all pi types from a Type to a Prop
This PR makes two modifications to the pretty printer for pi types: (1) if α is a Type and p is a Prop then α → p pretty prints as ∀ (_ : α), p, and (2) non-dependent pi types with non-explicit binders such as Π {x : α}, β pretty print as Π {_ : α}, β, with a special case that instance implicits pretty print as Π [foo α], β rather than Π [_ : foo α], β.
Rationale: Recall that if A : Sort u and B : A → Sort v we have that Π (a : A), B a : Sort (imax u v), and in particular when v is zero then ∀ (a : A), B a : Prop. Currently, when q : Prop then the non-dependent ∀ (a : A), q pretty prints as A → q : Prop. This tends to be surprising when A is a Type, since the implication A → q is a proposition but A is not. By instead pretty printing such a case as ∀ (_ : A), q, then, in addition to reducing surprise, we get strictly more information since we can tell from the_ that this is non-dependent and from the ∀ that A is not a Prop. Since knowing when a pi type is non-dependent is useful, we go ahead and generalize this _ feature to all pi types with non-explicit binders -- the ones with explicit binders already hide the binder name since they pretty print using A → B notation.
I had wondered about this behavior of the pretty printer before, and this Zulip thread led me to check how hard it would be to make the change. If it's unwanted, that's fine.
One one hand, it's an improvement because you can tell immediately whether a pi type with a binding domain in Type is a Prop since it will always show forall notation. On the other you can't immediately tell whether a forall is dependent or not. I think it's still on the balance an improvement that helps align Lean with common practice mathematics at little cost.
To an experienced user, I'd argue being able to spot a non-dependent binder at a glance is more valuable than matching pen and paper mathematics, but I understand the pedagogical appeal.
Do you think using underscores for the variable names in non-dependent binders is a good idea? I think that would remove the downside regarding dependent types.
Do you think using underscores for the variable names in non-dependent binders is a good idea? I think that would remove the downside regarding dependent types.
I like this idea @eric-wieser. I added a mild hack to get this to work -- anonymous names can't round-trip anyway, so I made the binder pp routine print anonymous names as _ rather than [anonymous]. That way the pp_pi function can set the pp_name of a local associated to a non-dependent pi to name() to get it to show up as _. This was the simplest way to get this feature to work that I could think of.
I generalized this to also apply to non-dependent pi types with non-explicit binders. For example, Π {n : ℕ}, ℤ pretty prints as Π {_ : ℕ}, ℤ.