Recursively dependent signatures

Author: polytypic

elab.ml

@@ -270,6 +270,18 @@ Trace.debug (lazy ("[WithT] aks12 = " ^ string_of_norm_extyp (ExT(aks12, StrT []
     ExT(aks11, subst_typ (subst aks12 ts) t1),
     lift_warn typ.at t1 (add_typs aks11 env) (zs1 @ zs2 @ zs3)
 
+  | EL.RecT(var, typ1, typ2) ->
+    let ExT(aks1, t1), zs1 = elab_typ env typ1 l in
+    let env1 = add_val var.it t1 (add_typs aks1 env) in
+    let ExT(aks2, t2), zs2 = elab_typ env1 typ2 l in
+    let ts, zs3, e =
+      try sub_typ env1 t2 t1 (varTs aks1) with Sub e -> error typ.at
+        ("recursive type does not match annotation: " ^ Sub.string_of_error e)
+    in
+    let aks' = freshen_vars env aks1 in
+    let t3 = subst_typ (subst aks1 (varTs aks')) t2 in
+    ExT(aks', t3), lift_warn typ.at t3 env (zs1 @ zs2 @ zs3)
+
 and elab_dec env dec l =
   Trace.elab (lazy ("[elab_dec] " ^ EL.label_of_dec dec));
   (fun (s, zs) -> dec.at, env, s, zs, None, EL.label_of_dec dec) <<<

regression.1ml

@@ -1,3 +1,27 @@
+type RDS = rec (R: let type T'1 = {type t _} in {A: T'1; B: T'1}) => let
+  type ONE (type this _) (type that _) = {
+    t = this;
+    aThis 'a: this a;
+    ofThat 'a: that a -> this a;
+  };
+in {
+  A: ONE R.A.t R.B.t;
+  B: ONE R.B.t R.A.t;
+};
+
+Rds :> RDS = let
+  One = {
+    type t _ = ();
+    aThis = ();
+    ofThat _ = ();
+  };
+in {
+  A = One;
+  B = One;
+};
+
+;;
+
 Equivalence: {
   type t a b;
 
@@ -60,13 +84,29 @@ type_error rec (R: {}) => {
   kaboom () = R;
 };
 
-Kaboom = rec (R: rec R => {kaboom: () -> R}) => @(= R) {
-  kaboom () = R;
-};
+;;Kaboom = rec (R: rec R => {kaboom: () -> R}) => @(= R) {
+;;  kaboom () = R;
+;;};
 
 ;;
 
-Mutually = let
+type MUTUALLY = rec (R: {
+  Even: {type t _};
+  Odd: {type t _};
+}) => {
+  Even: {
+    t = R.Even.t;
+    make 'x: x => R.Odd.t x => R.Even.t x;
+    size 'x: R.Even.t x -> int;
+  };
+  Odd: {
+    t = R.Odd.t;
+    make 'x: opt (R.Even.t x) => R.Odd.t x;
+    size 'x: R.Odd.t x -> int;
+  };
+};
+
+Mutually :> MUTUALLY = let
   T = rec (R: {
     Even: {type t _};
     Odd: {type t _};
@@ -109,7 +149,7 @@ in {
 ;;
 
 Hungry = {
-  type eat a = rec eat_a => a -> eat_a;
+  ...rec {type eat a} => {type eat a = a -> eat a};
 
   eater 'a: eat a = rec (eater: eat a) => @(eat a) (fun a => eater);
 
@@ -119,7 +159,7 @@ Hungry = {
 };
 
 PolyRec = {
-  type l a = rec (type t) => alt a t;
+  ...rec {type l a} => {type l a = alt a (l a)};
   ...rec {type t a} => {type t a = alt a (t (type (a, a)))};
 
   t_int = t int;

sub.ml

@@ -91,6 +91,25 @@ let lift_warn at t env zs =
 
 (* Subtyping *)
 
+let rec has_typs_typ ps = function
+  | VarT(_) -> false
+  | PrimT(_) -> false
+  | StrT(tr) -> List.exists (fun (_, t) -> has_typs_typ ps t) tr
+  | FunT(aks, td, ExT(_, tr), e) ->
+    (match e with
+     | Implicit | Explicit Pure ->
+       has_typs_typ (List.map (fun p -> AppT(p, varTs aks)) ps) tr
+     | Explicit Impure -> false)
+  | TypT(ExT(_, p)) -> List.mem p ps
+  | WrapT(_) -> false
+  | LamT(_) -> false
+  | AppT(_) -> false
+  | TupT(_) -> false
+  | DotT(_) -> false
+  | RecT(_) -> false
+  | InferT(_) -> false
+
+
 let resolve_typ z t =
   Trace.sub (lazy ("[resolve_typ] z = " ^ string_of_norm_typ (InferT(z))));
   Trace.sub (lazy ("[resolve_typ] t = " ^ string_of_norm_typ t));
@@ -101,12 +120,36 @@ let unify_typ t1 t2 =
   Trace.sub (lazy ("[unify_typ] t2 = " ^ string_of_norm_typ t2));
   unify_typ t1 t2
 
+let rec psubst p t =
+  match p with
+  | VarT(a, k) -> a, t
+  | AppT(p', ts) -> psubst p' (LamT(List.map unvarT ts, t))
+  | _ -> assert false
+
 
 let rec sub_typ env t1 t2 ps =
   Trace.sub (lazy ("[sub_typ] t1 = " ^ string_of_norm_typ t1));
   Trace.sub (lazy ("[sub_typ] t2 = " ^ string_of_norm_typ t2));
   Trace.sub (lazy ("[sub_typ] ps = " ^
     String.concat ", " (List.map string_of_norm_typ ps)));
+  let ts', zs', t2, ps =
+    if ps <> [] then
+      let su, zs' = match_typ env t1 t2 ps in
+      Trace.sub (lazy ("[sub_typ] su = " ^
+        String.concat ", " (List.map (fun (p, t) -> Printf.sprintf "[= %s] - [= %s]\n" (string_of_typ p) (string_of_typ t)) su)));
+      let t2 = subst_typ (List.map (fun (p, t) -> psubst p t) su) t2 in
+      let ps' = List.filter (fun p -> List.mem_assoc p su) ps in
+      let ts' = List.map (fun p -> List.assoc p su) ps' in
+      let ps = List.filter (fun p -> not (List.mem_assoc p su)) ps in
+      if ps <> [] then begin
+        Trace.sub (lazy ("[sub_typ] unmatched ps = " ^
+          String.concat ", " (List.map string_of_norm_typ ps)));
+        raise Not_found
+      end;
+      ts', zs', t2, ps
+    else
+      [], [], t2, ps
+  in
   let e1 = IL.VarE("x") in
   let ts, zs, e =
     match norm_typ t1, freshen_typ env (norm_typ t2) with
@@ -267,7 +310,7 @@ let rec sub_typ env t1 t2 ps =
   Trace.sub (lazy ("[sub_typ] done ts = " ^
     String.concat ", " (List.map string_of_norm_typ ts)));
   Trace.sub (lazy ("[sub_typ] done x -> " ^ IL.string_of_exp e));
-  ts, zs, IL.LamE("x", erase_typ t1, e)
+  ts' @ ts, zs' @ zs, IL.LamE("x", erase_typ t1, e)
 
 and sub_extyp env s1 s2 ps =
   Trace.sub (lazy ("[sub_extyp] s1 = " ^ string_of_norm_extyp s1));
@@ -290,18 +333,11 @@ and sub_row env tr1 tr2 ps =
   | [] ->
     [], [], []
   | (l, t2)::tr2' ->
-    Trace.sub (lazy ("[sub_row] l = " ^ l));
     let ts1, zs1, f =
       try sub_typ env (List.assoc l tr1) t2 ps with
       | Not_found -> raise (Sub (Struct(l, Missing)))
       | Sub e -> raise (Sub (Struct(l, e)))
     in
-    let rec psubst p t =
-      match p with
-      | VarT(a, k) -> a, t
-      | AppT(p', ts) -> psubst p' (LamT(List.map unvarT ts, t))
-      | _ -> assert false
-    in
     let su = List.map2 psubst (Lib.List.take (List.length ts1) ps) ts1 in
     let ps' = Lib.List.drop (List.length ts1) ps in
     let ts2, zs2, fs = sub_row env tr1 (subst_row su tr2') ps' in
@@ -331,3 +367,76 @@ and equal_row env tr1 tr2 ps =
   let _, zs2, _ =
     try sub_row env tr2 tr1 ps with Sub e -> raise (Sub (Right e)) in
   zs1 @ zs2
+
+and match_typ env t1 t2 ps =
+  let t2 = norm_typ t2 in
+  Trace.sub (lazy ("[match_typ] t1 = " ^ string_of_norm_typ t1));
+  Trace.sub (lazy ("[match_typ] t2 = " ^ string_of_typ t2));
+  Trace.sub (lazy ("[match_typ] ps = " ^
+    String.concat ", " (List.map string_of_norm_typ ps)));
+  if not (has_typs_typ ps t2) then [], [] else
+  match norm_typ t1, freshen_typ env t2 with
+  | t1, FunT(aks21, t21, ExT(aks22, t22), Implicit) ->
+    assert (aks22 = []);
+    let su, zs = match_typ (add_typs aks21 env) t1 t22 ps in
+    List.map (fun (p, t) -> (p, LamT(aks21, t))) su, lift env zs
+
+  | FunT(aks11, t11, ExT(aks12, t12), Implicit), t2 ->
+    assert (aks12 = []);
+    let ts1, zs1 = guess_typs (Env.domain_typ env) aks11 in
+    let t1' = subst_typ (subst aks11 ts1) t12 in
+    let su, zs2 = match_typ env t1' t2 ps in
+    su, zs1 @ zs2
+
+  | TypT(s1), TypT(s2) ->
+    (match s1, s2 with
+    | ExT(aks1, t), ExT([], p) when List.mem p ps ->
+      if aks1 <> [] || not (!undecidable_flag || is_small_typ t) then
+         raise (Sub (Mismatch (t1, t2)));
+      [(p, t)], []
+    | _ ->
+      [], [])
+
+  | StrT(tr1), StrT(tr2) ->
+    match_row env tr1 tr2 ps
+
+  | FunT(aks1, t11, s1, Explicit p1), FunT(aks2, t21, s2, Explicit p2) ->
+    if p1 = Impure && p2 = Pure then raise (Sub (FunEffect(p1, p2)));
+    if p1 <> Pure || p2 <> Pure then
+      [], []
+    else
+      let env' = add_typs aks2 env in
+      let ts1, zs1, f1 =
+        try sub_typ env' t21 t11 (varTs aks1) with Sub e ->
+          raise (Sub (FunParam e)) in
+      let ps' = List.map (fun p -> AppT(p, varTs aks2)) ps in
+      let su, zs2 =
+        try match_extyp env' (subst_extyp (subst aks1 ts1) s1) s2 ps'
+        with Sub e -> raise (Sub (FunResult e)) in
+      List.map (function (AppT(p, _), t) -> (p, LamT(aks2, t))
+                       | _ -> assert false) su, lift env (zs1 @ zs2)
+
+  | _ ->
+    [], []
+
+and match_extyp env s1 s2 ps =
+  let ExT(aks2, t2) = freshen_extyp env s2 in
+  let ExT(aks1, t1) = freshen_extyp (add_typs aks2 env) s1 in
+  match aks1, aks2 with
+  | [], [] ->
+    match_typ env t1 t2 ps
+  | _ ->
+    [], []
+
+and match_row env tr1 tr2 ps =
+  match tr2 with
+  | [] ->
+    [], []
+  | (l, t2)::tr2' ->
+    let su1, zs1 =
+      try match_typ env (List.assoc l tr1) t2 ps with
+      | Not_found -> raise (Sub (Struct(l, Missing)))
+      | Sub e -> raise (Sub (Struct(l, e)))
+    in
+    let su2, zs2 = match_row env tr1 (subst_row (List.map (fun (p, t) -> psubst p t) su1) tr2') ps in
+    su1 @ su2, zs1 @ zs2

syntax.ml

@@ -28,6 +28,7 @@ and typ' =
   | EqT of exp
   | AsT of typ * typ
   | WithT of typ * var list * exp
+  | RecT of var * typ * typ
 
 and dec = (dec', unit) phrase
 and dec' =
@@ -218,13 +219,10 @@ let dotopE(x) =
 
 let recT(p, t2) =
   let b, t1 = p.it in
-  let e = TypE(t2)@@t2.at in
-  let e' =
-    match b.it with
-    | VarB(x, _) -> RecE(x, t1, e)
-    | EmptyB -> RecE("_"@@b.at, t1, e)
-    | _ -> RecE("$"@@b.at, t1, letE(b, e)@@span[b.at; e.at])
-  in PathT(e'@@span[p.at; t2.at])
+  match b.it with
+  | VarB(x, _) -> RecT(x, t1, t2)
+  | EmptyB -> RecT("_"@@b.at, t1, t2)
+  | _ -> RecT("$"@@b.at, t1, letT(b, t2)@@span[b.at; t2.at])
 
 let recE(p, e) =
   let b, t = p.it in
@@ -355,6 +353,7 @@ let label_of_typ t =
   | EqT _ -> "EqT"
   | AsT _ -> "AsT"
   | WithT _ -> "WithT"
+  | RecT _ -> "RecT"
 
 let label_of_dec d =
   match d.it with
@@ -409,6 +408,8 @@ let rec string_of_typ t =
   | AsT(t1, t2) -> node' [string_of_typ t1; string_of_typ t2]
   | WithT(t, xs, e) ->
     node' ([string_of_typ t] @ List.map string_of_var xs @ [string_of_exp e])
+  | RecT(x, b, t) ->
+    node' [string_of_var x; string_of_typ b; string_of_typ t]
 
 and string_of_dec d =
   let node' = node (label_of_dec d) in

talk.1ml

@@ -107,24 +107,23 @@ do map :
 
 ;; Objects
 
-type point' self =
-{
-  getX : () -> int;
-  getY : () -> int;
-  move : int -> int -> self;
+...rec {type point} => {
+  type point = {
+    getX : () -> int;
+    getY : () -> int;
+    move : int -> int -> point;
+  }
 };
-type recpoint = rec (x : type) => point' x;
-type point = point' recpoint;
 
 newpoint = rec (newpoint : int -> int -> point) => fun x y =>
-{
+@point {
   getX () = x;
   getY () = y;
-  move dx dy = @recpoint (newpoint (x + dx) (y + dy));
+  move dx dy = newpoint (x + dx) (y + dy);
 };
 
 p = newpoint 3 4;
-p' = (p.move 1 2).@recpoint;
+p' = (p.@point.move 1 2).@point;
 do Int.print (p'.getX ());
 do print " ";
 do Int.print (p'.getY ());

test.1ml

@@ -295,11 +295,11 @@ in {
 
 
 type int = primitive "int";
-type t = rec a => int;
+...rec {type t} => {type t = int};
 v = @t 3;
 n = v.@t;
 @t m = v;
-type u a = rec _ => a;
+u (type a) = rec (_: type) => a;
 w = @(u int) 4;
 @(u int) x = w;
 type p a b = (a,b);