Remove T_abs with (Path = T_sub) and add T_abs & T_sub syntax...

...for type refinement.

The new

    T_abs & T_sub

mechanism is similar to the old

    T_abs with (Path = T_sub)

mechanism and also to the include mechanism

    {...T_abs; ...T_sub}

The main difference is that, instead of using a path to target a specific
substructure or requiring that no declarations overlap, an intersection,
`T_int`, of the nested declarations of `T_abs` and `T_sub`, is computed.

Then it is checked whether `T_abs :> T_int` and if so a substitution, `𝛿`, is
obtained.  Finally the nested declarations of `𝛿(T_abs)` and `T_sub` are merged.

Also, in `T1 & T2` both `T1` and `T2` are elaborated in the same environment
whereas in `{...T1; ...T2}` the environment for `T2` includes declarations from
`T1` and in `T1 with (P = T2)` the path `P` is specific to `T1`.

When defined, `T1 & T2` is always a subtype of both `T1` and `T2`

    T1 & T2  :>  T1
    T1 & T2  :>  T2

README.md

@@ -90,7 +90,7 @@ T ::=
     (X : T) -> E            (pure function/functor/constructor type)
     '(X : T) -> E           (implicit function/functor/constructor type)
     (= E)                   (singleton/alias type)
-    T with .Xs = E          (type refinement)
+    T & T                   (type refinement)
     wrap T                  (impredicative wrapped type)
     _                       (type wildcard)
     T as T                  (layered type (both operands have to be equal))
@@ -153,8 +153,6 @@ T ::= ...
     T1 -> T2                        ~> (_ : T1) -> T2
     P ~> T                          ~> ($ : TP) ~> let P in T  [2]
     P -> T                          ~> ($ : TP) -> let P in T  [2]
-    T with .Xs A1 ... An = E        ~> T with .Xs = fun A1 ... An => E
-    T with type .Xs A1 ... An = T'  ~> T with .Xs = fun A1 ... An => type T'
     let B in T                      ~> (let B in type T)
     rec P => T                      ~> (rec P => type T)
 

basis/index.1ml

@@ -19,7 +19,7 @@ type SET = {
   card : set ~> int
 }
 
