Skip to content

Commit

Permalink
First pass at reducing intersection types.
Browse files Browse the repository at this point in the history
  • Loading branch information
skaller committed Jul 11, 2022
1 parent 1d9ebae commit 67afdc9
Show file tree
Hide file tree
Showing 6 changed files with 99 additions and 4 deletions.
Binary file modified pdfs/technote-compact-linear-types.pdf
Binary file not shown.
2 changes: 1 addition & 1 deletion src/compiler/flx_bind/flx_bind_bexe.ml
Original file line number Diff line number Diff line change
Expand Up @@ -814,7 +814,7 @@ print_endline ("Beta reduced LHS is not actually reduced: " ^ sbt bsym_table lhs
sbe bsym_table (e',rhst) ^
"\nof type\n" ^
sbt bsym_table rhst ^
"\nis not a supertype of the declared variable type:\n" ^
"\nis not a subtype of the declared variable type:\n" ^
sbt bsym_table lhst
)
end
Expand Down
4 changes: 2 additions & 2 deletions src/compiler/flx_core/flx_beta.ml
Original file line number Diff line number Diff line change
Expand Up @@ -391,11 +391,11 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);


| BTYP_tuple ls -> btyp_tuple (List.map br ls)
| BTYP_intersect ls -> btyp_intersect (List.map br ls)
| BTYP_array (i,t) -> btyp_array (br i, br t)
| BTYP_rptsum (i,t) -> btyp_rptsum (br i, br t)
| BTYP_sum ls -> btyp_sum (List.map br ls)

| BTYP_intersect ls -> Flx_intersect.intersect bsym_table counter br ls
| BTYP_record (ts) ->
let ss,ls = List.split ts in
btyp_record (List.combine ss (List.map br ls))
Expand Down Expand Up @@ -616,4 +616,4 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);
| None -> btyp_subtype_match (tt,pts)
end
end

42 changes: 41 additions & 1 deletion src/compiler/flx_core/flx_bsym_table.ml
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,47 @@ let is_indirect_supertype bsym_table param arg : bool =
ignore(find_coercion_chains bsym_table param arg));
*)
result


let supertypes_of bsym_table a : BidSet.t =
List.fold_left (fun acc ((p',a'),j) -> if a = a' then BidSet.add p' acc else acc) (BidSet.singleton a) bsym_table.subtype_map


(* NOTE: this may not be unique! We should really return all of them.
Example: X > A, X > B, Y > A, Y > B then both X and Y are supertypes
of both A and B. In addition if W > X and W > Y, then still both
are less than W so W is a common supertype of A and B but not least.
This could happen in C++ with multiple inheritance.
W
/ \
X Y
\\ //
A B
NOTE: due to this issue, we cannot calculate the least supertype of a set pairwise, unless we retain
duplicates. This is because some type C might be a subtype of Y but not X, which would eliminate X
as a supertype of all three of A B C. Instead we have to find the intersection of ALL the supertypes
of each input type first before trying to find a least one. The pairwise routine couldn't work even
if BOTH X and Y were returned and then D came along which was a subtype of only W, unless we
regenerated all the supertypes of the set of pairwise results. So might as well just intersect
the whole set first.
*)
let least_supertype bsym_table ls : int option =
match ls with
| [] -> None
| [x] -> Some x
| h :: tail ->
let cands = List.fold_left
(fun acc elt -> BidSet.inter acc (supertypes_of bsym_table elt))
(supertypes_of bsym_table h)
tail
in
if BidSet.is_empty cands then None else
let chosen = BidSet.choose cands in
let cands = BidSet.remove chosen cands in
Some (BidSet.fold (fun cand current ->
if is_indirect_supertype bsym_table current cand then cand else current
) cands chosen)


let fold_coercions bsym_table f init =
Expand Down
2 changes: 2 additions & 0 deletions src/compiler/flx_core/flx_bsym_table.mli
Original file line number Diff line number Diff line change
Expand Up @@ -133,3 +133,5 @@ val validate : string -> t -> unit
val validate_types: (Flx_btype.t -> unit) -> t -> unit
val is_prim: t -> bid_t -> bool

val least_supertype: t -> int list -> int option

53 changes: 53 additions & 0 deletions src/compiler/flx_core/flx_intersect.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
open Flx_mtypes2
open Flx_bid
open Flx_print
open Flx_kind
open Flx_btype

let field_merge counter br fs =
let type_eq t1 t2 = Flx_typeeq.type_eq Flx_btype.st counter t1 t2 in
let meet t1 t2 =
if type_eq t1 t2 then t1 (* same type, hooray! *)
else br (btyp_intersect [t1;t2]) (* calculate the least type of which both are subtypes *)
in
let rec aux inp out =
match inp with
| [] -> List.rev out
| [x] -> List.rev (x::out)
| (s1,t1) :: (s2,t2) :: tail ->
if s1 = s2 then
aux ((s1, meet t1 t2) :: tail) out
else
aux ((s2,t2) :: tail) ((s1,t1) :: out)
in aux fs []


let intersect bsym_table counter br ls =
let ls = List.map br ls in
begin match ls with
| [] -> assert false
| [x] -> x (* NOTE: this is WRONG! We have to merge the fields even of a single operand *)
| h1 :: h2 :: tail ->
begin match h1, h2 with
| BTYP_record fs1, BTYP_record fs2 ->
let fs = fs1 @ fs2 in
let cmp (s1,t1) (s2, t2) = compare s1 s2 in
let fs = List.stable_sort cmp fs in
let fs = field_merge counter br (List.map (fun (s,t) -> s, br t) fs) in
let r = btyp_record fs in
br (btyp_intersect (r :: tail))
(* primitive least supertype can be calculated here *)
| BTYP_inst (`Nominal, i, [], KIND_type), BTYP_inst (`Nominal, j, [], KIND_type) ->
begin match Flx_bsym_table.least_supertype bsym_table [i;j] with
| Some k -> btyp_inst (`Nominal, k, [], KIND_type)
| None ->
print_endline ("No least supertype of primitives " ^ Flx_btype.st h1 ^ " and " ^ Flx_btype.st h2);
failwith ("No least supertype of primitives " ^ Flx_btype.st h1 ^ " and " ^ Flx_btype.st h2)
end
| _ ->
print_endline ("No least supertype of " ^ Flx_btype.st h1 ^ " and " ^ Flx_btype.st h2);
failwith ("No least supertype of " ^ Flx_btype.st h1 ^ " and " ^ Flx_btype.st h2)
end
end


0 comments on commit 67afdc9

Please sign in to comment.