Recursively dependent signatures

Author: polytypic

elab.ml

@@ -275,6 +275,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) <<<

readme.1ml

@@ -46,7 +46,7 @@ p = f (fun x => x)
 
 
 
-type stream = rec t => {hd : int, tl : () ~> opt t} ;; creates rec type
+...rec {type stream} => {type stream = {hd : int, tl : () ~> opt stream}} ;; creates rec type
 single x :@ stream = {hd = x, tl = fun () => none}  ;; b :@ t rolls value into t
 ({hd = n} :@ stream) = single 5        ;; p :@ t pattern matches on rec value
 do Int.print n                         ;; or:

regression.1ml

@@ -33,6 +33,30 @@ type DEC_PUNNING = {int, list}
 
 ;;
 
+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
 
@@ -220,11 +244,27 @@ type_error rec (R: {}) => {
   kaboom () = R
 }
 
-Kaboom = rec (R: rec R => {kaboom: () ~> R}) => {kaboom () = R} :@ (= R)
+;;Kaboom = rec (R: rec R => {kaboom: () ~> R}) => {kaboom () = R} :@ (= 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 _}
@@ -285,7 +325,7 @@ type (a `>>` b) c = c
 ;;
 
 Hungry = {
-  type eat a = rec eat_a => a ~> eat_a
+  ...rec {type eat a} => {type eat a = a ~> eat a}
 
   eater 'a = rec (eater: eat a) => (fun a => eater) :@ eat a
 
@@ -295,7 +335,7 @@ Hungry = {
 }
 
 PolyRec = {
-  type l a = rec (type t) => a | t
+  ...rec {type l a} => {type l a = a | l a}
   ...rec {type t a} => {type t a = a | t (a, a)}
 
   t_int = t int

sub.ml

@@ -153,6 +153,24 @@ let extract_bind infer_binds env tr1 l t2 =
     | None -> raise (Sub (Struct(l, Missing)))
     | Some (t, zs, e) -> t, zs, fun f _ _ -> IL.AppE(f, e)
 
+let rec has_typs_typ ps = function
+  | 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
+  | VarT(_)
+  | PrimT(_)
+  | WrapT(_)
+  | LamT(_)
+  | AppT(_)
+  | TupT(_)
+  | DotT(_)
+  | RecT(_)
+  | 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));
@@ -174,6 +192,24 @@ let rec sub_typ infer_binds env t1 t2 ps =
   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
@@ -335,7 +371,7 @@ let rec sub_typ infer_binds 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 infer_binds env s1 s2 ps =
   Trace.sub (lazy ("[sub_extyp] s1 = " ^ string_of_norm_extyp s1));
@@ -394,5 +430,79 @@ and equal_row env tr1 tr2 ps =
     try sub_row false 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 true 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 t1, zs, app = extract_bind true env tr1 l t2 in
+    let su1, zs1 =
+      try match_typ env t1 t2 ps with
+      | 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, zs @ zs1 @ zs2
+
 let sub_typ = sub_typ true
 let sub_extyp = sub_extyp true

syntax.ml

@@ -29,6 +29,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' =
@@ -228,13 +229,10 @@ type pat = {bind: bind; infer: typ option; annot: typ option}
 
 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, {it = VarE({it = "$"})}) -> 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, {it = VarE({it = "$"})}) -> 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
@@ -366,6 +364,7 @@ let label_of_typ t =
   | EqT _ -> "EqT"
   | AsT _ -> "AsT"
   | WithT _ -> "WithT"
+  | RecT _ -> "RecT"
 
 let label_of_dec d =
   match d.it with
@@ -422,6 +421,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
@@ -475,6 +476,7 @@ let rec imports_typ typ =
   | EqT exp -> imports_exp exp
   | AsT(typ1, typ2) -> imports_typ typ1 @ imports_typ typ2
   | WithT(typ, _, exp) -> imports_typ typ @ imports_exp exp
+  | RecT(_, typ1, typ2) -> imports_typ typ1 @ imports_typ typ2
 
 and imports_dec dec =
   match dec.it with

test.1ml

@@ -275,11 +275,11 @@ in {
 
 
 type int = primitive "int"
-type t = rec a => int
+...rec {type t} => {type t = int}
 v = 3 :@ t
 n = v @: t
 (m :@ t) = v
-type u a = rec _ => a
+...rec {type u a} => {type u a = a}
 w = 4 :@ u int
 (x :@ u int) = w
 ((x :@ t, y) :@ u (_, _)) = (6 :@ t, 7) :@ u (_, _)