Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

User-definable abstract types #1198

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions core/desugarDatatypes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions core/generalise.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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) ->
Expand Down
1 change: 1 addition & 0 deletions core/instantiate.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
5 changes: 5 additions & 0 deletions core/irCheck.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
dhil marked this conversation as resolved.
Show resolved Hide resolved
| _ -> false
end
(* Effect *)
| Effect l ->
begin match t2 with
Expand Down
1 change: 1 addition & 0 deletions core/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -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)) }
Expand Down
3 changes: 3 additions & 0 deletions core/sugarTraversals.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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) ->
Expand Down Expand Up @@ -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) ->
Expand Down Expand Up @@ -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) ->
Expand Down
1 change: 1 addition & 0 deletions core/sugartypes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions core/typeSugar.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions core/typeUtils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ ->
Expand Down Expand Up @@ -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
Expand Down
19 changes: 17 additions & 2 deletions core/types.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
dhil marked this conversation as resolved.
Show resolved Hide resolved

type tygroup = {
id: int;
type_map: ((Quantifier.t list * typ) Utility.StringMap.t);
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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) ->
Expand Down Expand Up @@ -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 _ -> ()
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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, _) ->
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions core/types.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
dhil marked this conversation as resolved.
Show resolved Hide resolved

(* Recursive type applications *)
val recursive_applications : datatype -> string list
Expand Down
3 changes: 3 additions & 0 deletions core/typevarcheck.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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, _) ->
Expand Down Expand Up @@ -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, _) ->
Expand Down Expand Up @@ -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, _) ->
Expand Down
25 changes: 23 additions & 2 deletions core/unify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems to assume only one layer of aliasing. I guess it is meant to dealwith the problem that if there are type parameters then the gensym.t generated once and for all for the abstract parameterized type will not know which parameters are applicable to any particular instance. However what about something like this:

typename MyParameterisedAbstractType(a,b,c);

typename MyAlias(a,b,c) = MyParameterisedAbstractType(a,b,c);

Now if I say pass something of type MyAlias(a,b,c) into something expecting MyParameterisedAbstractType(a,b,c) I think I will get a unification error, because we only look at the outer layer of aliasing.

I think it would be cleaner to make Abstract take Gensym.t and then a list of type arguments, and if the Gensyms are equal, unify recursively.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK, I will have a look at this.

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
Expand Down Expand Up @@ -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'
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See comment on line 93, this part would hopefully go away if we associate type parameter arguments with Abstract directly rather than piggypacking on Alias.

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^
Expand Down
17 changes: 17 additions & 0 deletions core/utility.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
38 changes: 38 additions & 0 deletions tests/abstract_types.tests
Original file line number Diff line number Diff line change
@@ -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 : () : ()
Loading