User-definable abstract types

core/desugarDatatypes.ml

@@ -79,6 +79,7 @@ module Desugar = struct
       let open Datatype in
       (* let z = *)
       match t with
+        | Datatype.Abstract abs -> Types.Abstract abs
         | TypeVar stv ->
            let point = SugarTypeVar.get_resolved_type_exn stv in
            Meta point

core/generalise.ml

@@ -30,6 +30,7 @@ let rec get_type_args : gen_kind -> TypeVarSet.t -> datatype -> type_arg list =
         | Not_typed -> raise (internal_error "Not_typed encountered in get_type_args")
         | (Var _ | Recursive _) ->
            failwith ("freestanding Var / Recursive not implemented yet (must be inside Meta)")
+        | Abstract _abs -> []
         | Alias (_, (_, _, ts, _), t) ->
            concat_map (get_type_arg_type_args kind bound_vars) ts @ gt t
         | Application (_, args) ->

core/instantiate.ml

@@ -43,6 +43,7 @@ let instantiates : instantiation_maps -> (datatype -> datatype) * (row -> row) *
     match datatype with
         | Not_typed -> raise (internal_error "Not_typed' passed to `instantiate'")
         | Primitive _  -> datatype
+        | Abstract _abs -> datatype
         | Meta point ->
             let t = Unionfind.find point in
               begin

core/irCheck.ml

@@ -344,6 +344,11 @@ let eq_types occurrence : type_eq_context -> (Types.datatype * Types.datatype) -
             else false
          | _ -> false
          end
+      | Abstract abs ->
+         begin match t2 with
+         | Abstract abs' -> abs == abs' (* pointer equality *)
+         | _ -> false
+         end
       (* Effect *)
       | Effect l ->
          begin match t2 with

core/parser.mly

@@ -539,6 +539,7 @@ signature:
 | SIG sigop COLON datatype                                     { with_pos $loc ($2, datatype $4) }
 
 typedecl:
+| TYPENAME CONSTRUCTOR typeargs_opt                             { alias $loc $2 $3 (Typename   ( WithPos.make (Datatype.Abstract (Gensym.gensym ())), None)) }
 | TYPENAME CONSTRUCTOR typeargs_opt EQ datatype                 { alias $loc $2 $3 (Typename   ( $5     , None)) }
 | EFFECTNAME CONSTRUCTOR typeargs_opt EQ LBRACE erow RBRACE     { alias $loc $2 $3 (Effectname ( $6     , None)) }
 | EFFECTNAME CONSTRUCTOR typeargs_opt EQ effect_app             { alias $loc $2 $3 (Effectname (([], $5), None)) }

core/sugarTraversals.ml

@@ -659,6 +659,7 @@ class map =
     method datatypenode : Datatype.t -> Datatype.t =
       let open Datatype in
       function
+      | Abstract abs -> Abstract abs
       | TypeVar _x ->
           let _x = o#type_variable _x in TypeVar _x
       | QualifiedTypeApplication (ns, args) ->
@@ -1450,6 +1451,7 @@ class fold =
     method datatypenode : Datatype.t -> 'self_type =
       let open Datatype in
       function
+      | Abstract _abs -> o
       | TypeVar _x ->
           let o = o#type_variable _x in o
       | QualifiedTypeApplication (ns, args) ->
