mlang#

A small functional language prototype written in Lean 4.

Current scope:

• integer, decimal, and boolean literals
• variables
• let
• if
• typed lambdas
• function application
• decimal arithmetic with implicit Int promotion
• 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 | 1.23 | "text" | name

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

type ::= Int | Decimal | LazyReal | 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. Plain numeric literals now default to Rational, so 1, 1.25, 1 + 2, and 5 / 2 are all rational values unless you explicitly cast them. 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 -> Rational -> Data ! {Error}

• asInt : Data -> Int ! {Error}

• asDecimal : Data -> Decimal ! {Error}

• asString : Data -> String ! {Error}

• asBool : Data -> Bool ! {Error}

• toInt : Rational -> Int ! {Error}

• toDecimal : Rational -> Decimal ! {Error}

• toJson : Data -> String

• toNickel : Data -> String

• rationalStability : Rational -> Stability

• decimalStability : Rational -> Stability

• sqrt : Decimal -> LazyReal ! {Error}

• pi : LazyReal

• lazyRationalStability : LazyReal -> Stability

• lazyDecimalStability : LazyReal -> Stability

• approx : LazyReal -> Rational -> Rational ! {Error}

• bounds : LazyReal -> Rational -> Data ! {Error}

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
• decimals
• strings
• arrays
• records

Exact rational values are supported in native literals and in Data values coming from JSON or Nickel.

Native Data literals are also supported directly in mlang:

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

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

LazyReal represents process-like numeric values that are observed through refinement. The current implementation supports decimal input to sqrt, while approx and bounds observe lazies as rationals:

let r = sqrt 2.0
approx r 4
bounds r 4
approx pi 4
toDecimal (approx pi 4)

Ordinary arithmetic lifts over LazyReal, so expressions like sqrt 2.0 + 3.0 stay lazy until observed with approx or bounds.

Stability observations classify how a number settles under rational and decimal observation:

rationalStability (1 / 3)      -- Immediate
decimalStability (1 / 3)       -- Periodic
lazyRationalStability pi       -- Refining
lazyDecimalStability (sqrt 2)  -- Refining

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