creating my own programming language in Lean

Stream: lean4

[Arthur Paulino]

I've been spending the past few days working on a simple and rudimentary programming language. I'm using Lean 4 to build an interpreter.

The thing is: I am struggling with the parser. I tried looking at Parsec but I couldn't understand how to use it in a way that wouldn't be too laborious. This is how the parser is implemented at the moment. And I'm afraid things are going very sideways at this point.

This is an example of what I'm trying to parse:

a := 4         # int
f x y := x + y # function _ → _ → _
fa := f a      # function int → int
fa3 := fa 3    # 7 : int
g n :=
  s := 0
  while > 0
    s := s + n
    n := n - 1
  s
print g 5      # 15

Ideas and feedback are very much welcome :pray:

[Wojciech Nawrocki]

Have you considered using Lean's own extensible Syntax? For example as in here and the webserver demo. Also the do notation definitions have an imperative flavour similar to your language.

[Arthur Paulino]

Will take a look tomorrow for sure. I always thought of Syntax as something exclusive for Lean's own compiler

[Arthur Paulino]

My main difficulty is extracting data from a formatted text (a term of type String) without regex

[Sebastian Ullrich]

It's not all pretty, but it's possible to use Lean's parser outside of Lean, yes. Lean 4 Leanpkg used to do this to parse TOML files: https://github.com/leanprover/lean4/blob/2b7427c962ddab1fc28c9b1f933947b5f7cd60cb/src/Leanpkg/Toml.lean

[Sebastian Ullrich]

This should get nicer in the future when we have builtin syntax for syntax compiled into the binary (currently covered by leading_parser etc.) and per-category token sets.

[Arthur Paulino]

Huh, I was scared of that approach. Am I mistaken or that program loads up the TOML file as a Lean file (hence the "HACKHACKHACK")?
I will seek other solutions for now then. Maybe something useful comes out of it

[Mario Carneiro]

I don't think it is necessary to load the file as a lean file, you should be able to create and call the Parser directly

[Mario Carneiro]

the simplest solution is if you can literally embed the syntax in a lean file, headed by a macro or something

[Arthur Paulino]

If this is possible, then I most likely can take care of the rest:

inductive MyType
  | num : Nat → MyType
  | op  : MyType → MyType → MyType
  deriving Repr

declare_syntax_cat mytype
syntax num : mytype
syntax num " !! " num : mytype

def parseMyType (s : String) : MyType := sorry

#eval parseMyType "3"      -- MyType.num 3
#eval parseMyType "4 !! 5" -- MyType.op (MyType.num 4) (MyType.num 5)

[Mario Carneiro]

do you mind if it lives in a monad, say MetaM?

[Sebastian Ullrich]

Arthur Paulino said:

that program loads up the TOML file as a Lean file

No, the file is parsed in the category file defined above https://github.com/leanprover/lean4/blob/2b7427c962ddab1fc28c9b1f933947b5f7cd60cb/src/Leanpkg/Toml.lean#L60

[Sebastian Ullrich]

I think the first two HACKs are obsolete, we now create antiquotations for syntax abbrevs

[Arthur Paulino]

Mario Carneiro said:

do you mind if it lives in a monad, say MetaM?

Nope. I already need to be in IO because I have to read a file. And I remember lifting a MetaM monad from IO

[Mario Carneiro]

if you need to lift from IO to MetaM, keep in mind that you need an environment that contains those syntax declarations

[Mario Carneiro]

