Lean 4 under the hood

Stream: lean4

[Mario Carneiro]

This will be a list of questions that came up while trying to write lean 4 tactics, macros and other backend things. The intent is to record that I had the question and what the answer was in hopes of improving documentation in the future.

To parse 1D array literals, you need:

syntax "#[" sepBy(term, ", ") "]" : term
macro_rules  | `(#[ $elems,* ]) => ...

Q: What is the analogue for 2D array literals (nested sepBy)?

syntax "#[" sepBy(sepBy(term, ", "), "; ") "]" : term
macro_rules | `(#[ ??? ]) => ...

The rust syntax would be $($elems,*);* but that doesn't work.

[Mario Carneiro]

Q: How do you evaluate a syntax quotation?

#eval `(#[1, 2; 3, 4])

doesn't work because it doesn't know what monad it's working in.

import Lean
open Lean Elab Command
#print CommandElabM
#eval show CommandElabM Syntax from do `(#[1, 2; 3, 4])

doesn't work because CommandElabM doesn't implement MetaEval, whatever that means. What monads should I be using in #eval?

[Mario Carneiro]

A: UseTermElabM:

import Lean
open Lean Elab
#eval show TermElabM Syntax from do `(#[1, 2; 3, 4])
-- (term#[_,;] "#[" [[(numLit "1") "," (numLit "2")] ";" [(numLit "3") "," (numLit "4")]] "]")

The only monads that can be used in #eval are those implementing MetaEval, namely TermElabM and MetaM, and those implementing Eval, namely IO and pure expressions.

[Lim, Thing-han]

I just found out that using quote also works for evaluate a syntax quotation~

[Mario Carneiro]

quote works but it does something else, I think. `(1+1) captures the Syntax corresponding to 1+1, i.e. the AST of that expression, while quote (1+1) will return a syntax that represents the numeral 2

[Mario Carneiro]

(it's the equivalent of lean 3 reflect, while `(..) is the equivalent of lean 3 ``(..))

[Sebastian Ullrich]

Mario Carneiro said:

The rust syntax would be $($elems,*);* but that doesn't work.

We use $[...] for that purpose because we already use $(e) for antiquotations with non-atomic terms.

macro_rules
  | `(#[ $[$elemss,*];* ]) => _

I've just written a journal chapter on our antiquotations, which I should copy to the docs when I find time...
For many (undocumented) examples, see also https://github.com/leanprover/lean4/blob/master/tests/lean/StxQuot.lean, which shows another way to run syntax quotations: Unhygienic.run, which as the name says can break hygiene because it does not depend on a name generator state.

[Mario Carneiro]

How do you do ambiguity resolution in a macro?

syntax "#[" sepBy(sepBy(term, ", "), "; ") "]" : term

macro_rules
  | `(#[ $[$elems,*];* ]) => `(())

#eval #[1, 2]
-- ambiguous, possible interpretations
--   Unit.unit
--
--   #[1, 2]

Is there a priority system, or a way to throwError in the macro_rules so that it doesn't get picked?

[Sebastian Ullrich]

Yes to both: https://github.com/leanprover/lean4/blob/master/tests/lean/macroPrio.lean and Macro.throwUnsupported

[Miguel Raz Guzmán Macedo]

Nice to see you thinking about this @Mario Carneiro . Julia and Numpy and Matlab have written tons of arguments on how to make A * B polymorphic and mathematically consistent. It turns out that Householder linear algebra notation can be quite tricky to get right because of historical and inconsistent definitions of what a vector means.
In Julia, we found that making #[1, 2, 3] a RowVector and #[ 1 2 3] a column vector a neat solution to preserve the appropriate mathematical mappings when doing linear algebra operations.
This 20 min talk by Dr. Jiahao Chen is a good summary of why it was hard to talk about and how it's been solved in Julia:
https://www.youtube.com/watch?v=C2RO34b_oPM

Concretely: distinguishing between a row vector and a column vector allowed us to have A * B when are different row or column vectors to have the appropriate dimentions or become a scalar when the dot product is applied. Lean should consider using that as well.

[Mario Carneiro]

I think that the #[1 2 3] syntax would be a bit tough in lean since that means application

[Yakov Pechersky]

You can use type synonyms instead in Lean

[Mario Carneiro]

but lean 4 parsing is pretty much magic so I wouldn't consider anything impossible, if you really want to make it work

[Johan Commelin]

In Lean 3 mathlib we have vector which is "1-dimensional" and you can apply row or col to make it "2-dimensional" in the sense that you get a matrix of size m x 1 or 1 x n.

[Miguel Raz Guzmán Macedo]

Yeah, it's your call on syntax, but its the distinction that matters.

[Mario Carneiro]

Oh yeah that wouldn't be too bad, you just write #[1, 2, 3].row and #[1, 2, 3].col

[Miguel Raz Guzmán Macedo]

Oh that's interesting @Johan Commelin .
Do you get a scalar from multiplying a 1 x n vector by an appropriate n x 1?

[Mario Carneiro]

You would get a 1x1 matrix

[Miguel Raz Guzmán Macedo]

Like Matlab!

[Johan Commelin]

I don't think you should want to get around that, if you use strict types

[Mario Carneiro]

If row and col vectors are considered separate types distinct from matrices then you could get that to evaluate to a scalar

[Johan Commelin]

We have dotproduct : vector -> vector -> scalar

[Miguel Raz Guzmán Macedo]

This is the neat comparison chart at the proper time-stamp
https://youtu.be/C2RO34b_oPM?t=913

[Mario Carneiro]

That too. Is it necessary to distinguish row and col vectors?

[Mario Carneiro]

I don't know that having a seriously overloaded * operator is worth it

[Johan Commelin]

I've always found the distinction artificial. But you certainly want functions to turn them into matrices.

[Miguel Raz Guzmán Macedo]

I'll need to think about how Lean does it.

[Mario Carneiro]

well lean doesn't do it right now so you can do what you like

[Yakov Pechersky]

I proposed a mathlib coercion of (1 x 1) matrices into scalars, but that was shut down

[Mario Carneiro]

In general, in mathlib we use a lot more projection notation like A.mul B which gives some more flexibility to pick the right operation

[Yakov Pechersky]

really a x b where unique a and unique b

[Miguel Raz Guzmán Macedo]

@Mario Carneiro the super overloaded * in Julia is about half the superpower of the language:

julia> methods(*)
# 331 methods for generic function "*":
[1] *(x::T, y::T) where T<:Union{Int128, UInt128} in Base at int.jl:908
[2] *(x::T, y::T) where T<:Union{Int128, Int16, Int32, Int64, Int8, UInt128, UInt16, UInt32, UInt64, UInt8} in Base at int.jl:88
[3] *(s1::Union{AbstractChar, AbstractString}, ss::Union{AbstractChar, AbstractString}...) in Base at strings/basic.jl:260
[4] *(c::Union{UInt16, UInt32, UInt64, UInt8}, x::BigInt) in Base.GMP at gmp.jl:539
[5] *(c::Union{Int16, Int32, Int64, Int8}, x::BigInt) in Base.GMP at gmp.jl:541
...

[327] *(x::Float16, y::Float16) in Base at float.jl:330
[328] *(x::Number) in Base at operators.jl:516
[329] *(x::T, y::T) where T<:Number in Base at promotion.jl:397
[330] *(x::Number, y::Number) in Base at promotion.jl:322
[331] *(a, b, c, xs...) in Base at operators.jl:560

[Yakov Pechersky]

What's very powerful about Lean matrices is that indexing types need not be numeric types.

[Mario Carneiro]

How the hell do you know what anything means?

[Mario Carneiro]

that looks like a nightmare

[Miguel Raz Guzmán Macedo]

This getting a polymorphic * with type class resolution dispatching to the appropriate structured matrix multiplication operations is an algorithmic must for nueric linear algebra.

[Miguel Raz Guzmán Macedo]

What do you mean know what anything means?

[Mario Carneiro]

which of the 331 functions gets called when you write x * y

[Mario Carneiro]

julia is dynamically typed (or something) so it isn't even that easy to find out the types of x and y

[Miguel Raz Guzmán Macedo]

Same as in primary school:
Multiply 2 ints, apply the integer multiplication:

x = 3
y = 4
x * y == 12

[Mario Carneiro]

okay, so which function is getting called there

[Mario Carneiro]

even with the type signatures it's not that obvious to me

[Mario Carneiro]

maybe it's 330? 331?

[Miguel Raz Guzmán Macedo]

julia> @which 3 * 4
*(x::T, y::T) where T<:Union{Int128, Int16, Int32, Int64, Int8, UInt128, UInt16, UInt32, UInt64, UInt8} in Base at int.jl:88

The multiplication that applies to all concrete Integer types.

[Miguel Raz Guzmán Macedo]

It's like 5 characters to find out which specific method is being called.

[Johan Commelin]

How many instance of has_mul does mathlib have? :rofl:

[Mario Carneiro]

well I wouldn't say mathlib is a shining beacon of hope here either

[Miguel Raz Guzmán Macedo]

And user defined functions are easy to instrospect as well:

julia> foo(x::Int, y::Int) = x * y
foo (generic function with 1 method)

julia> foo(2, 3)
6

julia> @which foo(2,3)
foo(x::Int64, y::Int64) in Main at REPL[7]:1

[Johan Commelin]

At least we have widgets :thinking:

[Mario Carneiro]

remember when application turned out to be a binary operator on nat?

[Miguel Raz Guzmán Macedo]

Here, foo(x::Int, y::Int) means: When you call foo and the first argument x is an Int, and the second argument y is an Int, do x * y

[Miguel Raz Guzmán Macedo]

and it's trivial to add new methods for foo that dispatch on different types:

julia> foo(x::String, y::String) = "$x and $y"
foo (generic function with 2 methods)

julia> foo("a", "b")
"a and b"

[Miguel Raz Guzmán Macedo]

And now foo has 2 specific methods:

julia> methods(foo)
# 2 methods for generic function "foo":
[1] foo(x::Int64, y::Int64) in Main at REPL[7]:1
[2] foo(x::String, y::String) in Main at REPL[10]:1

[Mario Carneiro]

I'm not a big fan of operator overloading, but lean has the ability to do these things

[Anne Baanen]

Mario Carneiro said:

julia is dynamically typed (or something) so it isn't even that easy to find out the types of x and y

Not to derail the discussion too much, but I find this a weird argument. If we define a type with a couple of constructors and a function pattern-matching on those:

inductive some_enum : Type
| a : some_enum
| b : some_enum
| c : some_enum
| d : some_enum
| e : some_enum

open some_enum

def foo : some_enum → some_enum → ℕ
| a b := 1
| c d := 37
| ...

would you complain it's hard to figure out which alternative of foo gets called?

[Miguel Raz Guzmán Macedo]

We call it multiple dispatch in Julia-land, I think Lean people have it as type-class based resolution.

[Miguel Raz Guzmán Macedo]

Oh hey @Anne Baanen , long time no see! :wave:

[Mario Carneiro]

@Anne Baanen My issue is more around "whole program type inference" and things of that nature. I'm talking about the types, not the values. In that example foo isn't getting called so I'm not sure exactly how the parallel goes

[Miguel Raz Guzmán Macedo]

FWIW, we don't do "whole program type inference" - Julia uses type inference for optimizations, but only at the function level. If it's not inside a function, we bail the analysis and run the program dynamically.

[Mario Carneiro]

Right, in julia it's more like dynamic typing + function overloading

[Mario Carneiro]

which means that by looking at the code you don't know what the types of values are (sometimes you do, but you don't have to) and hence what functions are getting called

[Mario Carneiro]

maybe I'm just jaded from C++

[Anne Baanen]

Mario Carneiro said:

Anne Baanen My issue is more around "whole program type inference" and things of that nature. I'm talking about the types, not the values. In that example foo isn't getting called so I'm not sure exactly how the parallel goes

Not sure I understand your distinction. Is it a type-level issue now?

def bar (x y : some_enum) : fin (foo x y) := sorry

[Mario Carneiro]

In that example, there is only one function foo getting called, so I can look it up and see the pattern match to find out how the values x and y get treated

[Miguel Raz Guzmán Macedo]

Yeah PTSD from C++ is understandable :sweat_smile: , no worries.

[Mario Carneiro]

If foo was a generic function parameterized by a typeclass, I would have to look to the caller to find out what function is getting run

[Mario Carneiro]

this can get quite involved

[Mario Carneiro]

I've been tracing through lean 4 functions and the higher order arguments make your head spin, it's hard to find where the work gets done

[Miguel Raz Guzmán Macedo]

fwiw in Julia we can always do @edit foo(3,4) and it will open up your editor to the specific line that implements that method.

[Mario Carneiro]

You could kinda sorta do that with lean typeclasses if you #check the term and then look up the relevant typeclass

[Mario Carneiro]

I don't think there is a unique place to look though, there could be lots of typeclasses involved in general

[Anne Baanen]

So this is really an issue with higher-order functions, not generic functions? Because as soon as you have first-class closures, you have arbitrary gotos.

[Mario Carneiro]

well, there are higher order functions but mostly as continuations, they aren't terrible

[Mario Carneiro]

The generics are tough though

[Mario Carneiro]

because go to definition just isn't sufficient anymore

[Mario Carneiro]

The other thing, which is lean specific, is the connection between syntax -> macro -> elab, these are all scattered about and it's not obvious how the links are even connected to each other, let alone how to follow the link

[Sebastian Ullrich]

Sebastian Ullrich said:

I've just written a journal chapter on our antiquotations, which I should copy to the docs when I find time...

Here is the new section (4.1) in the meantime: https://arxiv.org/pdf/2001.10490.pdf