nandi.uk
This repository has no description
1namespace Mlang
2
3abbrev Name := String
4
5inductive Effect where
6 | error : Effect
7 deriving Repr, Inhabited, BEq
8
9abbrev Effects := List Effect
10
11def Effects.contains (effects : Effects) (effect : Effect) : Bool :=
12 effects.any (· == effect)
13
14def Effects.insert (effects : Effects) (effect : Effect) : Effects :=
15 if effects.contains effect then effects else effect :: effects
16
17def Effects.union (lhs rhs : Effects) : Effects :=
18 rhs.foldl Effects.insert lhs
19
20def Effects.erase (effects : Effects) (target : Effect) : Effects :=
21 effects.filter (· != target)
22
23def Effects.render : Effects → String
24 | [] => "{}"
25 | effects =>
26 let names := effects.reverse.map (fun
27 | .error => "Error")
28 "{" ++ String.intercalate ", " names ++ "}"
29
30inductive Ty where
31 | int : Ty
32 | bool : Ty
33 | funTy : Ty → Effects → Ty → Ty
34 deriving Repr, Inhabited, BEq
35
36inductive Expr where
37 | int : Int → Expr
38 | bool : Bool → Expr
39 | var : Name → Expr
40 | add : Expr → Expr → Expr
41 | sub : Expr → Expr → Expr
42 | mul : Expr → Expr → Expr
43 | div : Expr → Expr → Expr
44 | eq : Expr → Expr → Expr
45 | letE : Name → Expr → Expr → Expr
46 | ifE : Expr → Expr → Expr → Expr
47 | tryE : Expr → Expr → Expr
48 | lam : Name → Ty → Expr → Expr
49 | app : Expr → Expr → Expr
50 deriving Repr, Inhabited
51
52inductive Value where
53 | int : Int → Value
54 | bool : Bool → Value
55 | closure : Name → Expr → List (Name × Value) → Value
56 deriving Repr, Inhabited
57
58abbrev Env := List (Name × Value)
59
60inductive RuntimeError where
61 | unboundVariable : Name → RuntimeError
62 | typeError : String → RuntimeError
63 | divisionByZero : RuntimeError
64 deriving Repr, Inhabited
65
66abbrev EvalM := Except RuntimeError
67
68def Env.lookup (env : Env) (name : Name) : Option Value :=
69 match env with
70 | [] => none
71 | (n, v) :: rest => if n = name then some v else rest.lookup name
72
73def expectInt : Value → EvalM Int
74 | .int n => .ok n
75 | _ => .error (.typeError "expected an integer")
76
77def expectBool : Value → EvalM Bool
78 | .bool b => .ok b
79 | _ => .error (.typeError "expected a boolean")
80
81partial def eval (env : Env) : Expr → EvalM Value
82 | .int n => .ok (.int n)
83 | .bool b => .ok (.bool b)
84 | .var name =>
85 match env.lookup name with
86 | some v => .ok v
87 | none => .error (.unboundVariable name)
88 | .add lhs rhs => do
89 let l ← expectInt (← eval env lhs)
90 let r ← expectInt (← eval env rhs)
91 pure (.int (l + r))
92 | .sub lhs rhs => do
93 let l ← expectInt (← eval env lhs)
94 let r ← expectInt (← eval env rhs)
95 pure (.int (l - r))
96 | .mul lhs rhs => do
97 let l ← expectInt (← eval env lhs)
98 let r ← expectInt (← eval env rhs)
99 pure (.int (l * r))
100 | .div lhs rhs => do
101 let l ← expectInt (← eval env lhs)
102 let r ← expectInt (← eval env rhs)
103 if r = 0 then
104 .error .divisionByZero
105 else
106 pure (.int (l / r))
107 | .eq lhs rhs => do
108 let l ← expectInt (← eval env lhs)
109 let r ← expectInt (← eval env rhs)
110 pure (.bool (l = r))
111 | .letE name value body => do
112 let value' ← eval env value
113 eval ((name, value') :: env) body
114 | .ifE cond thenBranch elseBranch => do
115 let c ← expectBool (← eval env cond)
116 if c then
117 eval env thenBranch
118 else
119 eval env elseBranch
120 | .tryE body handler =>
121 match eval env body with
122 | .ok value => .ok value
123 | .error _ => eval env handler
124 | .lam param _ body =>
125 pure (.closure param body env)
126 | .app fn arg => do
127 let fnVal ← eval env fn
128 let argVal ← eval env arg
129 match fnVal with
130 | .closure param body closureEnv =>
131 eval ((param, argVal) :: closureEnv) body
132 | _ =>
133 .error (.typeError "expected a function")
134
135def renderValue : Value → String
136 | .int n => toString n
137 | .bool b => toString b
138 | .closure _ _ _ => "<closure>"
139
140abbrev TyEnv := List (Name × Ty)
141
142structure Judgment where
143 ty : Ty
144 effects : Effects
145 deriving Repr, Inhabited
146
147inductive TypeError where
148 | unboundVariable : Name → TypeError
149 | mismatch : Ty → Ty → TypeError
150 | expectedFunction : Ty → TypeError
151 deriving Repr, Inhabited
152
153abbrev CheckM := Except TypeError
154
155def TyEnv.lookup (env : TyEnv) (name : Name) : Option Ty :=
156 match env with
157 | [] => none
158 | (n, ty) :: rest => if n = name then some ty else rest.lookup name
159
160def ensureType (expected actual : Ty) : CheckM Unit :=
161 if expected == actual then
162 pure ()
163 else
164 throw (.mismatch expected actual)
165
166def pureJudgment (ty : Ty) : Judgment :=
167 { ty := ty, effects := [] }
168
169partial def inferType (env : TyEnv) : Expr → CheckM Judgment
170 | .int _ => pure (pureJudgment .int)
171 | .bool _ => pure (pureJudgment .bool)
172 | .var name =>
173 match env.lookup name with
174 | some ty => pure (pureJudgment ty)
175 | none => throw (.unboundVariable name)
176 | .add lhs rhs
177 | .sub lhs rhs
178 | .mul lhs rhs => do
179 let lhsJ ← inferType env lhs
180 let rhsJ ← inferType env rhs
181 ensureType .int lhsJ.ty
182 ensureType .int rhsJ.ty
183 pure { ty := .int, effects := lhsJ.effects.union rhsJ.effects }
184 | .div lhs rhs => do
185 let lhsJ ← inferType env lhs
186 let rhsJ ← inferType env rhs
187 ensureType .int lhsJ.ty
188 ensureType .int rhsJ.ty
189 pure {
190 ty := .int
191 effects := (lhsJ.effects.union rhsJ.effects).insert .error
192 }
193 | .eq lhs rhs => do
194 let lhsJ ← inferType env lhs
195 let rhsJ ← inferType env rhs
196 ensureType .int lhsJ.ty
197 ensureType .int rhsJ.ty
198 pure { ty := .bool, effects := lhsJ.effects.union rhsJ.effects }
199 | .letE name value body => do
200 let valueJ ← inferType env value
201 let bodyJ ← inferType ((name, valueJ.ty) :: env) body
202 pure {
203 ty := bodyJ.ty
204 effects := valueJ.effects.union bodyJ.effects
205 }
206 | .ifE cond thenBranch elseBranch => do
207 let condJ ← inferType env cond
208 ensureType .bool condJ.ty
209 let thenJ ← inferType env thenBranch
210 let elseJ ← inferType env elseBranch
211 ensureType thenJ.ty elseJ.ty
212 pure {
213 ty := thenJ.ty
214 effects := condJ.effects.union (thenJ.effects.union elseJ.effects)
215 }
216 | .tryE body handler => do
217 let bodyJ ← inferType env body
218 let handlerJ ← inferType env handler
219 ensureType bodyJ.ty handlerJ.ty
220 pure {
221 ty := bodyJ.ty
222 effects := (bodyJ.effects.erase .error).union handlerJ.effects
223 }
224 | .lam param paramTy body => do
225 let bodyJ ← inferType ((param, paramTy) :: env) body
226 pure (pureJudgment (.funTy paramTy bodyJ.effects bodyJ.ty))
227 | .app fn arg => do
228 let fnJ ← inferType env fn
229 let argJ ← inferType env arg
230 match fnJ.ty with
231 | .funTy paramTy latentEffects resultTy =>
232 ensureType paramTy argJ.ty
233 pure {
234 ty := resultTy
235 effects := fnJ.effects.union (argJ.effects.union latentEffects)
236 }
237 | _ =>
238 throw (.expectedFunction fnJ.ty)
239
240def renderType : Ty → String
241 | .int => "Int"
242 | .bool => "Bool"
243 | .funTy lhs effects rhs => s!"({renderType lhs} -> {renderType rhs} ! {effects.render})"
244
245def renderJudgment (judgment : Judgment) : String :=
246 s!"{renderType judgment.ty} ! {judgment.effects.render}"
247
248def sampleProgram : Expr :=
249 .letE "inc" (.lam "x" .int (.add (.var "x") (.int 1)))
250 (.app (.var "inc") (.int 41))
251
252def lexicalScopeProgram : Expr :=
253 .letE "x" (.int 10)
254 (.letE "f" (.lam "y" .int (.add (.var "x") (.var "y")))
255 (.letE "x" (.int 100)
256 (.app (.var "f") (.int 5))))
257
258def conditionalProgram : Expr :=
259 .ifE (.eq (.mul (.int 6) (.int 7)) (.int 42))
260 (.int 1)
261 (.int 0)
262
263end Mlang