hmx_tc: HM(X) + multi parameter typeclasses

This extends `hmx` with multi parameter typeclasses. Follows THIH in
general and adds an elaborator.

Author: andreypopp

README.md

@@ -22,6 +22,10 @@
 
   The elaboration mechanism is shamelessly stolen from [inferno][].
 
+- `hmx_tc` - [HM(X)][] extends with Multi-Parameter Typeclasses (MPTC).
+  Type inference and elaborator are implemented but the environment construction
+  doesn't check for overlapping instances yet.
+
 # Development
 
 ```

hmx_tc/bin/dune

@@ -0,0 +1,4 @@
+(executable
+ (public_name hmx_tc)
+ (name main)
+ (libraries hmx_tc base stdio))

hmx_tc/bin/main.ml

@@ -0,0 +1,53 @@
+open Base
+open Hmx_tc
+
+let () =
+  let env =
+    Env.empty
+    |> Env.assume_val "one" "int"
+    |> Env.assume_val "hello" "string"
+    |> Env.assume_val "world" "string"
+    |> Env.assume_val "pair" "a, b . (a, b) -> pair[a, b]"
+    |> Env.assume_val "triple" "a, b, c . (a, b, c) -> triple[a, b, c]"
+    |> Env.assume_val "quadruple"
+         "a, b, c, e . (a, b, c, e) -> quadruple[a, b, c, e]"
+    |> Env.assume_val "plus" "(int, int) -> int"
+    |> Env.assume_val "true" "bool"
+    |> Env.assume_val "nil" "a . list[a]"
+    |> Env.assume_val "cons" "a . (a, list[a]) -> list[a]"
+    (* eq *)
+    |> Env.assume_tclass "eq" "a . (a, a) -> bool"
+    |> Env.assume_tclass_instance "eq_int" "eq[int]"
+    |> Env.assume_tclass_instance "eq_bool" "eq[bool]"
+    |> Env.assume_tclass_instance "eq_list" "a . eq[a] => eq[list[a]]"
+    |> Env.assume_tclass_instance "eq_pair"
+         "a, b . eq[a], eq[b] => eq[pair[a, b]]"
+    (* compare[a] *)
+    |> Env.assume_tclass "compare" "a . eq[a] => (a, a) -> bool"
+    |> Env.assume_tclass_instance "compare_list"
+         "a . compare[a] => compare[list[a]]"
+    |> Env.assume_tclass_instance "compare_int" "compare[int]"
+    |> Env.assume_tclass_instance "compare_bool" "compare[bool]"
+    (* coerce[a, b] *)
+    |> Env.assume_tclass "coerce" "a, b . a -> b"
+    |> Env.assume_tclass_instance "coerce_id" "a . coerce[a, a]"
+    |> Env.assume_tclass_instance "coerce_list"
+         "a, b . coerce[a, b] => coerce[list[a], list[b]]"
+    |> Env.assume_tclass_instance "coerce_bool_int" "coerce[bool, int]"
+    (* show *)
+    |> Env.assume_tclass "show" "a . a -> string"
+    |> Env.assume_tclass_instance "show_int" "show[int]"
+    |> Env.assume_tclass_instance "show_float" "show[float]"
+    (* (1* read *1) *)
+    |> Env.assume_tclass "read" "a . string -> a"
+    |> Env.assume_tclass_instance "read_int" "read[int]"
+    |> Env.assume_tclass_instance "read_float" "read[float]"
+    (* |> Env.assume_tclass "eq2" "a . (a, a) -> bool" *)
+    (* |> Env.assume_tclass_instance "eq2_int" "eq2[int]" *)
+    (* |> Env.assume_tclass_instance "eq2_list" "a . eq2[a] => eq2[list[a]]" *)
+    (* |> Env.assume_val "ch" "a . compare[a], eq2[a] => (a, a) -> bool" *)
+  in
+  let e = Expr.parse_chan Stdio.stdin in
+  match infer ~env e with
+  | Ok e -> Caml.Format.printf "%s@." (Expr.show e)
+  | Error err -> Caml.Format.printf "ERROR: %s@." (Type_error.show err)

hmx_tc/constraint.ml

@@ -0,0 +1,126 @@
+(**
+
+   This module defines constraint language.
+
+   The constraint language has applicative structure (see [C_map] constructor)
+   which is used for elaboration (the constraint solving algo computes a value).
+
+ *)
+
+open Base
+open Syntax
+
+type _ t =
+  | C_trivial : unit t
+      (** A trivial constraint, states nothing useful. Always can be solved. *)
+  | C_eq : ty * ty -> unit t
+      (** [C_eq (ty1, ty2)] states that the types [ty1] and [ty2] are equal. *)
+  | C_inst : name * ty -> expr t
+      (** [C_inst (name, ty)] states that [name] should be fetched from the
+          environment, instantiated and equated to [ty]. *)
+  | C_and : 'a t * 'b t -> ('a * 'b) t
+      (** Conjuction of two constraints, possibly of different value type. *)
+  | C_and_list : 'a t list -> 'a list t
+      (** Conjuction of multiple constraints of the same value type. *)
+  | C_exists : var list * 'a t -> 'a t
+      (** [C_exists (vs, c)] existentially quantifies variables [vs] over [c]. *)
+  | C_let :
+      (name * var list * expr t * ty) list * 'b t
+      -> ((expr * ty_sch) list * 'b) t
+      (** [C_let (bindings, c)] works is a constraint abstraction fused with
+          existential quantification. It adds [bindings] to the environment of
+          the following constraint [c].
+
+          It allows to define multiple names at once to support n-ary functions. *)
+  | C_map : 'a t * ('a -> 'b) -> 'b t
+      (** Map operation, this gives an applicative structure. *)
+
+let trivial = C_trivial
+
+let return v = C_map (C_trivial, fun () -> v)
+
+let ( =~ ) x y = C_eq (x, y)
+
+let inst name cty = C_inst (name, cty)
+
+let exists tys c =
+  match tys with
+  | [] -> c
+  | tys -> (
+    match c with
+    | C_exists (tys', c) -> C_exists (tys @ tys', c)
+    | c -> C_exists (tys, c))
+
+let let_in bindings c = C_let (bindings, c)
+
+let ( &~ ) x y = C_and (x, y)
+
+let ( >>| ) c f = C_map (c, f)
+
+let list cs = C_and_list cs
+
+let rec layout' : type a. names:Names.t -> a t -> PPrint.document =
+ fun ~names c ->
+  let open PPrint in
+  match c with
+  | C_trivial -> string "TRUE"
+  | C_eq (ty1, ty2) ->
+    layout_ty' ~names ty1 ^^ string " = " ^^ layout_ty' ~names ty2
+  | C_and (a, b) -> layout' ~names a ^^ string " & " ^^ layout' ~names b
+  | C_and_list cs ->
+    let sep = string " & " in
+    separate sep (List.map cs ~f:(layout' ~names))
+  | C_exists (vs, c) ->
+    string "∃"
+    ^^ separate comma (List.map vs ~f:(layout_con_var' ~names))
+    ^^ dot
+    ^^ parens (layout' ~names c)
+  | C_let (bindings, c) ->
+    let layout_cty' : type a. a t * ty -> document = function
+      | C_trivial, ty -> layout_ty' ~names ty
+      | c, ty -> layout' ~names c ^^ string " => " ^^ layout_ty' ~names ty
+    in
+    let layout_binding : type a. string * var list * a t * ty -> document =
+     fun (name, vs, c, ty) ->
+      string name
+      ^^ string " : "
+      ^^
+      match vs with
+      | [] -> layout_cty' (c, ty)
+      | vs ->
+        let vs = layout_var_prenex' ~names vs in
+        vs ^^ layout_cty' (c, ty)
+    in
+    let sep = comma ^^ blank 1 in
+    string "let "
+    ^^ separate sep (List.map bindings ~f:layout_binding)
+    ^^ string " in "
+    ^^ layout' ~names c
+  | C_inst (name, ty) -> string name ^^ string " ≲ " ^^ layout_ty' ~names ty
+  | C_map (c, _f) -> layout' ~names c
+
+include (
+  struct
+    type pack = P : _ t -> pack
+
+    include Showable (struct
+      type t = pack
+
+      let layout (P c) =
+        let names = Names.make () in
+        layout' ~names c
+    end)
+
+    let layout c = layout (P c)
+
+    let show c = show (P c)
+
+    let print ?label c = print ?label (P c)
+  end :
+    sig
+      val layout : _ t -> PPrint.document
+
+      val show : _ t -> string
+
+      val print : ?label:string -> _ t -> unit
+    end)

hmx_tc/debug.ml

@@ -0,0 +1,17 @@
+open! Base
+
+let flags = Caml.Sys.getenv_opt "HMX_DEBUG" |> Option.value ~default:""
+
+let log_levels = String.mem flags 'l'
+
+let log_solve = String.mem flags 's'
+
+let log_instantiate = String.mem flags 'i'
+
+let log_generalize = String.mem flags 'g'
+
+let log_unify = String.mem flags 'u'
+
+let log_match = String.mem flags 'm'
+
+let log_define = String.mem flags 'd'

hmx_tc/dune

@@ -0,0 +1,11 @@
+(library
+ (name hmx_tc)
+ (preprocess (pps ppx_sexp_conv))
+ (libraries base pprint nice_parser)
+ )
+
+(ocamllex lexer)
+
+(menhir
+  (modules parser)
+  (flags --explain --dump))

hmx_tc/hmx_tc.ml

@@ -0,0 +1,59 @@
+module Expr = struct
+  include Syntax.Expr
+
+  include Nice_parser.Make (struct
+    type token = Parser.token
+
+    type result = Syntax.expr
+
+    let parse = Parser.expr_eof
+
+    let next_token = Lexer.token
+
+    exception ParseError = Parser.Error
+
+    exception LexError = Lexer.Error
+  end)
+end
+
+module Ty = struct
+  include Syntax.Ty
+end
+
+module Ty_sch = struct
+  include Syntax.Ty_sch
+
+  include Nice_parser.Make (struct
+    type token = Parser.token
+
+    type result = Syntax.ty_sch
+
+    let parse = Parser.ty_sch_eof
+
+    let next_token = Lexer.token
+
+    exception ParseError = Parser.Error
+
+    exception LexError = Lexer.Error
+  end)
+end
+
+module Bound = struct
+  include Syntax.Bound
+end
+
+module Var = Var
+module Type_error = Type_error
+
+module Env = struct
+  include Infer.Env
+
+  let assume_val name ty env = add_val env name (Ty_sch.parse_string ty)
+
+  let assume_tclass name ty env = add_tclass env name (Ty_sch.parse_string ty)
+
+  let assume_tclass_instance name ty env =
+    add_tclass_instance env name (Ty_sch.parse_string ty)
+end
+
+let infer = Infer.infer