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