nandi.uk
This repository has no description
4.9 kB
150 lines
1# mlang
2
3A small functional language prototype written in Lean 4.
4
5Current scope:
6
7- integer and boolean literals
8- variables
9- `let`
10- `if`
11- typed lambdas
12- function application
13- integer arithmetic
14- integer division
15- strings
16- native parsed data values
17- lexical closures
18- hand-written lexer and parser
19- static type checker
20- implicit effect tracking
21- builtin file IO
22- builtin Nickel evaluation
23
24The interpreter lives in [Mlang/Interpreter.lean](/home/nandi/code/mlang/Mlang/Interpreter.lean:1).
25The parser lives in [Mlang/Parser.lean](/home/nandi/code/mlang/Mlang/Parser.lean:1).
26
27## Run
28
29With `devenv` installed:
30
31```bash
32devenv shell
33build
34run
35```
36
37You can also run commands directly without entering the shell:
38
39```bash
40devenv test
41devenv shell -- build
42devenv shell -- run
43```
44
45The executable supports a REPL and file execution:
46
47```bash
48devenv shell -- lake exe mlang
49devenv shell -- lake exe mlang --eval "1 + 2"
50devenv shell -- lake exe mlang examples/samples.mlg
51```
52
53Current syntax:
54
55```text
56expr ::= let name = expr in expr
57 | if expr then expr else expr
58 | try expr with name => expr
59 | pmap name in expr => expr
60 | -> expr ident*
61 | fun (name : type) => expr
62 | expr = expr
63 | expr + expr
64 | expr - expr
65 | expr * expr
66 | expr expr
67 | [expr, ...]
68 | { key = expr, ... }
69 | null
70 | (expr)
71 | true | false | 123 | "text" | name
72
73program ::= expr (';' expr)*
74
75type ::= Int | Bool | String | Data | List | Result | Error | type -> type | (type)
76```
77
78Inside the REPL, there is also a top-level binding form:
79
80```text
81repl ::= let name = expr
82```
83
84Bare REPL bindings persist across later entries, so you can write:
85
86```mlang
87let x = 42
88x + 1
89```
90
91Expressions 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:
92
93- `httpGet : String -> String ! {IO, Error}`
94- `parseJson : String -> Data ! {Error}`
95
96- `get : Data -> String -> Data ! {Error}`
97- `at : Data -> Int -> Data ! {Error}`
98- `asInt : Data -> Int ! {Error}`
99- `asString : Data -> String ! {Error}`
100- `asBool : Data -> Bool ! {Error}`
101- `toJson : Data -> String`
102- `toNickel : Data -> String`
103
104`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.
105`try ... with name => ...` handles `Error`, binds the caught error as an `Error` value, and removes `Error` from the resulting effect set when recovered locally.
106
107The host-side Nickel bridge currently maps evaluated Nickel values back into `mlang` data for:
108- `null`
109- booleans
110- integers
111- strings
112- arrays
113- records
114
115Non-integer numeric Nickel values are not supported yet by `mlang`'s `Data` model.
116
117Native `Data` literals are also supported directly in `mlang`:
118
119```mlang
120{ answer = 42, flags = [true, false], note = "ok", empty = null }
121```
122
123Fields and array elements may be `Int`, `Bool`, `String`, or existing `Data` expressions.
124
125`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.
126
127There is also a thread-first form that desugars statically to nested application:
128
129```mlang
130-> "examples/sample.ncl" readFileNickel (get "answer")
131```
132
133Parallel collection mapping example:
134
135```mlang
136pmap x in parseNickel "[{ answer = 1 }, { missing = 2 }, { answer = 3 }]"
137 => get x "answer"
138```
139
140Files 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.
141
142The 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).
143
144A separate HTTP example is [examples/http.mlg](/home/nandi/code/mlang/examples/http.mlg:1).
145
146## Next steps
147
148- add recursive functions
149- add algebraic data types and pattern matching
150- compile to a bytecode VM or another backend