commit 55f4454813f79263221e199532d0865c602ba94e
parent ef23c70fab3f52ab642184b3dd7fe3c26b9c36e7
Author: Robert Russell <robert@rr3.xyz>
Date: Mon, 26 Aug 2024 15:21:07 -0700
Clean up, add examples, and add README
Diffstat:
9 files changed, 37 insertions(+), 383 deletions(-)
diff --git a/README b/README
@@ -0,0 +1,9 @@
+Dependently-typed lambda calculus with Type-in-Type, general (mutual)
+recursive let bindings, (non-recursive) data types and pattern matching, and
+a built-in Nat type with some arthimetic and comparison operations
+
+This project is somewhat incomplete: implicit arguments are only half
+implemented, dependent pattern matching is broken, pattern matching
+on built-in Nats is not implemented.
+
+See the examples in the examples directory.
diff --git a/dep/dep.ml b/dep/dep.ml
@@ -1,216 +0,0 @@
-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)))
diff --git a/examples/church b/examples/church.dtlc
diff --git a/examples/list b/examples/list
@@ -1,10 +0,0 @@
-UnaryNat: Type := rec #{
- @Z;
- @S UnaryNat;
-};
-@S (@S @Z): UnaryNat
-\List: Type -> Type := rec fn A => #{
-\ @nil;
-\ @cons A, List A;
-\};
-\@cons 1 @nil : List Nat
diff --git a/examples/list.dtlc b/examples/list.dtlc
@@ -0,0 +1,26 @@
+\ Church-encoded unary natural numbers (pattern matching on built-in Nats is
+\ not implemented)
+UNat: Type := [M: Type, M, M -> M] -> M;
+zero: UNat := fn M, z, s => z;
+succ: UNat -> UNat := fn n => fn M, z, s => s (n M z s);
+
+\ Conversion from UNat to built-in Nat type for pretty printing
+toNat: UNat -> Nat := fn n => n Nat 0 (fn m => m + 1);
+
+\ Polymorphic Church-encoded lists
+List: Type -> Type := fn A =>
+ [M: Type, M, [A, M] -> M] -> M;
+nil: [A: Type] -> List A := fn A =>
+ fn M, n, c => n;
+cons: [A: Type, A, List A] -> List A := rec fn A, hd, tl =>
+ fn M, n, c => c hd (tl M n c);
+
+\ Example operations on lists
+length: [A: Type, List A] -> UNat := fn A, l =>
+ l UNat zero (fn _, n => succ n);
+map: [A: Type, B: Type, A -> B, List A] -> List B := fn A, B, f, l =>
+ l (List B) (nil B) (fn a, tl' => cons B (f a) tl');
+
+l0: List UNat := cons UNat zero (cons UNat zero (cons UNat zero (nil UNat)));
+l1: List UNat := map UNat UNat succ l0;
+(map UNat Nat toNat l0, map UNat Nat toNat l1)
diff --git a/examples/nat.dtlc b/examples/nat.dtlc
@@ -0,0 +1 @@
+(5 + 3, 5 - 3, 5 * 3, 5 / 3, 5 % 3, 5 < 3, 5 = 3, 5 > 3)
+\ No newline at end of file
diff --git a/lam/lam.ml b/lam/lam.ml
@@ -1,59 +0,0 @@
-type idx = int
-
-type term =
- | TVar of idx
- | TLam of term
- | TApp of term * term
- | TLet of term * term
- | TInt of int
- | TAdd of term * term
- | TMul of term * term
-
-let rec string_of_term = function
- | TVar i -> "$" ^ string_of_int i
- | TLam t -> "(λ" ^ string_of_term t ^ ")"
- | TApp (t, u) -> "(" ^ string_of_term t ^ ") (" ^ string_of_term u ^ ")"
- | TLet (t, u) -> "(" ^ string_of_term t ^ "; " ^ string_of_term u ^ ")"
- | TInt i -> string_of_int i
- | TAdd (t, u) -> "(" ^ string_of_term t ^ " + " ^ string_of_term u ^ ")"
- | TMul (t, u) -> "(" ^ string_of_term t ^ " * " ^ string_of_term u ^ ")"
-
-type value =
- | VLam of env * term
- | VInt of int
-and env = value list
-
-let rec string_of_value = function
- | VLam (e, t) -> String.concat ", " (List.map string_of_value e) ^ " ⊢ " ^ string_of_term t
- | VInt i -> string_of_int i
-
-let rec lookup e i =
- match e, i with
- | v :: _, 0 -> v
- | _ :: vs, j -> lookup vs j
- | [], _ -> failwith "variable not in scope"
-
-let rec eval e = function
- | TVar i -> lookup e i
- | TLam t -> VLam (e, t)
- | TApp (t, u) -> (
- match eval e t, eval e u with
- | VLam (c, b), v -> eval (v :: c) b
- | _, _ -> failwith "can only apply functions"
- )
- | TLet (t, u) -> eval (eval e t :: e) u
- | TInt i -> VInt i
- | TAdd (t, u) -> (
- match eval e t, eval e u with
- | VInt i, VInt j -> VInt (i + j)
- | _, _ -> failwith "can only add ints"
- )
- | TMul (t, u) -> (
- match eval e t, eval e u with
- | VInt i, VInt j -> VInt (i * j)
- | _, _ -> failwith "can only multiply ints"
- )
-
-let t = TLet (TLam (TAdd (TInt 3, TVar 0)), TApp (TVar 0, TInt 4))
-let () = print_endline (string_of_term t)
-let () = print_endline (string_of_value (eval [] t))
diff --git a/porig.ml b/porig.ml
@@ -1,66 +0,0 @@
-(* TODO: Generalize to partial add and mul? *)
-module type Porig = sig
- type t
- val zero : t
- val one : t
- val default : t
- val add : t -> t -> t
- val mul : t -> t -> t
- val leq : t -> t -> bool
- val lub : t -> t -> t option
- val to_string : t -> string
-end
-
-(* TODO: How does compilation work with this porig? What gets erased? *)
-module Intuitionistic: Porig = struct
- type t = Zero
-
- let zero = Zero
- let one = Zero
- let default = Zero
-
- let add Zero Zero = Zero
-
- let mul Zero Zero = Zero
-
- let leq Zero Zero = true
-
- let lub Zero Zero = Zero
-
- let to_string Zero = "0"
-end
-
-(* TODO: module DiscreteBoolean: Porig = struct ... end*)
-(* TODO: module TotalBoolean: Porig = struct ... end*)
-
-module NoneOneTons: Porig = struct
- type t = Zero | One | Omega
-
- let zero = Zero
- let one = One
- let default = Omega
-
- let add a b = match a, b with
- | Zero, b -> b
- | a, Zero -> a
- | _, _ -> Omega
-
- let mul a b = match a, b with
- | Zero, _ -> Zero
- | _, Zero -> Zero
- | One, b -> b
- | _, _ -> Omega
-
- let leq a b = a = b ||
- match a, b with
- | Zero, Omega -> true
- | One, Omega -> true
- | _, _ -> false
-
- let lub a b = if a = b then a else Omega
-
- let to_string = function
- | Zero -> "0"
- | One -> "1"
- | Omega -> "ω"
-end
diff --git a/repr.ml b/repr.ml
@@ -1,32 +0,0 @@
-(* TODO: functions/closures *)
-(* TODO: packing control *)
-
-type repr =
-| Constant of constant
-| Uniform of uniform
-| NonUniform of nonuniform
-and constant =
-| CAlign of constant * term1 (* The term has type Nat1. *)
-| CPtr
-| CBits of term1 (* The term has type Nat1. *)
-| CData of constant array
-| CTuple of constant array
-| CArray of constant * term1 (* The term has type Nat1. *)
-and uniform =
-| UConstant of constant
-| UAlign of uniform * term1 (* The term has type Nat1. *)
-| UData of uniform array
-| UTuple of (uniform * term1) array * uniform
-| UArray of uniform * term1 (* The term has type ↑Nat0. *)
-and nonuniform =
-| NUniform of uniform
-| NTuple of (uniform * term1) array * nonuniform
- (* The array is of (repr, lifted type) pairs, and each repr is formed in a
- * context with variables of the preceding lifted types bound. E.g., if
- * type T has uniform repr R and type Nat0 has repr CBits 64, then
- * #(n: Nat0, a: Arr T n) has repr
- * NTuple ([|(CBits 64, ↑Nat0)|], n: ↑Nat0 ⊢ UArray (R, n)). *)
-
-(* This isn't quite right, because we also need to allow for representation
- * variables. The above types need to be embedded in the term1 syntax, just
- * like how we embed types in terms. *)