in the example this is done using importModules [{ module := `Leanpkg.Toml }] {}

[Mario Carneiro]

where the syntax declarations are in Leanpkg.Toml

[Arthur Paulino]

I don't understand it. Is Leanpkg.Toml on that very same file?

[Arthur Paulino]

(I ask this because I see namespace Toml)

[Mario Carneiro]

yes, Leanpkg.Toml is the file itself

[Mario Carneiro]

this is a lean file that at runtime reads the olean file it created at compile time

[Arthur Paulino]

Mario Carneiro said:

do you mind if it lives in a monad, say MetaM?

I got the impression that you were about to propose a solution that's simpler than the TOML example. Were you :D ?

[Mario Carneiro]

import Lean
open Lean Parser
inductive MyType
  | num : Nat → MyType
  | op  : MyType → MyType → MyType
  deriving Repr

declare_syntax_cat mytype
syntax num : mytype
syntax mytype " !! " mytype : mytype


partial def parseMyType (env : Environment) (s : String) : Except String MyType := do
  let rec parseCore
  | `(mytype| $x:numLit) => pure $ MyType.num x.toNat
  | `(mytype| $a !! $b) => return MyType.op (← parseCore a) (← parseCore b)
  | _ => throw "parse error"
  parseCore (← runParserCategory env `mytype s)

#eval show MetaM _ from return parseMyType (← getEnv) "3"      -- MyType.num 3
#eval show MetaM _ from return parseMyType (← getEnv) "4 !! 5" -- MyType.op (MyType.num 4) (MyType.num 5)

[Arthur Paulino]

Holy smokes, let me try using that idea :open_mouth:

[Mario Carneiro]

it even gives kind-of-good error messages

[Arthur Paulino]

It's working!

#eval show MetaM _ from return parseProgram (← getEnv) "a := 3; b := a + a; b + 1"
-- Except.ok (Program.attribution
--   "a"
--   (Program.sequence
--     (Program.evaluation (Expression.atom (Value.int 3)))
--     (Program.attribution
--       "b"
--       (Program.sequence
--         (Program.evaluation (Expression.add (Expression.var "a") (Expression.var "a")))
--         (Program.evaluation (Expression.add (Expression.var "b") (Expression.atom (Value.int 1))))))))

[Arthur Paulino]

Although it should start with Program.sequence .... It's parsing as an attribution of 3; b := a + a; b + 1 to the variable a

[Jakob von Raumer]

You should be able to fix this by giving the precedences explicitly

[Arthur Paulino]

I was able to create the env by doing

initSearchPath (← Lean.findSysroot) ["build/lib"]
let env ← importModules [{ module := `FunnyLang.Parser }] {}

But now my binary relies on being inside the repository. Is there a workaround for this?

[Arthur Paulino]

There is one solution, which is keeping a copy of the Parser.lean file as a string and then running Lean's frontend on it to get the env. But I really don't want to touch that

[Sebastian Ullrich]

You do not need the source file, but you do need the .olean file and those of its dependencies

[Arthur Paulino]

Does it mean that if I wanted to release a binary for this interpreter, I'd need to release the olean file as well?

[Arthur Paulino]

Is this kind of issue that builtin syntax would solve?

[Sebastian Ullrich]

yes to both

[Sebastian Ullrich]

You could do the latter right now by using Parser instead of syntax like Lean itself does, but it is quite different.

[Arthur Paulino]

is there an example I can see that's not the Lean 4 parser itself? Maybe some simple test case

[Sebastian Ullrich]

I don't think so, no. I developed syntax so most people could avoid Parser/leading_parser :)

[Arthur Paulino]

I'm happy waiting for builtin syntax then (and using this current solution) :smiley:

[Arthur Paulino]

Still on the topic of syntax, I'm not being able to figure this out on my own.
I believe this line is the culprit.

I've set up a bunch of tests below this line and I want to define the syntax such that those #assert lines say nothing. Some of them are already passing, but most of them are complaining.

I'm trying to make the parser understand indentation. But as soon as I use withPosition on the syntax:25 program program : program line, Lean breaks down and the server dies due to some loop that I don't understand.

As always, guidance is very much appreciated :pray:

[Mario Carneiro]

wait, how is syntax:25 program program : program supposed to work? That's just going to cause unbounded recursion

[Mario Carneiro]

is the intention to support newline-separated statements like in by blocks? If so you can look at how tactic does it

[Mario Carneiro]

the key part there is src4#Lean.Parser.many1indent, which would be written withPosition(colGe p) in the syntax language

[Mario Carneiro]

Here's a version that works, except that I had to adjust the indentation in p10 and p11 since all the lines have to line up

declare_syntax_cat                            value
syntax ("-" noWs)? num                      : value
syntax str                                  : value
syntax "true"                               : value
syntax "false"                              : value
syntax ("-" noWs)? num noWs "." (noWs num)? : value
syntax withPosition("[ " colGt value* " ]") : value
syntax "nil"                                : value

declare_syntax_cat                    expression
syntax value                        : expression
syntax " ! " expression             : expression
syntax expression " + "  expression : expression
syntax expression " * "  expression : expression
syntax expression " = "  expression : expression
syntax expression " != " expression : expression
syntax expression " < "  expression : expression
syntax expression " <= " expression : expression
syntax expression " > "  expression : expression
syntax expression " >= " expression : expression
syntax ident (colGt expression)*    : expression
syntax "( " expression " )"         : expression

declare_syntax_cat program

syntax programSeq := withPosition((colGe program)+)
syntax "skip"                                                 : program
syntax withPosition(ident+ " := " colGt programSeq)           : program
syntax expression                                             : program
syntax "if" expression "then" colGt programSeq "else" colGt programSeq : program
syntax withPosition("while" expression "do" colGt programSeq) : program
syntax " ( " programSeq " ) " : program

open Lean Elab Meta

def mkApp' (name : Name) (e : Expr) : Expr :=
  mkApp (mkConst name) e

def elabValue : Syntax → TermElabM Expr
  | `(value|$n:numLit) =>
    mkAppM ``Value.int #[mkApp' ``Int.ofNat (mkNatLit n.toNat)]
  | _ => throwUnsupportedSyntax

def elabStringOfIdent (id : Syntax) : Expr :=
  mkStrLit id.getId.toString

partial def elabExpression : Syntax → TermElabM Expr
  | `(expression| $v:value) => do mkAppM ``Expression.atom #[← elabValue v]
  | `(expression| ! $e:expression) => do
    mkAppM ``Expression.not #[← elabExpression e]
  | `(expression| $n:ident $[$es:expression]*) => do
    let es ← es.data.mapM elabExpression
    match es with
    | []      => mkAppM ``Expression.var #[elabStringOfIdent n]
    | e :: es =>
      let l  ← mkListLit (Lean.mkConst ``Expression) es
      let nl ← mkAppM ``List.toNEList #[e, l]
      mkAppM ``Expression.app #[elabStringOfIdent n, nl]
  | `(expression| $l:expression + $r:expression) => do
    mkAppM ``Expression.add #[← elabExpression l, ← elabExpression r]
  | `(expression| $l:expression * $r:expression) => do
    mkAppM ``Expression.mul #[← elabExpression l, ← elabExpression r]
  | `(expression| $l:expression = $r:expression) => do
    mkAppM ``Expression.eq #[← elabExpression l, ← elabExpression r]
  | `(expression| $l:expression != $r:expression) => do
    mkAppM ``Expression.ne #[← elabExpression l, ← elabExpression r]
  | `(expression| $l:expression < $r:expression) => do
    mkAppM ``Expression.lt #[← elabExpression l, ← elabExpression r]
  | `(expression| $l:expression <= $r:expression) => do
    mkAppM ``Expression.le #[← elabExpression l, ← elabExpression r]
  | `(expression| $l:expression > $r:expression) => do
    mkAppM ``Expression.gt #[← elabExpression l, ← elabExpression r]
  | `(expression| $l:expression >= $r:expression) => do
    mkAppM ``Expression.ge #[← elabExpression l, ← elabExpression r]
  | `(expression| ($e:expression)) => elabExpression e
  | _ => throwUnsupportedSyntax

partial def elabProgram : Syntax → TermElabM Expr
  | `(programSeq| $p1:program $[$p:program]*) => do
    p.foldlM (init := ← elabProgram p1) fun a b => do
      mkAppM ``Program.sequence #[a, ← elabProgram b]
  | `(program| skip) => return mkConst ``Program.skip
  | `(program| $n:ident $ns:ident* := $p:programSeq) => do
    match ns.data.map elabStringOfIdent with
    | []      =>
      mkAppM ``Program.attribution #[elabStringOfIdent n, ← elabProgram p]
    | n' :: ns =>
      let l  ← mkListLit (Lean.mkConst ``String) ns
      let nl ← mkAppM ``List.toNEList #[n', l]
      mkAppM ``Program.attribution #[
        elabStringOfIdent n,
        mkApp' ``Program.evaluation $
          mkApp' ``Expression.atom $
            ← mkAppM ``Value.curry #[nl, ← elabProgram p]
      ]
  | `(program| if $e:expression then $p:programSeq else $q:programSeq) => do
    mkAppM ``Program.ifElse
      #[← elabExpression e, ← elabProgram p, ← elabProgram q]
  | `(program| while $e:expression do $p:programSeq) => do
    mkAppM ``Program.whileLoop #[← elabExpression e, ← elabProgram p]
  | `(program| $e:expression) => do
    mkAppM ``Program.evaluation #[← elabExpression e]
  | `(program| ($p:programSeq)) => elabProgram p
  | _ => throwUnsupportedSyntax

------- ↓↓ testing area ↓↓

elab ">>" ppLine p:programSeq ppLine "<<" : term => elabProgram p

open Lean.Elab.Command Lean.Elab.Term in
elab "#assert " x:term:60 " = " y:term:60 : command =>
  liftTermElabM `assert do
    let x ← elabTerm x none
    let y ← elabTerm y none
    synthesizeSyntheticMVarsNoPostponing
    unless (← isDefEq x y) do
      throwError "{← reduce x}\n------------------------\n{← reduce y}"

def p1 := >>
min x y :=
  if x < y
    then x
    else y
min 5 3
<<.toString

def p2 := >>
(min x y :=
  if x < y
    then x
    else y)
min 5 3
<<.toString

#assert p1 = p2

def p3 := >>
while 1 < a do
  x := 2
a < 3
<<.toString

def p4 := >>
while 1 < a do x := 2
a < 3
<<.toString

def p5 := >>
(while 1 < a do x := 2)
a < 3
<<.toString

#assert p3 = p4
#assert p4 = p5

def p6 := >>
(f x y :=
  x + y)
(f3 := f 3)
f32 := f3 2
<<.toString

def p7 := >>
(f x y := x + y)
(f3 := f 3)
f32 := f3 2
<<.toString

#assert p6 = p7

def p8 := >>
f x y := x + y
f3 := f 3
f32 := f3 2
<<.toString

#assert p7 = p8


def p9 := >>
a :=
  x := 5
  y = 5
2 + 5
<<.toString

def p9' := >>
(a :=
  x := 5
  y = 5)
2 + 5
<<.toString

def p10 := >>
a :=
  (x := 5
   y = 5)
2 + 5
<<.toString

def p11 := >>
(a :=
  ((x := 5)
   y = 5))
2 + 5
<<.toString

#assert p9 = p9'
#assert p9 = p10
#assert p10 = p11

[Sebastian Ullrich]

Arthur Paulino said:

I'm trying to make the parser understand indentation. But as soon as I use withPosition on the syntax:25 program program : program line, Lean breaks down and the server dies due to some loop that I don't understand.

Lean eliminates the left recursion in syntax cat ... : cat, but if you wrap it in withPosition, it doesn't happen anymore

[Arthur Paulino]

And as always, thanks a lot :octopus:

[Arthur Paulino]

(I just noticed that you fixed other syntax definitions in my code, thanks for those as well :heart:)

[Arthur Paulino]

I ran into a syntax trouble again :face_palm:
I apologize upfront for not being able to reduce the code to a smaller #mwe.

I'm trying to represent a function application:

• f 3 3 applies 3 and 3 to the function f
• f a 3 applies a and 3 to the function f

In my code, f 3 3 is properly parsed as "f [3 3]", "[3 3]" being a list of expressions. However, I can't seem to be able to make Lean understand f a 3 as "f [a 3]". Instead, it's parsing as if I were passing an application of 3 to the "function" a and then passing the result to the function f

As you can see, I put a debug message so we can know the number of application arguments being parsed. In the f 3 3 example it prints out 2, which is correct. But in f a 3 it prints out 1 and then 1 again, which is coherent with the behavior I'm describing above.

Any ideas how I can escape of this right precedence behavior? I tried setting precedence values in a lot of different ways without success

[Arthur Paulino]

While trying to create an #mwe, I was able to make this small prototype work:

import Lean

declare_syntax_cat foo
syntax num                      : foo
syntax:51 ident                 : foo
syntax:49 ident (colGt foo:50)+ : foo

elab " ⟪ " f:foo " ⟫ " : term =>
  match f with
  | `(foo| $i:ident $fs:foo*) =>
    dbg_trace fs.size
    default
  | _ => default

#eval ⟪f 3 3⟫ -- 2
#eval ⟪f a 3⟫ -- 2

But when I try to plug this idea in my code, it breaks all my other examples with working syntax

[Arthur Paulino]

Wait, nevermind. I got it!
I had to add a match case for the | `(expression| $n:ident) alone :tada:

[Notification Bot]

Arthur Paulino has marked this topic as resolved.

[Notification Bot]

Arthur Paulino has marked this topic as unresolved.

[Arthur Paulino]

Hi everyone! I'm happy to announce that the first iteration my first ever programming language is finished and documented. I named it Fxy.

There's still a lot of work on the reasoning front, but the implementation is working nicely already. I wouldn't have been able to do it without the ideas from @Simon Hudon and @Mario Carneiro. Also, big thanks to everyone who helped me in this thread.

Fxy is (obviously) infinitely simpler than Lean 4 and thus might serve as a small (and yet not too trivial) showcase of how to use Lean 4 for programming purposes.

A small example of a Fxy program to compute the sum of the n first natural numbers:

f n :=
  s := 0
  i := 0
  while i < n do
    i := i + 1
    s := s + i
  s
!print f 5 # prints 15

[Julian Berman]

Very very cool Arthur. I see you're also working on showing off some reasoning there now -- is the idea that someone will be able to take a Fxy program like that one and prove things about it from within Lean via some exposed intermediate API? If so in some nice future world where someone writes an e.g. Python interpreter in Lean 4 that will be very cool.

[Arthur Paulino]

That idea actually blew my mind. No, it wasn't on my radar. I just want to learn about semantics reasoning and that's why there exists an implementation of small steps. But hey, being able to reason about Python code from Lean would be pretty cool! (Although I believe that only a subset of Python could be considered in such scenario)

[Henrik Böving]

Julian Berman said:

Very very cool Arthur. I see you're also working on showing off some reasoning there now -- is the idea that someone will be able to take a Fxy program like that one and prove things about it from within Lean via some exposed intermediate API? If so in some nice future world where someone writes an e.g. Python interpreter in Lean 4 that will be very cool.

Formally arguing about non functional languages is usually rather complicated because of all the pointer/reference stuff that can change all the time. The Coq people have done huge amounts of efforts to argue about a C subset, I imagine an even more complicated and less typed language like python will be much harder.

[Julian Berman]

Thanks, I figured this was definitely not a new idea and likely a hard one :D -- seems like I found this or this fairly quickly to peruse.

[Tomas Skrivan]

Very nice! At some point I might attempt to parse existing scripting language VEX in Houdini to Lean 4 and looking at Fxy as a guiding example will be tremendously helpful.

[Henrik Böving]

Julian Berman said:

Thanks, I figured this was definitely not a new idea and likely a hard one :D -- seems like I found this or this fairly quickly to peruse.

The two big names in Coq world regarding formalization of C are CompCert and VST/Verified Software Toolchain if youre interested in that.

[Julian Berman]

I am indeed, thanks for pointing me in the right direction! (Now I'll probably stop crowding Arthur's cool thread!)

[Arthur Paulino]

@Tomas Skrivan I also implemented a way to parse Fxy code in Lean itself (not from a string). I used it mostly for debugging (see MetaDebug.lean), but I believe cooler things can be done with it

[Tomas Skrivan]

I have no clue how these things work ... are you using the same parser code to parse Fxy from a *.fxy file and from within a *.lean file?

[Tomas Skrivan]

Ughhh I'm confused, you have two ways of running Fxy, right? Either you have your own execution defined in Executaion.lean or you turn Fxy code into Lean expression, in MetaDebug.lean, and execute that. Why do you have these two ways of doing that?

[Arthur Paulino]

There are two ways to parse Fxy code and two ways to run a (parsed) Fxy program. Those are orthogonal.

You can parse code from a fxy file or from a lean file. Once you have a Program, you can run it using the verifiable runner or the non-verifiable runner.

The parsers use the same syntax (see Syntax.lean). Hm, I should explain this better in the repo

[Arthur Paulino]

The parsers themselves are very similar, but one produces a term of Program (when reading from a fxy file) and the other produces a term of Expr (this is what you'd do in term elaboration - read this chapter written by @Henrik Böving )

[Arthur Paulino]

Answering the question of "why", it was just for debugging. It's much faster to debug the executor if the code can be parsed from Lean code than if I had to do cycles of lake build and fxy file editing everytime. And btw this was one aspect of the development which really made Lean 4 shine IMO

[Tomas Skrivan]

That makes sense, is there a way to keep those two executors in sync? Or you just hope they match each other? As the language grows I guess you will drop the debugging executor, or no?

[Siddhartha Gadgil]

Very Nice. One hope of mine to try some day is the GAP system so a bunch of mathematical algorithms run in Lean 4. Hopefully they can be lifted step-by-step to certified ones.

[Arthur Paulino]

@Tomas Skrivan I think you mean the debugging parser. Maybe!
If you see the file you'll notice that it's also easy to create test cases with it

[Christian Pehle]

Similarly it might be cool if Lean 4 would eventually be used to replace the bespoke scripting languages in Singular, Macaulay 2 etc. with something that has more solid foundations.

[Arthur Paulino]

If using Lean's syntax to parse generic strings (e.g. extracted from text files) becomes a thing, then a proper workaround for this part might be more useful than expected

[Kevin Buzzard]

@Siddhartha Gadgil which group theory algorithms in particular are you interested in? I'm assuming that "formally verify GAP algorithms" is not really possible, so it's "re-implement GAP algorithms in Lean and prove they're correct"?

[Siddhartha Gadgil]

@Kevin Buzzard The actual algorithms I plan to try to implement (with proofs) are those from Geometric/Combinatorial group theory. For example, the word and conjugacy problems for surface groups and free groups. I do not know if these are in GAP, but either way I would work from scratch in Lean 4.

The GAP stuff was more speculation. What I mean was that since the syntax of lean 4 is so nicely extendable, elaborators will translate appropriately enclosed (or read from files) objects as lean objects. So in principle one can try to prove theorems about these. A variant is to use the pretty printer to actually generate lean code and work with this. The broad idea is to start with lean purely as a programming language, with interpreters able to run code in at least small languages like GAP. And see if algorithms can be enriched incrementally with proofs.

Whether this is even remotely practical I have no idea, and won't till it is tried.

[Kevin Buzzard]

I think it's an interesting idea whether or not it's practical. It might be hard to sell to the math community -- "oh GAP is a pretty good piece of software and I'll continue to use it over yours because it's faster and you don't usually hit bugs" -- but I think that formally verified serious mathematical software will only get better over time and it's worth trying to put down some markers, so we can discover what the state of the art looks like.

[Siddharth Bhat]

One thought might be to run GAP algorithms unverified in Lean, and then verify that the results are correct via proof certificates within Lean4. So GAP is used to import untrusted algorithms, whose results we check with formally proven verifiers..I've started on a GAP embedding in Lean (https://github.com/opencompl/lean-gap), though it's early days yet.

[Siddhartha Gadgil]

A verified algorithm can also give a formal proof. For instance one may want to show that something is not a sphere, and a verified algorithm may show that its fundamental group is non-trivial (there is an actual published paper in a top journal with the opposite error - something that was claimed about a sphere but turns out was about a space with non-trivial fundamental group).

[Siddhartha Gadgil]

Just speculation at this point, but how hard will it be to have a command elaborator for say importFxy filename which imports an fxy file and makes lean definitions corresponding to function definitions in the fxy file?

[Arthur Paulino]

i'm guessing you'd intend to do it at compilation time, because at execution time it's already the current flow.

If you can perform IO operations (reading a text file) at compilation time, then you can pass the content of a fxy file to the parse function, which should take care of the rest. Notice that the current parsing method also requires an Environment containing the syntax definitions, but it can be done from a monad like MetaM via getEnv.

[Arthur Paulino]

So the question becomes: how to read an arbitrary text file at compilation time? I don't know, but I do recall seeing people do it

[Sebastian Ullrich]

Easily, because IO can be lifted into CoreM etc

[Siddhartha Gadgil]

That is what I thought @Sebastian Ullrich - and am I correct that this should work in the interpreter too? (My agenda eventually is to target GAP).

[Sebastian Ullrich]

There should be no semantic difference between compiled code and the interpreter except that the latter cannot directly call extern declarations

[Arthur Paulino]

@Sebastian Ullrich I just want to point out that this still happens with yesterday's nightly build