commit e28dea8dbba00607a1670757d0f37b84b9b8a6e9
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Sun, 3 Dec 2023 11:09:19 -0800
Simple dependently typed elaborator
Diffstat:
| A | dep.ml | | | 216 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
1 file changed, 216 insertions(+), 0 deletions(-)
diff --git a/dep.ml b/dep.ml
@@ -0,0 +1,216 @@
+type ident = string
+
+type index = int
+type level = int
+
+type surf =
+| SVar of ident (* x *)
+| SAnn of surf * surf (* t : u *)
+| SLet of patt * surf * surf (* let p = t in u *)
+| SType (* Type *)
+| SPi of ident * surf * surf (* (x : t) -> u *)
+| SLam of patt * surf (* λp. t *)
+| SApp of surf * surf (* t u *)
+| SNat (* Nat *)
+| SLit of int (* 0, 1, ... *)
+| SAdd of surf * surf (* t + u *)
+and patt =
+| PVar of ident (* x *)
+| PAnn of patt * surf (* p : t *)
+
+type core =
+| CVar of index
+| CLet of core * core
+| CType
+| CPi of core * core
+| CLam of core
+| CApp of core * core
+| CNat
+| CLit of int
+| CAdd of core * core
+
+type value =
+| VVar of level
+| VType
+| VPi of value * closure
+| VLam of closure
+| VApp of value * value
+| VNat
+| VLit of int
+| VAdd of value * value
+and closure = environ * core
+and environ = value list
+
+let rec eval env = function
+| CVar i -> List.nth env i
+| CLet (a, b) -> eval (eval env a :: env) b
+| CType -> VType
+| CPi (dom, cod) -> VPi (eval env dom, (env, cod))
+| CLam body -> VLam (env, body)
+| CApp (f, a) ->
+ begin match eval env f, eval env a with
+ | VLam clo, va -> apply clo va
+ | vf, va -> VApp (vf, va)
+ end
+| CNat -> VNat
+| CLit n -> VLit n
+| CAdd (a, b) ->
+ begin match eval env a, eval env b with
+ | VLit m, VLit n -> VLit (m + n)
+ | va, vb -> VAdd (va, vb)
+ end
+
+and apply (env, c) v = eval (v :: env) c
+
+let rec quote l = function
+| VVar i -> CVar (l - i - 1)
+| VType -> CType
+| VPi (dom, cod) -> CPi (quote l dom, quote (l + 1) (apply cod (VVar l)))
+| VLam clo -> CLam (quote (l + 1) (apply clo (VVar l)))
+| VApp (f, a) -> CApp (quote l f, quote l a)
+| VNat -> CNat
+| VLit n -> CLit n
+| VAdd (a, b) -> CAdd (quote l a, quote l b)
+
+let rec conv l a b = match a, b with
+| VVar x, VVar y -> x = y
+| VType, VType -> true
+| VPi (dom0, cod0), VPi (dom1, cod1) -> conv l dom0 dom1
+ && conv (l + 1) (apply cod0 (VVar l)) (apply cod1 (VVar l))
+(* no β nor η for lams? *)
+| VApp (a0, a1), VApp (b0, b1) -> conv l a0 b0 && conv l a1 b1
+| VNat, VNat -> true
+| VLit m, VLit n -> m = n
+| VAdd (a0, a1), VAdd (b0, b1) -> conv l a0 b0 && conv l a1 b1
+| _, _ -> false
+
+type context = {env: environ; free: (ident * value) list}
+
+let let_bind ctx x t v = {
+ env = v :: ctx.env;
+ free = (x, t) :: ctx.free;
+}
+
+let var_bind ctx x t = {
+ env = VVar (List.length ctx.env) :: ctx.env;
+ free = (x, t) :: ctx.free;
+}
+
+let rec check (ctx: context) s t = match s, t with
+| SLet (p, s0, s1), t ->
+ let (c0, t0, x) = infer_with_patt ctx s0 p in
+ let v0 = eval ctx.env c0 in
+ let c1 = check (let_bind ctx x t0 v0) s1 t in
+ CLet (c0, c1)
+| SLam (p, s), VPi (dom, cod) ->
+ let x = check_patt ctx p dom in
+ let c = check (var_bind ctx x dom) s (apply cod (VVar (List.length ctx.env))) in
+ CLam c
+| s, t ->
+ let (c, u) = infer ctx s in
+ if conv (List.length ctx.env) t u then c else failwith "type error"
+
+and infer (ctx: context) = function
+| SVar x ->
+ let rec go i = function
+ | [] -> failwith ("variable '" ^ x ^ "' out of scope")
+ | (y, v) :: rest -> if x = y then (CVar i, v) else go (i + 1) rest in
+ go 0 ctx.free
+| SAnn (s0, s1) ->
+ let c1 = check ctx s1 VType in
+ let v1 = eval ctx.env c1 in
+ let c0 = check ctx s0 v1 in
+ (c0, v1)
+| SLet (p, s0, s1) ->
+ let (c0, t0, x) = infer_with_patt ctx s0 p in
+ let v0 = eval ctx.env c0 in
+ let (c1, t1) = infer (let_bind ctx x t0 v0) s1 in
+ (CLet (c0, c1), t1)
+| SType -> (CType, VType)
+| SPi (x, s0, s1) ->
+ let c0 = check ctx s0 VType in
+ let t0 = eval ctx.env c0 in
+ let c1 = check (var_bind ctx x t0) s1 VType in
+ (CPi (c0, c1), VType)
+| SLam (p, s) ->
+ let (x, t) = infer_patt ctx p in
+ let (c, u) = infer (var_bind ctx x t) s in
+ (CLam c, VPi (t, (ctx.env, quote (List.length ctx.env) u)))
+| SApp (s0, s1) ->
+ let (c0, t0) = infer ctx s0 in
+ begin match t0 with
+ | VPi (dom, cod) ->
+ let c1 = check ctx s1 dom in
+ (CApp (c0, c1), apply cod (eval ctx.env c1))
+ | _ -> failwith "expected function type in application"
+ end
+| SNat -> (CNat, VType)
+| SLit n -> (CLit n, VNat)
+| SAdd (s0, s1) ->
+ let c0 = check ctx s0 VNat in
+ let c1 = check ctx s1 VNat in
+ (CAdd (c0, c1), VNat)
+
+and infer_with_patt ctx s0 = function
+| PVar x -> let (c0, t0) = infer ctx s0 in (c0, t0, x)
+| PAnn (q, s1) ->
+ let c1 = check ctx s1 VType in
+ let v1 = eval ctx.env c1 in
+ let x = check_patt ctx q v1 in
+ let c0 = check ctx s0 v1 in
+ (c0, v1, x)
+
+and check_patt ctx p t = match p with
+| PVar x -> x
+| PAnn (q, s) ->
+ let c = check ctx s VType in
+ let v = eval ctx.env c in
+ if conv (List.length ctx.env) t v then
+ check_patt ctx q t
+ else
+ failwith "patt_check fail"
+
+and infer_patt ctx = function
+| PVar _ -> failwith "can not infer type for variable pattern"
+| PAnn (q, s) ->
+ let c = check ctx s VType in
+ let v = eval ctx.env c in
+ let x = check_patt ctx q v in
+ (x, v)
+
+let rec string_of_core c =
+ let go = function
+ | CVar i -> "$" ^ string_of_int i
+ | CLet (a, b) -> "let" ^ string_of_core a ^ string_of_core b
+ | CType -> "Type"
+ | CPi (a, b) -> "Π" ^ string_of_core a ^ string_of_core b
+ | CLam a -> "λ" ^ string_of_core a
+ | CApp (a, b) -> string_of_core a ^ string_of_core b
+ | CNat -> "Nat"
+ | CLit n -> string_of_int n
+ | CAdd (a, b) -> string_of_core a ^ "+" ^ string_of_core b in
+ "(" ^ go c ^ ")"
+
+
+
+let s = SLet (
+ PVar "f",
+ SLam (
+ PAnn (
+ PVar "n",
+ SApp (
+ SLam (
+ PAnn (PVar "α", SType),
+ SNat
+ ),
+ SType
+ )
+ ),
+ SAdd (SLit 3, SVar "n")
+ ),
+ SApp (SVar "f", SLit 4)
+)
+let (c, t) = infer {env = []; free = []} s
+let () = print_endline (string_of_core c)
+let () = print_endline (string_of_core (quote 0 t))
+let () = print_endline (string_of_core (quote 0 (eval [] c)))
