RFC: Add left actions and right actions to expression tree elaborator and make ^ be a right action

[kmill]

Summary

• Extend the Lean.Elab.Extra expression tree elaborator (which processes binop%, unop%, etc.) with leftact% and rightact%, which are for left actions (operations of the form α → β → β) and right actions (operations of the form α → β → α).
• Switch ^ notation from using binop% to using rightact%.
• Add NatPow and HomogeneousPow classes that provide default Pow instances for the α → Nat → α and α → α → α cases. Add NatPow Nat and HomogeneousPow Float instances.

Motivation

The ^ operator currently uses binop%, which causes the notation to preferentially use a Pow α α instance if it exists. This leads to issues throughout mathlib -- and to repeated questions on Zulip -- because more often one wants x ^ 2 to elaborate using a Pow α Nat instance if it exists rather than using a Pow α α instance. For illustration, if x : Real, then x ^ 2 elaborates with 2 : Real rather than 2 : Nat because (1) there is a Pow Real Real instance and (2) the expression tree elaborator tries to make binop% operations be fully homogeneous.

This is behavior is unwanted because generally there are more theorems about Nat exponents. To use these theorems, one needs to apply coercion lemmas first, and this is not obvious to newer users who might not realize that they need to check exactly how ^ elaborated to make progress. Here's an example using mathlib:

example (x : Real) : x ^ 2 = x * x := by
  -- rw [pow_two] by itself fails since it needs `2 : Nat` to apply
  -- Instead, need to go through some coercions:
  rw [← Nat.cast_ofNat, Real.rpow_nat_cast, pow_two]

Actions

Mathematically speaking, ^ is an example of a right action of Nat on a multiplicative monoid M. That is to say, whenever a type has an associative multiplication operation and a multiplicative unit, it makes sense to define ^ as a function M → Nat → M by the rules a ^ 0 = 1 and a ^ (n + 1) = a ^ n * a, and this action supports nice lemmas such as a ^ (n + m) = a ^ n * a ^ m. The real numbers, though a complicated construction, are incidentally able to support a fully homogeneous ^ operation. However, taking a theorem about an abstract field k and specializing it to Real can lead to it no longer typechecking since ^ for this specific type elaborates differently. While we cannot expect every piece of syntax to support specialization like this, ideally arithmetic operations support it wherever possible as this is a way to help limit user confusion.

While the expression tree elaborator has logic to handle heterogenous instances, it is for heterogenous default instances so another solution is necessary. There are a few reasons for this. First, Pow is already a heterogeneous default instance of HPow, so the logic is not particularly appropriate for this operation. Second, the logic is for default instances for types with constant heads, and we wouldn't want to introduce default instances such as Pow Real Nat as that would cause 3 ^ 2 to elaborate with 3 : Real rather than 3 : Nat. Third, this logic only applies if there's a fully homogenous instance. Rather than finding some hack that would make binop% work in this case, it is easier to implement true support for left and right actions.

Making ^ elaborate with rightact% rather than binop% means that the exponent is free to be of any type, and then default instances can specialize the exponent it if necessary. (For example, mathlib's Pow instance for monoids.)

Having leftact% in addition to rightact% is not just a matter of symmetry. Mathlib's theory of modules over rings is a theory of left actions, and providing it would allow for the SMul notation for module actions to participate in the expression tree elaborator. Here is an example:

variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m : M) (n : N)

#check m + r • n

With the current SMul notation, which does not participate in the expression tree elaborator at all, this elaborates as m + ↑(r • n : ↑N) : M. Making SMul use leftact% allows this to elaborate as m + r • (↑n : M) : M, like other arithmetic expressions. Just as is the case for Pow, sometimes SMul too has fully homogeneous instances, like from the canonical Module R R instance of a ring acting on itself by multiplication, but this is not the preferred instance when working with actions.

Nat and Float elaboration issues

While we want the exponent to not influence types when elaborating an expression tree, there are some considerations to make sure reasonable expressions can elaborate at all.

First, consider Float. In programming applications, an expression tree that uses Float wants everything in sight to be a Float, even exponents, which helps ensure floating-point operations are used rather that, say, repeated multiplication if the exponent is accidentally a natural number. Expressions such as (2.2 ^ 2.2 : Float) ideally would elaborate as well. If we made exponents default to Nat universally, then this would yield a frustrating "failed to synthesize instance OfScientific Nat" error.

Second, consider Nat. In an expression such as ∃ a b, 2 ^ a = b, if we do not have a default instance that can hint that a is a Nat due to the fact that 2 defaults to being a Nat then this would fail to elaborate, so ideally there would be some way to hint in this case that the exponent is a Nat. However, we would not expect ∃ a b, a ^ 2 = b to elaborate because the base of the exponent is unconstrained by the mere fact that the exponent is a Nat (this is consistent with ∃ a b, a * a = b not elaborating), and in fact this elaborating with a Nat base would be problematic as it would conflict with, for instance, mathlib's Pow instance for monoids.

These two ideals seem to be at odds. However, default instances can support a solution for both situations, without introducing regressions. In particular, we can define NatPow and HomogeneousPow classes that implement default instances for Pow, and then by having a NatPow Nat instance and a HomogeneousPow Float instance, both motivating examples elaborate.

