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
• strings
• native parsed data values
• lexical closures
• hand-written lexer and parser
• static type checker
• implicit effect tracking
• builtin file IO
• builtin Nickel evaluation

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 --eval "1 + 2"
devenv shell -- lake exe mlang examples/samples.mlg

Current syntax:

expr ::= let name = expr in expr
       | if expr then expr else expr
       | try expr with name => expr
       | pmap name in expr => expr
       | -> expr ident*
       | fun (name : type) => expr
       | expr = expr
       | expr + expr
       | expr - expr
       | expr * expr
       | expr expr
       | [expr, ...]
       | { key = expr, ... }
       | null
       | (expr)
       | true | false | 123 | "text" | name

program ::= expr (';' expr)*

type ::= Int | Bool | String | Data | List | Result | Error | type -> type | (type)

Inside the REPL, there is also a top-level binding form:

repl ::= let name = expr

Bare REPL bindings persist across later entries, so you can write:

let x = 42
x + 1

Expressions are checked as Type ! Effects. Pure expressions get {}; division carries {Error} implicitly. readFile is a builtin with type String -> String ! {IO, Error}. readFileNickel is a builtin with type String -> Data ! {IO, Error}. parseNickel is a builtin with type String -> Data ! {Error} and is backed by the real Nickel Rust crate. Nickel source is evaluated on the host side and converted back into mlang Data. Parsed data inspection is available through:

• httpGet : String -> String ! {IO, Error}

• parseJson : String -> Data ! {Error}

• get : Data -> String -> Data ! {Error}

• at : Data -> Int -> Data ! {Error}

• asInt : Data -> Int ! {Error}

• asString : Data -> String ! {Error}

• asBool : Data -> Bool ! {Error}

• toJson : Data -> String

• toNickel : Data -> String

httpGet is implemented through a thin Rust host library plus a small C shim for Lean FFI. The Rust layer uses a real HTTP client crate rather than spawning an external tool. try ... with name => ... handles Error, binds the caught error as an Error value, and removes Error from the resulting effect set when recovered locally.

The host-side Nickel bridge currently maps evaluated Nickel values back into mlang data for:

• null
• booleans
• integers
• strings
• arrays
• records

Non-integer numeric Nickel values are not supported yet by mlang's Data model.

Native Data literals are also supported directly in mlang:

{ answer = 42, flags = [true, false], note = "ok", empty = null }

Fields and array elements may be Int, Bool, String, or existing Data expressions.

pmap name in expr => body expects expr to evaluate to a native Data array. It evaluates body concurrently for each element bound to name, preserves input order, and returns a native List of native Result values instead of failing the whole traversal.

There is also a thread-first form that desugars statically to nested application:

-> "examples/sample.ncl" readFileNickel (get "answer")

Parallel collection mapping example:

pmap x in parseNickel "[{ answer = 1 }, { missing = 2 }, { answer = 3 }]"
  => get x "answer"

Files and REPL entries may contain multiple expressions separated by ;. Each expression is parsed, typechecked, evaluated, and printed in order. REPL-specific bare let bindings persist across later entries. devenv shell -- run now launches a Rust rustyline frontend for the REPL, while the Lean binary still handles evaluation. Use :quit to exit the REPL.

The checked-in sample program is examples/samples.mlg, which now contains the old demo coverage as semicolon-separated expressions, including file IO, Nickel parsing, threading, pmap, local error handling, and an HTTP fetch. It reads from examples/sample.ncl.

A separate HTTP example is examples/http.mlg.

Next steps#

• add recursive functions
• add algebraic data types and pattern matching
• compile to a bytecode VM or another backend