A new implementation in Lean 4

[loredanacirstea]

A new Mal implementation in https://github.com/leanprover/lean4

Except eval related tests from step 6, all non-optional tests pass. Due to Lean's restrictions on types, I was not able to implement eval in a satisfactory way.

The Mal version at commit loredanacirstea@562f84e is provable by Lean standards - it does not contain IO side effects (reading files, IO printing). It solves logs by keeping them in the environment instance and forwarding them along, only printing them at the end. There are no mutable elements.

The Env instances are not recursive, but I found a way to merge environments and assign each environment and variable a level index. Root has a 0 index, which increases each time a new environment is created with fn* or let*. When I merge two environments, I choose the variable with a higher level. And I make sure to bubble up any atoms defined in lower-level environments, in case they were changed.

To implement the full guide, I had to change and introduce the IO monad for files, printing logs, and throwing errors, which simplified the code, but we lost proving abilities.

Regarding eval: it needs access to the root Env instance, which is usually passed by reference in other implementations. I tried to have a recursive Env here https://github.com/loredanacirstea/mal/blob/lean4-env-ioref-recursive/impls/lean/LeanMal/types.lean#L59, but the prover complained that it does not have a full understanding of all the types, due to the cyclic definition (Types <-> Fun <-> Env ...) . Lean has the mutual block that supports cyclic definitions only for inductive types (like Types, Dict), not for types using IO.Ref (required for passing by reference).

A functional, immutable way to implement eval may be to bubble up any variables with a low level index in Env (eval should set variables with level index 0), similar to what I did for atoms.

[kanaka]

You'll need to add a Dockerfile and add the implementation to Makefile.impls and IMPLS.yaml and to get the automated GHA CI workflow to test this.

The inability to mutate environments may not allow it to pass all tests including self-hosting. For particularly interesting implementations, I've waived the self-host requirement before (and Lean might fit that, not sure yet), but it will need to pass all the non-self-hosting tests at least. If it can't pass the non-self-hosted tests then I'll be happy to link to this in the "Other Implementations" section of the README. There are some extra tests that specifically test env mutation that are not in the base set of tests yet but probably will be soon (because this issue is detected in self-host tests but should be detected earlier):

(def! a 12)
(def! fx (fn* () a))
(fx)
;=>12
(def! a 2000)
(fx)
;=>2000

Regarding the eval issue, it's preferred but it's not strictly required that the eval function wrap the outer REPL environment. Closing over the current lexical scope env is also acceptable. The guide indicates the former, but I don't think there are any tests that enforce that and for the time being a suggestion rather than requirement.

[loredanacirstea]

I added the Dockerfile.

Regarding eval:

Closing over the current lexical scope env is also acceptable.

I tested this and introduced a small change where the new env returned by eval is forwarded to its parent scope, instead of being discarded as usual.

partial def evalFunc (env: Env) (head : Types) (args : List Types) : IO (Env × Types) := do
    let (env2, fn) ← evalTypes env head
    let (fref, res, forwardEnv) ← evalFuncVal env2 fn args
    -- after executing a function, propagate atoms (defined in outer environments) to the parent scope
    -- eval returns true for forwarding the environment
    if forwardEnv then return (fref, res)
    else return ((forwardMutatedAtoms fref env), res)

Non-optional eval tests pass. But this is not enough to make the load-file tests pass. (def! load-file (fn* (f) (eval (read-string (str "(do " (slurp f) "\nnil)"))))) -> eval's env is forwarded to load-file env, but not forwarded further.

step 6 tests:

TEST: '(eval (read-string "(+ 2 3)"))' -> ['',5] -> SUCCESS
TEST: '(let* (b 12) (do (eval (read-string "(def! aa 7)")) aa ))' -> ['',7] -> SUCCESS

TEST: '(load-file "../tests/inc.mal")' -> ['',nil] -> SUCCESS
TEST: '(inc1 7)' -> ['',8] -> FAIL (line 43):
    Expected : '.*\n8'
    Got      : "(inc1 7)\nError: 'inc1' not found"
TEST: '(inc2 7)' -> ['',9] -> FAIL (line 45):
    Expected : '.*\n9'
    Got      : "(inc2 7)\nError: 'inc2' not found"
