# 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](/home/nandi/code/mlang/Mlang/Interpreter.lean:1).
The parser lives in [Mlang/Parser.lean](/home/nandi/code/mlang/Mlang/Parser.lean:1).

## Run

With `devenv` installed:

```bash
devenv shell
build
run
```

You can also run commands directly without entering the shell:

```bash
devenv test
devenv shell -- build
devenv shell -- run
```

The executable supports a REPL and file execution:

```bash
devenv shell -- lake exe mlang
devenv shell -- lake exe mlang --eval "1 + 2"
devenv shell -- lake exe mlang examples/samples.mlg
```

Current syntax:

```text
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:

```text
repl ::= let name = expr
```

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

```mlang
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`:

```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:

```mlang
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:

```mlang
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:

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

Parallel collection mapping example:

```mlang
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](/home/nandi/code/mlang/examples/samples.mlg:1), 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](/home/nandi/code/mlang/examples/sample.ncl:1).

A separate HTTP example is [examples/http.mlg](/home/nandi/code/mlang/examples/http.mlg:1).

## Next steps

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