mlang#

A small functional language prototype written in Lean 4.

Current scope:

• integer and boolean literals
• variables
• let
• if
• typed lambdas
• function application
• integer arithmetic
• integer division
• lexical closures
• hand-written lexer and parser
• static type checker
• implicit effect tracking

The interpreter lives in Mlang/Interpreter.lean. The parser lives in Mlang/Parser.lean.

Run#

With devenv installed:

devenv shell
build
run

You can also run commands directly without entering the shell:

devenv test
devenv shell -- build
devenv shell -- run

The executable supports a REPL and file execution:

devenv shell -- lake exe mlang
devenv shell -- lake exe mlang examples/samples.mlg
devenv shell -- lake exe mlang --demo

Current syntax:

expr ::= let name = expr in expr
       | if expr then expr else expr
       | try expr with expr
       | fun (name : type) => expr
       | expr = expr
       | expr + expr
       | expr - expr
       | expr * expr
       | expr expr
       | (expr)
       | true | false | 123 | name

type ::= Int | Bool | type -> type | (type)

Expressions are checked as Type ! Effects. Pure expressions get {}; division carries {Error} implicitly. try ... with ... handles Error and removes it from the resulting effect set when recovered locally.

The REPL parses, typechecks, and evaluates one expression per line. Use :quit to exit.

Next steps#

• persist top-level bindings across REPL entries
• add recursive functions
• add algebraic data types and pattern matching
• compile to a bytecode VM or another backend