-
Notifications
You must be signed in to change notification settings - Fork 217
Refactoring structures
We currently flat all inherited fields. For example, given
structure foo :=
(x : nat) (y : nat)
structure boo :=
(x : nat) (z : nat)
structure bla extends foo, boo :=
(w : nat)The structure bla is internally represented as
structure bla :=
(x : nat) (y : nat) (z : nat) (w : nat)We automatically merge "duplicate" fields (e.g., x). Lean will sign an error if the type of duplicate fields do not match.
Remark, the files at library/init/algebra use multiple inheritance in many different places, and there are many duplicate fields.
We also automatically generate the coercions
def bla.to_foo (b : bla) : foo :=
{x := b^.x, y := b^.y}
def bla.to_boo (b : bla) : foo :=
{x := b^.x, z := b^.z}This way of encoding coercions guarantee that given b : bla, b^.x, b^.to_foo^.x and b^.to_boo^.x are all definitionally equal. This would not be the case if we had encoded the coercions as:
def bla.to_foo : bla → foo
| ⟨x, y, z, w⟩ := ⟨x, y⟩
def bla.to_foo : bla → boo
| ⟨x, y, z, w⟩ := ⟨x, z⟩When declaring a structure, we often need to refer to a parent structure. @semorrison makes a heavy use of this feature, and the algebraic hierarchy indirectly uses it to be able to use notation while declaring the structure. For example, we can write
class group (α : Type u) extends monoid α, has_inv α :=
(mul_left_inv : ∀ a : α, a⁻¹ * a = 1)Because group has the parents monoid (which is indirectly an instance of has_mul and has_one) and has_inv. If we try
set_option pp.all true
#check @group.mul_left_invWe have that the reference to parent structure monoid is encoded as
(@monoid.mk α (@group.mul α c) (@group.mul_assoc α c) (@group.one α c)
(@group.one_mul α c) (@group.mul_one α c))The type of group.mul_left_inv is already big, but, in principle, it can be simplified. For example, the
term
(@semigroup.to_has_mul α (@monoid.to_semigroup α
(@monoid.mk α (@group.mul α c) (@group.mul_assoc α c) (@group.one α c)
(@group.one_mul α c) (@group.mul_one α c))))reduces to @has_mul.mul α (@group.mul α c).
This kind of reduction minimizes the performance problem, but does not solve it. In this example, we got a substantial reduction because we were coercing the parent structure to a structure with a single field has_mul.
For an extreme case, we can try
set_option pp.all true
#check @ordered_ring.mkAdvantages:
1- We can use multiple inheritance even if there are duplicate fields.
2- We can rename inherited field names.
3- Projections are fast.
4- The object memory layout is very similar to the memory layout used in programming languages such as C/C++.
Disadvantages:
1- Coercion to the parent structure is slow.
2- There is not cheap way of referring to the parent structure at declaration time.
3- Our structures keep getting bigger and bigger. For example, "single liners" such as
class decidable_linear_ordered_semiring (α : Type u) extends linear_ordered_semiring α, decidable_linear_order αare monstrosities behind the scenes.
We use type based indexed type classes to encode the algebraic hierarchy.
The main problem with this approach is that classes such as semigroup, monoid, comm_semigroup, comm_monoid and group may have many different instances for the same type. Haskell has a similar problem with the Monoid type class. Another problem is that we can construct a monoid using list.append and list.nil, but none of the monoid lemmas can be easily used since they are all stated using the constants mul and one. For example, if we mark the monoid lemmas as [simp], and use the simp tactic, we will not be able to reduce the subterm l ++ [] into l.
Another problem with the current hierarchy is that we have many duplicates (e.g., add_semigroup, add_monoid, etc). We use tactics to reduce the burden of creating these copies, but it still looks like an ugly hack.
The main advantage of this approach is that most lemmas can be viewed as rewriting rules, and we can use a minor variation of first-order matching (e.g., we need to add support for type class resolution).
If we disallow duplicate fields in parent structures, then we can have a more efficient encoding for inheritance. Example:
structure foo :=
(x : nat) (y : nat)
structure boo :=
(w : nat) (z : nat)
structure bla extends foo, boo :=
(bit : bool)The structure bla would be encoded as
structure bla extends foo, boo :=
(foo_parent : foo)
(boo_parent : boo)
(bit : bool)That is, we have field for each parent. Now, coercion to parent structures are very efficient, and we can easily reference parent structures at declaration time. The drawbacks are: parent structures cannot have duplicate fields. We also need to provide the "illusion" to users that bla inherited the fields from foo and boo.
For example, given b : bla, we want to be able to write b^.x, {b with x := 1, bit := ff}.
Tactics such as cases should also provide this illusion. That is, cases b would introduce 5 hypotheses x, y, w, z, bit instead of foo_parent and boo_parent. Field renaming at declaration time would also be disallowed.
As described above, we use multiple inheritance with duplicate fields in many different places at library/init/algebra. Example:
class decidable_linear_ordered_semiring (α : Type u) extends linear_ordered_semiring α, decidable_linear_order αI believe this would be a minor annoyance. First, we can manually show that a decidable_linear_ordered_semiring α is also a decidable_linear_order α. Second, the following modification will also minimize the problem.
We switch to unbundled type classes for all type classes in library/init/algebra/order.lean, library/init/algebra/group.lean, and library/init/algebra/ordered_group.lean.
The idea is to replace type classes such as
class semigroup (α : Type u) extends has_mul α :=
(mul_assoc : ∀ a b c : α, a * b * c = a * (b * c))
class comm_semigroup (α : Type u) extends semigroup α :=
(mul_comm : ∀ a b : α, a * b = b * a)with
class is_semigroup {α : Type u} (op : α -> α -> α) :=
(assoc : ∀ a b c : α, op (op a b) c = op a (op b c))
class is_comm_semigroup (α : Type u) (op : α -> α -> α) extends is_semigroup op :=
(comm : ∀ a b : α, op a b = op b a)That is, we use the operations to index the type classes too.
We are already using two unbundled type classes with some success
https://github.com/leanprover/lean/blob/master/library/init/algebra/classes.lean#L10-L14
They are used by theory_ac.cpp.
They are very convenient to use. Check the tests at tests/lean/run. The AC support in the congruence closure module works for +, *, union, intersection, etc. We just defined the instances and the automation works.
We want to continue this approach in the SMT module, and use it in the arithmetic/algebraic normalizer. The goal is to delete all the little lemmas we have in the algebraic hierarchy, and keep only the ones we need for the automation.
The unbundled approach doesn't work with the simplifier as is.
The problem is that the lemmas are hard to index. For example: the left hand side of the assoc lemma is
(?op (?op ?a ?b) ?c)where ?op, ?a, ?b and ?c are metavariables (aka matching variables). We don't have a single constant that we can use to filter the locations where this lemma can be applied.
We think this is not a big problem, because in the long term, we want to use the algebraic normalizer to apply the lemmas. That is, after we have the arithmetic/algebraic normalizer, we will not need simp lemmas such as mul_assoc and mul_comm. Actually, we may not even need type classes such as semigroup, monoid, etc.
By parametrizing the arithmetic and smt theory modules with unbundled type classes, we will have a very flexible approach. The main drawback is that the simplifier will not be able to use the fully generic lemmas. Another potential problem is performance: theory_ac.cpp generates many type class resolution problems. It generates at least one for every subterm of the form f a b. I'm not sure how expensive it will be. The simplifier also generates a lot of type class resolution problems.
Given a subterm f a b, the algebraic normalizer will have to decide whether the following instances have inhabitants: is_semigroup A f, is_comm_semigroup A f, is_monoid A f _, is_comm_monoid A f _, is_group A f _ _, etc where A is the type of a.
This is a potential performance bottleneck because the algebraic normalizer will have to make these decisions for many subterms. We can cache results (successes and failures). We will potentially have many more failures than successes. We need a mechanism for failing quickly. One idea is to add a new attribute @[algebraic_class], and use to mark algebraic classes such as is_semigroup. Then whenever we add a new instance for one of the algebraic classes, we record in a set S all constants (and local constants) occurring as parameters. Now, if the head symbol of f is not in the set S we don't even try to synthesize the type classes is_semigroup A f, is_comm_semigroup A f, ... This trick is similar to the keyed-matching approach we use in the rewrite tactic.
Remark: we may potentially miss solutions when the head symbol of f is not in S because of is not reduced. Example: S = {add, mul}, and f is @id _ add _ _
We can also use the new "output" parameters available in Lean to encode the unbundled type classes.
The "output" parameters in Lean are really input/output.
So, we can retrieve is_monoid instances by providing just α, (α, op), (α, u), and (α, op, u). There is a performance overhead for type classes that have output parameters.
class is_monoid {α : Type u} (op : out_param $ α → α → α) (u : out_param α) extends is_semigroup op :=
...The main objective is to make sure we can effectively use these type classes in applications.
We will find instances of algebraic structures in many different applications (See Haskell type classes).
Group theory is used in crypto. More generally, it is relevant in any domain where we have transformations, an identity transformation, a composition operator, and an inverse. It feels weird to tell users that whenever they have a group in their application, they MUST use the constants mul or add.
Otherwise, the automation will not work.
The list.append and list.nil example emphasizes this issue. It is a monoid, a left_cancel_semigroup, and a right_cancel_semigroup. We want users to be able to use the algebraic normalizer without forcing them to use add for list.append and zero for list.nil.
For more complex structures (e.g., rings and fields), it may be reasonable to force users to stick to some notation, and tell them that the automation will only work if they use add and mul.
Note that we already do it in many cases (e.g., monad, functor, ...).
I think this approach works reasonably well whenever type indexed type classes is a good match. By a good match, I meant "given a type A, there is only one instance of type class C".
We want to be able to define notation as we declare structures. Example:
class functor (f : Type u → Type v) : Type (max u+1 v) :=
(map : Π {α β : Type u}, (α → β) → f α → f β)
(map_const : Π {α : Type u} (β : Type u), α → f β → f α := λ α β, map ∘ const β)
(infixr <$> := map)
(infixr <$ := map_const)and avoid artificial declarations such as
def fmap {f : Type u → Type v} [functor f] {α β : Type u} : (α → β) → f α → f β :=
functor.map
def fmap_const {f : Type u → Type v} [functor f] {α : Type u} : Π (β : Type u), α → f β → f α :=
functor.map_constFor example, in the current approach we use, we rely on the fact that @add nat nat_has_add is not reduced to nat.add when we use dsimp or the SMT preprocessor. This is not the case if we use has_add.add instead of add. For example, dsimp will reduce @has_add.add nat nat_has_add into nat.add.