TEST: '(inc3 9)' -> ['',12] -> FAIL (line 47):
    Expected : '.*\n12'
    Got      : "(inc3 9)\nError: 'inc3' not found"

--optional--
TEST: '(def! a 1)' -> ['',1] -> SUCCESS
TEST: '(let* (a 2) (eval (read-string "a")))' -> ['',1] -> SOFT FAIL (line 172):
    Expected : '.*\n1'
    Got      : '(let* (a 2) (eval (read-string "a")))\n2'

So, I am going to try the idea from my first post and bubble up variables defined with eval for the root scope (level 0).

[loredanacirstea]

I don't understand why this test is not passing. run_argv_test.sh executes print_argv.mal => executes (prn *ARGV*)
which prints the args and returns nil.
Why does it expect to only print the args?

Testing ARGV of test^lean^step6; step file: impls/lean/step6_file
Running: env STEP=step6_file MAL_IMPL=js ../tests/run_argv_test.sh ../lean/run 
FAIL: Expected '("aaa" "bbb" "ccc")' but got '("aaa" "bbb" "ccc")
nil'

make: *** [Makefile:238: test^lean^step6] Error 1

[kanaka]

That's so that you can use mal implementations as a scripting language (and pipe results into other commands for example). Being able to print exactly what the script wants to print is important. The script can print the return value explicitly if it wants, but it should be able to avoid printing that too. So when a mal is invoked to load/run another command the final return value needs to be swallowed.

[loredanacirstea]

Status:

I now have a more general/correct handling of scopes:

• Env contains all symbols defined in the current & outer scopes, where (key, level) is a unique identifier
• you can get a value by recursively searching in the env by (key, current_level)
• I added a cache of key => last_level, to get the most up-to-date value for a variable fast - this is required for recursive function support.

I expected all non-optional tests to pass, but I still have an issue with exiting the process for this test:

Testing ARGV of test^lean^step6; step file: impls/lean/step6_file
Running: env STEP=step6_file MAL_IMPL=js ../tests/run_argv_test.sh ../lean/run 
OK: '("aaa" "bbb" "ccc")'
FAIL: Expected '()' but got 'user> '

Even though IO.Process.exit seems to be the way to exit a process in Lean4: https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#IO.Process.exit

mal/impls/lean/LeanMal/step6_file.lean

Lines 277 to 283 in fcdd7e5

	if args.length > 2 then
	let astArgs := ((args.drop 1).map (fun arg => Types.strVal arg))
	let newenv := setSymbol env0 "*ARGV*" (Types.listVal astArgs)
	let (_, _) ← rep newenv s!"(load-file \"{args[0]!}\")"
	IO.Process.exit 0
	return
	else

[kanaka]

I don't know why the exit doesn't immediately exit (although if it's monadic, maybe control flow needs to unroll to the top-level before the action takes effect? It doesn't look like the code after the else statement is indented. Is the "else" statement in lean 4 indent sensitive? If not maybe you need a do after the else so that the repl code isn't executed? Just stabbing in the dark here.

Maybe another option would be moving the donext up and then setting it to false in the args > 2 case?

[loredanacirstea]

The above issue was at the last run_argv_test.sh test, with just a filename and no args. I modeled the main code after the js/node implementation & forgot to update if args.length > 2 to if args.length > 0

The more complex implementation with env levels brought an issue with tail call optimization. I tried to fix it in https://github.com/loredanacirstea/mal/tree/lean4-TCO, trying to make evalFunc TCO friendly again by rewriting forwardOuterScopeDefs (last version forwardOuterScopeDefs7), but no luck. Step 5 passes (def! res2 (sum2 10000 0)) test in 8-9sec, but step 6 times out.
The most I could do with this version (lean4-TCO branch) is:

• (def! res2 (sum2 5000 0)) - 6sec
• (def! res2 (sum2 7000 0)) - 12sec
• (def! res2 (sum2 10000 0)) - 28sec

For this lean4 PR, I reverted to an older version (with an eval that only works on the parent scope) which passed older tests, but I see it now fails with a new test added last week (try* (eval (read-string "(+ 1")) (catch* e (prn :e e)))

Unfortunately, I don't have more time now to work on this PR.