Links types refactor -- draft

links_types_refactor.ml

(* Links types refactoring.
   Initial draft. 2020-04-16.
 *)
module StringMap = Map.Make(struct type t = string let compare = String.compare end) 
type 'a point = unit

module Kind = struct
  type primary = Type | Presence | Row
  type secondary = Session | Effect
  type t = primary * secondary
end

module Primitive = struct
  type t =
    | Bool
    | Float
    | Int
    | String
end

module TypeIdent = struct
  type t = int
end
module Quantifier = struct
  type t = { name: string;
             ident: TypeIdent.t;
             kind: Kind.t }
end

type typ =
  (* Special types. *)
  | Not_typed
  (* Regular types. *)
  | Primitive of Primitive.t
  | Meta of typ point
  | Var of { ident: TypeIdent.t; kind: Kind.t; freedom: Freedom.t }
  | ForAll of { quantifiers: Quantifier.t list; body: typ }
  | Function of { domain: typ list; row: typ; codomain: typ }
  | Lolli of { domain: typ list; row: typ; codomain: typ }
  | TypeConstructor of TypeIdent.t
  | Apply of { constr: typ; arguments: typ list }
  | Record of typ
  | Variant of typ
  | Effect of typ
  | Table of { read: typ; write: typ; needed: typ }
  | Recursive of { binder: Quantifier.t; body: typ }
  (* Row-y types. *)
  | Row of { fields: typ StringMap.t; dual: bool; var: typ }
  | Absent
  | Present of typ
  (* Session-y types. *)
  | Input of { supply: typ; continuation: typ }
  | Output of { demand: typ; continuation: typ }
  | Select of typ
  | Choice of typ
  | Dual of typ
  | End

| Mu of { binder: Quantifier.t; body: typ }

| TVar of TypeIdent.t

Skolem => MetaVar