-Set (Elem : ORD) :> SET with (elem = Elem.t) = {
+Set (Elem : ORD) :> SET & {elem = Elem.t} = {
   type elem = Elem.t
   x == y = let ...Elem in (x <= y) && (y <= x)
   type set = (int, elem ~> bool)
@@ -44,7 +44,7 @@ type MAP = {
   lookup 'a : key -> map a ~> opt a
 }
 
-Map (Key : ORD) :> MAP with (key = Key.t) = {
+Map (Key : ORD) :> MAP & {key = Key.t} = {
   type key = Key.t
   x == y = let ...Key in (x <= y) && (y <= x)
   type map a = key ~> opt a

elab.ml

@@ -268,27 +268,29 @@ let rec elab_typ env typ l =
     in
     s1, lift_warn typ.at t1 (add_typs aks1 env) (zs1 @ zs2 @ zs3)
 
-  | EL.WithT(typ1, vars, exp) ->
-    let t2, zs2 = elab_pathexp env exp l in
-    let ExT(aks1, t1), zs1 = elab_typ env typ1 l in
-    let ls = List.map (fun var -> var.it) vars in
-Trace.debug (lazy ("[WithT] s1 = " ^ string_of_norm_extyp (ExT(aks1, t1))));
-Trace.debug (lazy ("[WithT] ls = " ^ String.concat "." ls));
-Trace.debug (lazy ("[WithT] t2 = " ^ string_of_norm_typ t2));
-    let ta = try project_typ ls t1 with Not_found ->
-      error typ.at ("path " ^ quote (String.concat "." ls) ^ " unbound") in
-Trace.debug (lazy ("[WithT] ta = " ^ string_of_norm_typ ta));
-    let bs = vars_typ ta in
-    let aks11 = List.filter (fun (a, k) -> not (VarSet.mem a bs)) aks1 in
-    let aks12 = List.filter (fun (a, k) -> VarSet.mem a bs) aks1 in
-Trace.debug (lazy ("[WithT] aks11 = " ^ string_of_norm_extyp (ExT(aks11, StrT []))));
-Trace.debug (lazy ("[WithT] aks12 = " ^ string_of_norm_extyp (ExT(aks12, StrT []))));
+  | EL.AndT(typ1, typ2) ->
+    let s1', zs1 = elab_typ env typ1 l in
+    let s2', zs2 = elab_typ env typ2 l in
+    let ExT(aks1, t1) as s1 = freshen_extyp env s1' in
+    let ExT(aks2, t2) as s2 = freshen_extyp (add_typs aks1 env) s2' in
+Trace.debug (lazy ("[AndT] s1 = " ^ string_of_norm_extyp s1));
+Trace.debug (lazy ("[AndT] s2 = " ^ string_of_norm_extyp s2));
+    let ti = intersect_typs t1 t2 in
+Trace.debug (lazy ("[AndT] ti = " ^ string_of_norm_typ ti));
+    let vi = vars_typ ti in
+    let aksi = List.filter (fun (a, k) -> VarSet.mem a vi) aks1 in
+Trace.debug (lazy ("[AndT] aksi = " ^ string_of_norm_extyp (ExT(aksi, StrT []))));
+    let aks = aks1 @ aks2 in
     let ts, zs3, _ =
-      try sub_typ env t2 ta (varTs aks12) with Sub e -> error exp.at
-        ("refinement type does not match type component: " ^ Sub.string_of_error e)
-    in
-    ExT(aks11, subst_typ (subst aks12 ts) t1),
-    lift_warn typ.at t1 (add_typs aks11 env) (zs1 @ zs2 @ zs3)
+      try sub_typ (add_typs aks env) t2 ti (varTs aksi) with Sub e ->
+        error typ.at ("type refinement does not match: " ^ Sub.string_of_error e) in
+Trace.debug (lazy ("[AndT] ts = " ^ String.concat ", " (List.map string_of_norm_typ ts)));
+    let t = merge_typs (subst_typ (subst (Lib.List.take (List.length ts) aksi) ts) t1) t2 in
+Trace.debug (lazy ("[AndT] t = " ^ string_of_norm_typ t));
+    let vt = vars_typ t in
+    let s = ExT(List.filter (fun (a, k) -> VarSet.mem a vt) aks, t) in
+Trace.debug (lazy ("[AndT] s = " ^ string_of_norm_extyp s));
+    s, lift_warn typ.at t env (zs1 @ zs2 @ zs3)
 
 and elab_dec env dec l =
   Trace.elab (lazy ("[elab_dec] " ^ EL.label_of_dec dec));

examples/fc.1ml

@@ -48,12 +48,14 @@ AssociatedTypes = {
     insert: Elem.t -> t ~> t
   }
 
-  CollectEq (Elem: EQ) :> COLLECTS with (Elem = Elem) = {
+  CollectEq (Elem: EQ) :> COLLECTS & {Elem} = {
+    Elem
     empty = List.nil
     insert = List.::
   }
 
-  BitSet :> COLLECTS with (Elem = Char) = {
+  BitSet :> COLLECTS & {Elem = Char} = {
+    Elem = Char
     empty = List.nil
     insert = List.::
   }

lexer.mll

@@ -98,6 +98,7 @@ module Offside = struct
 
   let slack_of token =
     match token with
+    | AMP -> 2
     | SYM text -> String.length text + 1
     | _ -> 0
 
@@ -280,7 +281,7 @@ rule token = parse
   | "rec" { REC }
   | "then" { THEN }
   | "type" { TYPE }
-  | "with" { WITH }
+  | "&" { AMP }
   | "=" { EQUAL }
   | ":" { COLON }
   | ":>" { SEAL }

paper.1ml

@@ -65,7 +65,7 @@ type MAP = {
   lookup : (a : type) -> key -> map a ~> opt a
 }
 
-Map (Key : EQ) :> MAP with (type key = Key.t) = {
+Map (Key : EQ) :> MAP & {key = Key.t} = {
   type key = Key.t
   type map a = key ~> opt a
   empty (a : type) = fun (k : key) => none
@@ -141,7 +141,7 @@ joinM (M : MONAD) (a : type) (mm : M.t (M.t a)) : M.t a =
   M.bind (M.t a) a mm (fun (m : M.t a) => m)
 
 StackM (M : MONAD) =
-  rec (Loop : (n : int) ~> (MONAD_TRANS with (base = M.t))) =>
+  rec (Loop : (n : int) ~> (MONAD_TRANS & {base = M.t})) =>
   fun (n : int) =>
   if n == 1 then
     { ... M
@@ -162,7 +162,7 @@ StackM (M : MONAD) =
           (fun (mx : M.t a) => M.bind a b mx
             (fun (x : a) => f x))
     }
-  ) : MONAD_TRANS with (type base a = M.t a)
+  ) : MONAD_TRANS & {base = M.t}
 ;)
 
 ;; Predicativity
@@ -213,7 +213,7 @@ type MAP = {
   lookup 'a : key -> map a ~> opt a
   add 'a : key -> a -> map a ~> map a
 }
-Map (Key : EQ) :> MAP with (type key = Key.t) = {
+Map (Key : EQ) :> MAP & {key = Key.t} = {
   type key = Key.t
   type map a = key ~> opt a
   empty = fun x => none

parser.mly

@@ -29,7 +29,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %token FUN REC LET IN DO WRAP TYPE ELLIPSIS
 %token IF THEN ELSE LOGICAL_OR LOGICAL_AND AS
 %token EQUAL COLON SEAL ARROW SARROW DARROW
-%token WITH
+%token AMP
 %token LPAR RPAR
 %token LBRACE RBRACE
 %token DOT TICK
@@ -123,13 +123,6 @@ label :
     { index($1)@@at() }
 ;
 
-path :
-  | label
-    { $1::[] }
-  | label DOT path
-    { $1::$3 }
-;
-
 infixtyp :
   | TYPE typparam sym typparam
     { ($3, [$2; $4]) }
@@ -226,20 +219,18 @@ attyp :
   | LPAR EQUAL exp RPAR
     { EqT($3)@@at() }
 ;
-withtyp :
+andtyp :
   | infpathexp
     { pathT($1)@@at() }
-  | withtyp WITH LPAR path typparamlist EQUAL exp RPAR
-    { WithT($1, $4, funE($5, $7)@@span[ati 5; ati 7])@@at() }
-  | withtyp WITH LPAR TYPE path typparamlist typdef RPAR
-    { WithT($1, $5, funE($6, $7)@@span[ati 6; ati 7])@@at() }
+  | infpathexp AMP andtyp
+    { AndT(pathT($1)@@ati 1, $3)@@at() }
 ;
 typ :
-  | withtyp
+  | andtyp
     { $1 }
   | annparam arrow typ
     { funT([$1], $3, $2)@@at() }
-  | withtyp arrow typ
+  | andtyp arrow typ
     { funT([(headB("_"@@ati 1)@@ati 1, $1, Expl@@ati 2)@@ati 1], $3, $2)@@at() }
   | WRAP typ
     { WrapT($2)@@at() }

prelude.1ml

@@ -208,7 +208,7 @@ type SET = {
   card : set -> int
 }
 
-Set (Elem : ORD) :> SET with (elem = Elem.t) = {
+Set (Elem : ORD) :> SET & {elem = Elem.t} = {
   type elem = Elem.t
   x == y = let ...Elem in (x <= y) && (y <= x)
   type set = (int, elem ~> bool)
@@ -233,7 +233,7 @@ type MAP = {
   lookup 'a : key -> map a ~> opt a
 }
 
-Map (Key : ORD) :> MAP with (key = Key.t) = {
+Map (Key : ORD) :> MAP & {key = Key.t} = {
   type key = Key.t
   x == y = let ...Key in (x <= y) && (y <= x)
   type map a = key ~> opt a

regression.1ml

@@ -159,6 +159,28 @@ Monadic = {
 
 ;;
 
+ExpressiveLanguageOfSignatures = {
+  type T = {type t, type u, x: t}
+  type V = {type t, type u, x: u}
+
+  type_error { type L = T & V }
+
+  type L1 = T & V & {type t, u = t}
+  type L2 = T & V & {x 'a: a}
+}
+
+And = {
+  type Reveal = {type t, x: t} & {t = int}
+  type Nested = {Nested: {type t, v: t}, x: Nested.t} & {Nested: {t = int}}
+  type RevealWithPath = {type t, toText: t ~> text} & (= Int)
+
+  type RDS = {A: {type t}, B: {type t}}
+           & {A: {type t}, B: {v: A.t}}
+           & {B: {type t}, A: {v: B.t}}
+}
+
+;;
+
 hole_is_allowed_type_pattern (type _ _) = ()
 
 typparams_allowed (id 'a: a -> a) ({alsoId 'x: x -> x}) =

syntax.ml

@@ -28,7 +28,7 @@ and typ' =
   | WrapT of typ
   | EqT of exp
   | AsT of typ * typ
-  | WithT of typ * var list * exp
+  | AndT of typ * typ
 
 and dec = (dec', unit) phrase
 and dec' =
@@ -396,7 +396,7 @@ let label_of_typ t =
   | WrapT _ -> "WrapT"
   | EqT _ -> "EqT"
   | AsT _ -> "AsT"
-  | WithT _ -> "WithT"
+  | AndT _ -> "AndT"
 
 let label_of_dec d =
   match d.it with
@@ -451,8 +451,8 @@ let rec string_of_typ t =
   | WrapT(t) -> node' [string_of_typ t]
   | EqT(e) -> node' [string_of_exp e]
   | 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])
+  | AndT(t1, t2) ->
+    node' [string_of_typ t1; string_of_typ t2]
 
 and string_of_dec d =
   let node' = node (label_of_dec d) in
@@ -505,7 +505,7 @@ let rec imports_typ typ =
   | WrapT typ -> 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
+  | AndT(typ1, typ2) -> imports_typ typ1 @ imports_typ typ2
 
 and imports_dec dec =
   match dec.it with

talk.1ml

@@ -37,7 +37,7 @@ type MAP = {
   add : (a : type) -> key -> a -> map a ~> map a
 }
 
-Map (Key : EQ) :> MAP with (type key = Key.t) = {
+Map (Key : EQ) :> MAP & {key = Key.t} = {
   type key = Key.t
   type map a = key ~> opt a
   empty (a : type) = fun (x : key) => none
@@ -57,7 +57,7 @@ type MAP = {
   add 'a : key -> a -> map a ~> map a
 }
 
-Map (Key : EQ) :> MAP with (type key = Key.t) = {
+Map (Key : EQ) :> MAP & {key = Key.t} = {
   type key = Key.t
   type map a = key ~> opt a
   empty = fun x => none

test.1ml

@@ -214,7 +214,7 @@ type SET = {
   card : set ~> int
 }
 
-Set (Elem : ORD) :> SET with (elem = Elem.t) = {
+Set (Elem : ORD) :> SET & {elem = Elem.t} = {
   type elem = Elem.t
   type set = (int, elem ~> bool)
   type t = set
@@ -237,7 +237,7 @@ type MAP = {
   lookup 'a : key -> map a ~> opt a
 }
 
-Map (Key : ORD) :> MAP with (key = Key.t) = {
+Map (Key : ORD) :> MAP & {key = Key.t} = {
   type key = Key.t
   type map a = key ~> opt a
   t = map

types.ml

@@ -111,12 +111,53 @@ let intersect_row r1 r2 =
 let diff_row r1 r2 =
   List.filter (fun (l1, _) -> List.for_all (fun (l2, _) -> l1 <> l2) r2) r1
 
-let rec project_typ ls t =
-  match ls, t with
-  | [], _ -> t
-  | l::ls', StrT(tr) -> project_typ ls' (List.assoc l tr)
-  | _ -> raise Not_found
-
+let rec intersect_typs t1 t2 =
+  match t1, t2 with
+  | StrT(r1), StrT(r2) ->
+    StrT(intersect_row r1 r2
+         |> List.map (fun (l, t1) ->
+                (l, intersect_typs t1 (List.assoc l r2))))
+  | _ ->
+    t1
+
+let rec has_typs = function
+  | VarT(_) -> false
+  | PrimT(_) -> false
+  | StrT(tr) -> List.exists (fun (_, t) -> has_typs t) tr
+  | FunT(aks, td, ExT(_, tr), e) ->
+    (match e with
+     | Implicit | Explicit Pure ->
+       has_typs tr
+     | Explicit Impure -> false)
+  | TypT(ExT(_, p)) -> true
+  | WrapT(_) -> false
+  | LamT(_) -> false
+  | AppT(_) -> false
+  | TupT(_) -> false
+  | DotT(_) -> false
+  | RecT(_) -> false
+  | InferT(_) -> false
+
+let rec merge_typs t1 t2 =
+  match t1, t2 with
+  | StrT(r1), StrT(r2) ->
+    let ls = List.map fst r1 @
+      List.filter (fun l -> not (List.mem_assoc l r1)) (List.map fst r2) in
+    let merge kind =
+      ls
+      |> List.filter (fun l ->
+          List.mem_assoc l r1 && kind (List.assoc l r1) ||
+          List.mem_assoc l r2 && kind (List.assoc l r2))
+      |> List.map (fun l ->
+          if List.mem_assoc l r1 && List.mem_assoc l r2 then
+            (l, merge_typs (List.assoc l r1) (List.assoc l r2))
+          else if List.mem_assoc l r2 then
+            (l, List.assoc l r2)
+          else
+            (l, List.assoc l r1)) in
+    StrT(merge has_typs @ merge (fun t -> not (has_typs t)))
+  | _ ->
+    t2
 
 (* Size check *)
 

types.mli

@@ -97,7 +97,8 @@ val map_rowi : (lab -> 'a -> 'b) -> 'a row -> 'b row
 val intersect_row : 'a row -> 'a row -> 'a row
 val diff_row : 'a row -> 'a row -> 'a row
 
-val project_typ : lab list -> typ -> typ (* raise Not_found *)
+val intersect_typs : typ -> typ -> typ
+val merge_typs : typ -> typ -> typ
 
 
 (* Size check *)