Workarounds

Currently, mathlib employs a workaround throughout the library. Many files using ^ turn off the expression tree elaborator completely by adding

local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)

This pairs with the Pow instance for monoids to get the exponent to default to a Nat. The reason for doing this is that it saves inserting convoluted workarounds into expressions to get the binop% operator to elaborate with the wanted type for the exponent. Adding a rightact% elaborator makes it so these workarounds can be removed, resolving #2220.

Manual-level explanation

The elaborator provides binop%, binop_lazy%, leftact%, rightact%, and unop% syntax to mark syntax that should participate in the expression tree elaborator.

At a high level, the elaborator tries to solve for a type that each of the operands in the expression tree can be coerced to, while taking into account the expected type for the entire expression tree. Once this type is computed (and if it exists), it inserts coercions where needed.

Here are brief descriptions of each of the operator types:

• binop% f a b elaborates f a b as a binary operator with two operands a and b, and each operand participates in the protocol.
• binop_lazy% f a b is like binop% but elaborates as f a (fun () => b).
• unop% f a elaborates f a as a unary operator with one operand a, which participates in the protocol.
• leftact% f a b elaborates f a b as a left action (the a operand "acts upon" the b operand). Only b participates in the protocol since a can have an unrelated type, for example scalar multiplication of vectors.
• rightact% f a b elaborates f a b as a right action (the b operand "acts upon" the a operand). Only a participates in the protocol since b can have an unrelated type. This is used by HPow since, for example, there are both Real -> Nat -> Real and Real -> Real -> Real exponentiation functions, and we prefer the former in the case of x ^ 2.
• There are also binrel% and binrel_no_prop% for relations; in particular, these are binary operations where the expected type plays no role in the expression tree elaboration.

The way to cause notation to use the expression tree elaborator is to write a macro for it. Here are some examples from the core library:

macro_rules | `($x + $y)   => `(binop% HAdd.hAdd $x $y)
macro_rules | `($x ^ $y)   => `(rightact% HPow.hPow $x $y)
macro_rules | `(- $x)      => `(unop% Neg.neg $x)

The elaborator assumes that each function is as heterogenous as possible, for example HAdd.hAdd : α → β → γ where HAdd is a three-argument typeclass. Generally, these heterogenous typeclasses have default instances that specialize them to a more homogeneous version.

In the case of HPow, there are three specializations:

class Pow (α : Type u) (β : Type v) where
  pow : α → β → α

class NatPow (α : Type u) where
  pow : α → Nat → α

class HomogeneousPow (α : Type u) where
  pow : α → α → α

Pow provides the default instance associated to how Pow is generally a right action. Both NatPow and HomogeneousPow provide a default Pow instance, and types can choose to implement an instance for one of these two depending on whether they would prefer the exponent to default to being a Nat or to the base's type. There is a NatPow Nat instance and a HomogeneousPow Float instance in the core library.

Reference-level explanation

The expression tree elaborator handles leftact% and rightact% in the following way:

• For leftact% f a b, the term a is a leaf and b is processed as a tree. During type analysis, the algorithm only looks at b's tree. During coercion insertion, coercions are only inserted in b's tree.
• For rightact% f a b, the term a is processed as a tree and b is a leaf. During type analysis, the algorithm only looks at a's tree. During coercion insertion, coercions are only inserted in a's tree.

Drawbacks

• This is a breaking change for how ^ is elaborated, and it impacts libraries such as mathlib due to workarounds they have employed to avoid the way it elaborates. However:

  • std does not need any fixes
  • we commit to fixing issues in mathlib that arise from this change
  • we have NatPow and HomogeneousPow to mitigate regressions that might otherwise result in "normal" Lean use

• Adding the NatPow and HomogeneousPow classes adds more complexity to the arithmetic typeclasses.

• There is a recent issue (explicit ↑ in coercions + infix operators = unfolding timeout #2831) involving timeouts due to interactions between coercion arrows and the expression tree elaborator. Making ^ use leftact% and fixing mathlib causes this issue to become more prominent, but there are workarounds such as using (... :) notation to limit the scope of the expression tree elaborator until this issue is fixed.

• One mathlib use case this fails to support is if the exponent is an integer literal. For example, if G is a group and g : G, it makes sense to write g ^ (-2) for (inv g)^2. However, the NatPow default instance causes -2 to be a Nat and then result in a "failed to synthesize instance Neg Nat" error. There is a workaround, which is to write g ^ (-2 : Int).

Future possibilities

We might want to design a system to allow more general interaction between other syntaxes and the expression tree elaborator. For example, users may be surprised when they find that if/bif statements do not participate:

variable (b : Bool) (x y : Nat)

#check (1 : Int) + bif b then x else y
-- 1 + Int.ofNat (bif b then x else y) : Int

One could imagine that the result should instead be 1 + bif b then Int.ofNat x else Int.ofNat y.

Community Feedback

The leftact% and rightact% additions have been mentioned on Zulip without much discussion. The mathlib community is excited to have a solution to the ^ elaboration issue.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.