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,21 @@
+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;
 
@@ -38,6 +56,22 @@ type_error {
 
 ;;
 
+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 = {
   T = rec (R: {
     Even: {type t _};
@@ -76,7 +110,7 @@ Mutually = {
   };
 };
 
-Mutually = {
+Mutually :> MUTUALLY = {
   Even = {...Mutually.T.Even; ...Mutually.V.Even};
   Odd = {...Mutually.T.Odd; ...Mutually.V.Odd};
 
@@ -86,7 +120,7 @@ Mutually = {
 ;;
 
 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);
 
@@ -96,7 +130,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

@@ -101,12 +101,31 @@ 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
+      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 +286,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 +309,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 +343,67 @@ 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 =
+  Trace.sub (lazy ("[match_typ] t1 = " ^ string_of_norm_typ t1));
+  Trace.sub (lazy ("[match_typ] t2 = " ^ string_of_norm_typ t2));
+  Trace.sub (lazy ("[match_typ] ps = " ^
+    String.concat ", " (List.map string_of_norm_typ ps)));
+  match norm_typ t1, freshen_typ env (norm_typ 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 ->
+    [], []
+
+  | 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)));
+    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' =
@@ -210,13 +211,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
@@ -344,6 +342,7 @@ let label_of_typ t =
   | EqT _ -> "EqT"
   | AsT _ -> "AsT"
   | WithT _ -> "WithT"
+  | RecT _ -> "RecT"
 
 let label_of_dec d =
   match d.it with
@@ -398,6 +397,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 @@ end;
 
 
 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);