@@ -2372,6 +2374,7 @@ class fold_map =
     method datatypenode : Datatype.t -> ('self_type * Datatype.t) =
       let open Datatype in
       function
+      | Abstract abs -> (o, Abstract abs)
       | TypeVar _x ->
           let (o, _x) = o#type_variable _x in (o, (TypeVar _x))
       | QualifiedTypeApplication (ns, args) ->

core/sugartypes.ml

@@ -192,6 +192,7 @@ type fieldconstraint = Readonly | Default
 
 module Datatype = struct
   type t =
+    | Abstract        of Gensym.t
     | TypeVar         of SugarTypeVar.t
     | QualifiedTypeApplication of Name.t list * type_arg list
     | Function        of with_pos list * row * with_pos

core/typeSugar.ml

@@ -2224,6 +2224,7 @@ let close_pattern_type : Pattern.with_pos list -> Types.datatype -> Types.dataty
           let pats = concat_map unwrap pats in
             Application (Types.list, [cpta pats t])
       | ForAll (qs, t) -> ForAll (qs, cpt pats t)
+      | Abstract abs -> Abstract abs
       | Meta point ->
           begin
             match Unionfind.find point with

core/typeUtils.ml

@@ -232,6 +232,7 @@ let rec primary_kind_of_type t =
   match concrete_type t with
   | Not_typed ->
      failwith "Not_typed has no kind"
+  | Abstract _ -> PrimaryKind.Type
   | Var (_, kind, _) ->
      Kind.primary_kind kind
   | Recursive _ ->
@@ -325,6 +326,7 @@ let check_type_wellformedness primary_kind t : unit =
     | (Var _ | Recursive _ | Closed) ->
        (* freestanding Var / Recursive / Closed not implemented yet (must be inside Meta) *)
        raise tag_expectation_mismatch
+    | Abstract _abs -> pk_type
     | Alias (_, (_name, qs, ts, _), d) ->
        List.iter2 (compare_kinds rec_env) qs ts;
        typ rec_env d

core/types.ml

@@ -136,6 +136,8 @@ module RecIdMap = Map.Make(RecId)
 module type RECIDSET = Utility.Set with type elt = rec_id
 module RecIdSet : RECIDSET = Set.Make(RecId)
 
+let pp_exn fmt _ = Format.fprintf fmt "exn"
+
 type tygroup = {
   id: int;
   type_map: ((Quantifier.t list * typ) Utility.StringMap.t);
@@ -171,6 +173,7 @@ and typ =
   | Table of (Temporality.t * typ * typ * typ)
   | Lens of Lens.Type.t
   | ForAll of (Quantifier.t list * typ)
+  | Abstract of Gensym.t
   (* Effect *)
   | Effect of row
   | Operation of (typ * typ * DeclaredLinearity.t)
@@ -400,6 +403,7 @@ struct
          let (o, names') = o#list (fun o -> o#quantifier) names in
          let (o, body') = o#typ body in
          (o, ForAll (names', body'))
+      | Abstract abs -> (o, Abstract abs)
       (* Effect *)
       | Effect row ->
          let (o, row') = o#row row in
@@ -613,6 +617,7 @@ class virtual type_predicate = object(self)
     | Table _ -> true
     | Lens _ -> true
     | ForAll (qs, t) -> self#type_satisfies (rec_appl, rec_vars, TypeVarSet.add_quantifiers qs quant_vars) t
+    | Abstract _abs -> true (* This does assume that all abstract types satisfy the predicate. *)
     | Row (fields, row_var, _) ->
        let row_var = self#point_satisfies self#row_satisfies vars row_var in
        let fields = FieldEnv.for_all (fun _ f -> self#field_satisfies vars f) fields in
@@ -681,6 +686,7 @@ class virtual type_iter = object(self)
     | Lens _ -> ()
     | ForAll (qs, t) ->
        self#visit_type (rec_appl, rec_vars, TypeVarSet.add_quantifiers qs quant_vars) t
+    | Abstract _abs -> ()
     (* Effect *)
     | Effect r -> self#visit_row vars r
     | Operation (a, b, _) -> self#visit_type vars a; self#visit_type vars b
@@ -779,7 +785,7 @@ module Base : Constraint = struct
         (* Type *)
         | Primitive (Bool | Int | Char | Float | String | DateTime) -> true
         | Primitive _ -> false
-        | (Function _ | Lolli _ | Record _ | Variant _ | Table _ | Lens _ | ForAll (_::_, _)) -> false
+        | (Function _ | Lolli _ | Record _ | Variant _ | Table _ | Lens _ | ForAll (_::_, _)) | Abstract _ -> false
         | ForAll ([], t) -> super#type_satisfies vars t
         (* Effect *)
         | Effect _ as t -> super#type_satisfies vars t
@@ -829,6 +835,7 @@ module Unl : Constraint = struct
       | (Record _ | Variant _) as t -> super#type_satisfies vars t
       | (Table _ | Lens _) -> true
       | ForAll _ as t -> super#type_satisfies vars t
+      | Abstract _ as t -> super#type_satisfies vars t
       (* Effect *)
       | Effect _  -> true
       | Operation (_,_,b) ->
@@ -882,6 +889,7 @@ module Unl : Constraint = struct
        | (Record _ | Variant _) as t -> super#visit_type vars t
        | Table _ | Lens _ -> ()
        | ForAll _ as t -> super#visit_type vars t
+       | Abstract _abs -> ()
        (* Effect *)
        | Effect _ -> ()
        | Operation _ -> ()
@@ -929,7 +937,7 @@ module Session : Constraint = struct
         (* Unspecified kind *)
         | Application _ -> false (* FIXME: we assume that abstract types cannot have session kind *)
         (* Type but not Session *)
-        | Primitive _ | Function _ | Lolli _ | Record _ | Variant _ | Table _ | Lens _ | ForAll _ -> false
+        | Primitive _ | Function _ | Lolli _ | Record _ | Variant _ | Table _ | Lens _ | ForAll _ | Abstract _ -> false
         (* Effect *)
         | Effect _  -> false
         | Operation _ -> failwith "TODO types.ml/910"
@@ -1209,6 +1217,7 @@ let free_type_vars, free_row_type_vars, free_tyarg_vars =
        S.union_all (List.map (free_tyarg_vars' rec_vars) r_args)
     | ForAll (tvars, body)    -> S.diff (free_type_vars' rec_vars body)
                                    (TypeVarSet.add_quantifiers tvars S.empty)
+    | Abstract _abs -> S.empty
     | Meta point       ->
        begin
          match Unionfind.find point with
@@ -1407,6 +1416,7 @@ and subst_dual_type : var_map -> datatype -> datatype =
      RecursiveApplication { app with r_args =
                                        List.map (subst_dual_type_arg rec_points) app.r_args }
   | ForAll (qs, body) -> ForAll (qs, sdt body)
+  | Abstract abs -> Abstract abs
   | Meta point ->
      begin
        match Unionfind.find point with
@@ -1619,6 +1629,7 @@ and normalise_datatype rec_names t =
        | ForAll (qs', body) -> ForAll (qs @ qs', body)
        | body -> ForAll (qs, body)
      end
+  | Abstract abs -> Abstract abs
   | Meta point       ->
      begin
        match Unionfind.find point with
@@ -1908,6 +1919,7 @@ struct
            (bound_vars, [])
            tyvars in
        (List.rev vars) @ (free_bound_type_vars bound_vars body)
+    | Abstract _abs -> []
     (* Effect *)
     | Effect row -> free_bound_row_type_vars bound_vars row
     | Operation (f, t, _) ->
@@ -2674,6 +2686,7 @@ struct
                  "forall "^ mapstrcat "," (quantifier p) tyvars ^"."^ datatype { context with bound_vars } p body
             else
               "forall "^ mapstrcat "," (quantifier p) tyvars ^"."^ datatype { context with bound_vars } p body
+         | Abstract _abs -> "<abstract>"
          (* Effect *)
          | Effect r -> "{" ^ row "," context p r ^ "}"
          | Operation (f, t, b) -> sd f ^ (if b=DeclaredLinearity.Lin then " =@ " else " => ") ^ sd t
@@ -4131,6 +4144,7 @@ module RoundtripPrinter : PRETTY_PRINTER = struct
             | Table tab          -> with_value table tab
             | Lens tp            -> with_value lens tp
             | ForAll fa          -> with_value forall fa
+            | Abstract _abs      -> constant "<abstract>"
 
             | Input _ | Output _ -> with_value session_io tp
             | Dual tp            -> with_value session_dual tp
@@ -4473,6 +4487,7 @@ let make_fresh_envs : datatype -> datatype IntMap.t * row IntMap.t * field_spec
     | RecursiveApplication { r_args ; _ } -> union (List.map (make_env_ta boundvars) r_args)
     | ForAll (qs, t)          ->
        make_env (TypeVarSet.add_quantifiers qs boundvars) t
+    | Abstract _abs -> empties
     | Meta point ->
        begin
          match Unionfind.find point with

core/types.mli

@@ -143,6 +143,7 @@ and typ =
   | Table of (Temporality.t * typ * typ * typ)
   | Lens of Lens.Type.t
   | ForAll of (Quantifier.t list * typ)
+  | Abstract of Utility.Gensym.t
   (* Effect *)
   | Effect of row
   | Operation of (typ * typ * DeclaredLinearity.t)
@@ -453,6 +454,7 @@ val pp_row' : Format.formatter -> row' -> unit
 val pp_type_arg : Format.formatter -> type_arg -> unit
 val pp_tycon_spec: Format.formatter -> tycon_spec -> unit
 val pp_field_spec: Format.formatter -> field_spec -> unit
+val pp_exn : Format.formatter -> exn -> unit
 
 (* Recursive type applications *)
 val recursive_applications : datatype -> string list

core/typevarcheck.ml

@@ -85,6 +85,7 @@ let rec is_guarded : TypeVarSet.t -> StringSet.t -> int -> datatype -> bool =
             is_guarded
               (TypeVarSet.add_quantifiers qs bound_vars)
               expanded_apps var t
+        | Abstract _abs -> true (* TODO(dhil): could be unguarded... *)
         (* Effect *)
         | Effect row -> isgr row
         | Operation (f, t, _) ->
@@ -174,6 +175,7 @@ let rec is_negative : TypeVarSet.t -> StringSet.t -> int -> datatype -> bool =
             is_negative
               (TypeVarSet.add_quantifiers qs bound_vars)
               expanded_apps var t
+        | Abstract _abs -> false
         (* Effect *)
         | Effect row -> isnr row
         | Operation (f, t, _) ->
@@ -263,6 +265,7 @@ and is_positive : TypeVarSet.t -> StringSet.t -> int -> datatype -> bool =
             is_positive
               (TypeVarSet.add_quantifiers qs bound_vars)
               expanded_apps var t
+        | Abstract _abs -> false
         (* Effect *)
         | Effect row -> ispr row
         | Operation (f, t, _) ->

core/unify.ml

@@ -83,8 +83,18 @@ let rec eq_types : (datatype * datatype) -> bool =
   fun (t1, t2) ->
     let rec unalias = function
       | Alias (_, _, x) -> unalias x
-      | x            -> x in
+      | x            -> x
+    in
     match unalias t1 with
+      | Abstract abs ->
+         begin match unalias t2 with
+         | Abstract abs' ->
+            Gensym.equal abs abs'
+            && (let [@ocaml.warning "-8"]Alias (_, (_, _, tyargs, _), _) = t1 in
+                let [@ocaml.warning "-8"]Alias (_, (_, _, tyargs', _), _) = t2 in
+                List.for_all2 (fun (_tyk, ty) (_tyk', ty') -> eq_types (ty, ty')) tyargs tyargs')
+         | _ -> false
+         end
       | Not_typed ->
           begin match unalias t2 with
           | Not_typed -> true
@@ -598,7 +608,18 @@ let rec unify' : unify_env -> (datatype * datatype) -> unit =
             Unionfind.change point t; *)
          | t' -> ut (t, t')
        end
-    | Alias (_, _, t1), t2 | t1, Alias (_, _, t2) -> ut (t1, t2)
+    | Abstract _, _ | _, Abstract _ ->
+       failwith "freestanding Abstract (must be under an alias)"
+    | Alias (_, _, Abstract abs), Alias (_, _, Abstract abs') ->
+       if Gensym.equal abs abs'
+       then let [@ocaml.warning "-8"]Alias (_, (_, _, tyargs, _), _) = t1 in
+            let [@ocaml.warning "-8"]Alias (_, (_, _, tyargs', _), _) = t2 in
+            List.iter2 (fun tyargs tyargs' -> unify_type_args' rec_env (tyargs, tyargs')) tyargs tyargs'
+       else raise (Failure (`Msg "cannot unify different abstract types"))
+    | ((Alias (_, _, Abstract _) as t1), t2) | (t2, (Alias (_, _, Abstract _) as t1)) ->
+       raise (Failure (`Msg ("Cannot unify abstract type '" ^ string_of_datatype t1 ^ "' with concrete type '" ^ string_of_datatype t2 ^ "'")))
+    | Alias (_, _, t1), t2 | t1, Alias (_, _, t2) ->
+       ut (t1, t2)
     | Application (l, _), Application (r, _) when l <> r ->
        raise (Failure
                 (`Msg ("Cannot unify abstract type '"^string_of_datatype t1^

core/utility.ml

@@ -1087,6 +1087,23 @@ let pair_fresh_names ?prefix:pfx list =
 let refresh_names =
   graph_func (fun x -> gensym ~prefix:x ())
 
+(** Generates an opaque unique identity.  TODO(dhil): reconcile the
+   above (legacy) gensym with this. *)
+module Gensym: sig
+  type t
+  val gensym : unit -> t (* generates a unique identity *)
+  val to_string : t -> string (* string representation; used in codegen *)
+  val equal : t -> t -> bool (* decides whether two identities are the same *)
+  val pp : Format.formatter -> 'a -> unit
+end = struct
+  type t = exn
+  let gensym () =
+    let exception E in E
+  let to_string exn = Printf.sprintf "%d" (Hashtbl.hash exn)
+  let equal exn exn' = exn == exn'
+  let pp fmt exn = Format.fprintf fmt "%s" (to_string exn)
+end
+
 (** Return [true] if any element of the given list is [true] *)
 let any_true = List.exists identity
 

tests/abstract_types.tests

@@ -0,0 +1,38 @@
+Abstract type declaration
+typename Foo;
+stdout : () : ()
+
+Abstract type unification
+typename Foo; sig foo : (Foo) -> Foo fun foo(x) { x }
+stdout : () : ()
+
+Abstract type identities (1)
+typename Foo; typename Bar; sig foobar : (Foo) -> Bar fun foobar(x) { x }
+stderr : @.
+exit : 1
+
+Abstract type identities (2)
+typename Foo; sig foo : () -> Foo fun foo() { error("I cannot materialise a foo") }; typename Foo; sig foo' : (Foo) -> () fun foo'(_) { () }; foo'(foo())
+stderr : @.
+exit : 1
+
+Parameterised abstract types (1)
+typename Foo(a,b,c); sig foo : (Foo(a,b,c)) -> Foo(String,Int,Float) fun foo(x) { x }
+stderr : @.
+exit : 1
+
+Parameterised abstract types (2)
+typename Foo(a,b); sig foo : (Foo(Int,String)) -> Foo(Int,String) fun foo(x) { x }
+stdout : () : ()
+
+Parameterised abstract types (3)
+typename Foo(a,b); sig foo : (a, b) ~> Foo(a,b) fun foo(_,_) { error("cannot materialise Foo") }
+stdout : () : ()
+
+Parameterised abstract types (4)
+typename Foo(a,b); sig foo : (Foo(a,b)) ~> Foo(b,a) fun foo(_) { error("cannot materialise Foo") }
+stdout : () : ()
+
+Alien
+typename A; alien javascript "" f : () -> A;
+stdout : () : ()