diff options
author | William Carroll <wpcarro@gmail.com> | 2022-10-12T17·22-0700 |
---|---|---|
committer | wpcarro <wpcarro@gmail.com> | 2022-10-24T17·42+0000 |
commit | a8876a4cdaaf0a1f051fefad436e08d983b402e2 (patch) | |
tree | dfd6f25617691d866d340357e1b808c19ecfdc6a /users/wpcarro/scratch/compiler/types.ml | |
parent | 5bd0e723c13b8a41bfba442bd8ef5351e31099e6 (diff) |
feat(wpcarro/scratch): Implement "Algorithm W" r/5194
I've been wanting to grok Haskell-style type inference for awhile, so instead of just watching conference talks and reading papers about it, I've decided to attempt to implement it to more readily test my understanding of it. Change-Id: I69261202a3d74d55c6e38763d7ddfec73c392465 Reviewed-on: https://cl.tvl.fyi/c/depot/+/6988 Tested-by: BuildkiteCI Reviewed-by: wpcarro <wpcarro@gmail.com> Autosubmit: wpcarro <wpcarro@gmail.com>
Diffstat (limited to 'users/wpcarro/scratch/compiler/types.ml')
-rw-r--r-- | users/wpcarro/scratch/compiler/types.ml | 76 |
1 files changed, 76 insertions, 0 deletions
diff --git a/users/wpcarro/scratch/compiler/types.ml b/users/wpcarro/scratch/compiler/types.ml new file mode 100644 index 000000000000..99f35cd5a57d --- /dev/null +++ b/users/wpcarro/scratch/compiler/types.ml @@ -0,0 +1,76 @@ +type literal = LiteralInt of int | LiteralBool of bool + +(* Lambda Calculus definition *) +type value = + | ValueLiteral of literal + | ValueVariable of string + | ValueFunction of string * value + | ValueApplication of value * value + | ValueVarApplication of string * value + | ValueBinder of string * value * value + +let rec debug_value (x : value) : string = + match x with + | ValueLiteral (LiteralInt x) -> + Printf.sprintf "Int %d" x + | ValueLiteral (LiteralBool x) -> + Printf.sprintf "Bool %b" x + | ValueVariable x -> + Printf.sprintf "Var %s" x + | ValueFunction (name, x) -> + Printf.sprintf "Fn %s %s" name (debug_value x) + | ValueApplication (f, x) -> + Printf.sprintf "App %s %s" (debug_value f) (debug_value x) + | ValueVarApplication (name, x) -> + Printf.sprintf "App %s %s" name (debug_value x) + | ValueBinder (name, x, body) -> + Printf.sprintf "Bind %s %s %s" name (debug_value x) (debug_value body) + +module FromString = Map.Make (String) + +type _type = + | TypeInt + | TypeBool + | TypeVariable of string + | TypeArrow of _type * _type + +let rec debug_type (t : _type) : string = + match t with + | TypeInt -> "Integer" + | TypeBool -> "Boolean" + | TypeVariable k -> Printf.sprintf "%s" k + | TypeArrow (a, b) -> Printf.sprintf "%s -> %s" (debug_type a) (debug_type b) + +type quantified_type = QuantifiedType of string list * _type + +let debug_quantified_type (q : quantified_type) : string = + let QuantifiedType (vars, t) = q in + if List.length vars == 0 then + Printf.sprintf "%s" (debug_type t) + else + Printf.sprintf "forall %s. %s" (String.concat "," vars) (debug_type t) + +type set = bool FromString.t +type substitution = _type FromString.t + +let debug_substitution (s : substitution) : string = + FromString.fold (fun k v acc -> Printf.sprintf "%s\"%s\" |-> %s;" acc k (debug_type v)) s "" + |> Printf.sprintf "{ %s }" + +type env = quantified_type FromString.t + +let debug_env (s : env) : string = + FromString.fold (fun k v acc -> Printf.sprintf "%s\"%s\" |-> %s;" acc k (debug_quantified_type v)) s "" + |> Printf.sprintf "{ %s }" + +type inference = Inference of substitution * _type + +let debug_inference (Inference (s, t)) = + Printf.sprintf "type: %s; sub: %s" (debug_type t) (debug_substitution s) + +let rec pretty (t : _type) : string = + match t with + | TypeInt -> "Integer" + | TypeBool -> "Boolean" + | TypeVariable k -> Printf.sprintf "%s" k + | TypeArrow (a, b) -> Printf.sprintf "%s -> %s" (pretty a) (pretty b) |