Change to infer (un)roll, (un)wrap, and un(roll|wrap) in elim forms

Subtyping is changed to look for cases where one (but not both) of the types is
a rolled type.  Either a roll or unroll is then generated depending on which of
the types `T1 <: T2` was a rolled type.

Also, in case one of the types is wrapped, but the other is not, then a wrap
or (pure) unwrap is generated.  Impure unwraps are not implicitly generated.

Also, elimination forms, like `if v then ... else ...` and `e.l`, try
to (purely) unwrap and unroll, as appropriate, the type of their input.

Together these changes largely eliminate the need to manually (un)roll
and (un)wrap.

Author: polytypic

README.md

@@ -341,14 +341,14 @@ This also shows that implicit functions naturally are first-class values.
 #### Recursive Types
 
 There are no datatype definitions, recursive types have to be defined
-explicitly, and require explicit injection/projection.
+explicitly, and sometimes require explicit annotations.
 
 ```1ml
 type stream = rec t => {hd : int, tl : () ~> opt t} ;; 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
+single x : stream = {hd = x, tl = fun () => none}  ;; b : t rolls value into t
+{hd = n} = single 5                    ;; pattern match rec value
 do Int.print n                         ;; or:
-do Int.print (single 7 @: stream).hd   ;; e @: t unrolls rec value directly
+do Int.print (single 7).hd             ;; access rec value
 ```
 
 #### Recursive Functions
@@ -359,16 +359,16 @@ The `rec` expression form allows defining recursive functions:
 count = rec self => fun i =>
   if i <> 0 then self (i - 1)
 
-repeat = rec self => fun x =>
-  {hd = x, tl = fun () => some (self x)} :@ stream
+repeat = rec self => fun x : stream =>
+  {hd = x, tl = fun () => some (self x)}
 ```
 
 Mutual recursion is also expressible:
 
 ```1ml
 {even, odd} = rec (self : {even : int ~> stream, odd : int ~> stream}) => {
-  even x :@ stream = {hd = x, tl = fun () => some (self.odd (x + 1))}
-  odd x :@ stream = {hd = x, tl = fun () => some (self.even (x + 1))}
+  even x : stream = {hd = x, tl = fun () => some (self.odd (x + 1))}
+  odd x : stream = {hd = x, tl = fun () => some (self.even (x + 1))}
 }
 ```
 
@@ -392,13 +392,15 @@ Opt :> OPT = {
   ;; Church encoding; it requires the abstract type opt a to be implemented
   ;; with a polymorphic (i.e., large) type. Thus, wrap the type.
   type opt a = wrap (b : type) -> b -> (a ~> b) ~> b
-  none :# opt _ = fun (b : type) (n : b) (s : _ ~> b) => n
-  some x :# opt _ = fun (b : type) (n : b) (s : _ ~> b) => s x
-  caseopt (xo :# opt _) = xo _
+  none (b : type) (n : b) (s : _ ~> b) = n
+  some x (b : type) (n : b) (s : _ ~> b) = s x
+  caseopt (xo : opt _) = xo _
 }
 ```
 
-Note how values of type `wrap T` have to be wrapped and unwrapped explicitly.
+Values of type `T` can be implicitly wrapped to `wrap T` and, in case `wrap T`
+contains no abstract types, can be implicitly unwrapped to `T`. In case `wrap T`
+contains abstract types, unwrapping must be done explicitly.
 
 ---
 

elab.ml

@@ -123,24 +123,40 @@ and paths_row ta ps = function
 
 
 let rec_from_extyp typ label s =
-  match s with
-  | ExT([], t) ->
-    let rec find_rec = function
-      | AppT(t, ts) ->
-        let rec_t, unroll_t, roll_t, ak = find_rec t in
-        rec_t, AppT(unroll_t, ts), AppT(roll_t, ts), ak
-      | RecT(ak, unroll_t) as rec_t ->
-        rec_t, unroll_t, rec_t, ak
-      | DotT(t, lab) ->
-        let rec_t, unroll_t, roll_t, ak = find_rec t in
-        rec_t, DotT(unroll_t, lab), DotT(roll_t, lab), ak
-      | _ ->
-        error typ.at ("non-recursive type for " ^ label ^ ":"
-                      ^ " " ^ Types.string_of_extyp s) in
-    find_rec t
-  | _ ->
+  match try_rec_from_extyp s with
+  | Some r -> r
+  | None ->
     error typ.at ("non-recursive type for " ^ label ^ ":"
-                  ^ " " ^ Types.string_of_extyp s)
+                  ^ " " ^ string_of_extyp s)
+
+
+let try_unwrap (t, zs, e) =
+  match t with
+  | WrapT(ExT([], t)) -> Some (t, zs, IL.DotE(e, "wrap"))
+  | _ -> None
+
+let try_unroll (t, zs, e) =
+  try_rec_from_typ t
+   |> Lib.Option.map (fun (unroll_t, roll_t) ->
+      unroll_t, zs, IL.UnrollE(e))
+
+let try_peel r =
+  try_unwrap r |> Lib.Option.orelse (fun () -> try_unroll r)
+
+let avar fn r = fn r
+
+let anexp fn r =
+  match r with
+  | ExT([], t), p, zs, e ->
+    fn (t, zs, e)
+     |> Lib.Option.map (fun (t, zs, e) ->
+        ExT([], t), p, zs, e)
+  | _ -> None
+
+let rec fully fn pre r =
+  match pre fn r with
+  | None -> r
+  | Some r -> fully fn pre r
 
 
 (* Instantiation *)
@@ -418,9 +434,8 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain
 
   | EL.RollE(var, typ) ->
     let s, zs1 = elab_typ env typ l in
-    let rec_t, unroll_t, roll_t, ak = rec_from_extyp typ "rolling" s in
+    let unroll_t, roll_t = rec_from_extyp typ "rolling" s in
     let var_t = lookup_var env var in
-    let unroll_t = subst_typ (subst [ak] [rec_t]) unroll_t in
     let _, zs2, f =
       try sub_typ env var_t unroll_t []
       with Sub e ->
@@ -432,7 +447,7 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain
     IL.RollE(IL.AppE(f, IL.VarE(var.it)), erase_typ roll_t)
 
   | EL.IfE(var, exp1, exp2) ->
-    let t0, zs0, ex = elab_instvar env var in
+    let t0, zs0, ex = fully try_peel avar (elab_instvar env var) in
     let _ =
       match t0 with
       | PrimT(Prim.BoolT) -> ()
@@ -451,7 +466,8 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain
     IL.IfE(ex, IL.AppE(f1, e1), IL.AppE(f2, e2))
 
   | EL.DotE(exp1, var) ->
-    let ExT(aks, t), p, zs1, e1 = elab_instexp env exp1 "" in
+    let ExT(aks, t), p, zs1, e1 =
+      fully try_peel anexp (elab_instexp env exp1 "") in
     let tr, zs2 =
       match t with
       | StrT(tr) -> tr, []
@@ -476,7 +492,7 @@ Trace.debug (lazy ("[DotE] s = " ^ string_of_extyp s));
         IL.DotE(IL.VarE("x"), var.it), erase_extyp s))
 
   | EL.AppE(var1, var2) ->
-    let tf, zs1, ex1 = elab_instvar env var1 in
+    let tf, zs1, ex1 = fully try_peel avar (elab_instvar env var1) in
 Trace.debug (lazy ("[AppE] tf = " ^ string_of_norm_typ tf));
     let aks1, t1, s, p, zs =
       match freshen_typ env tf with
@@ -509,7 +525,7 @@ Trace.debug (lazy ("[AppE] ts = " ^ String.concat ", " (List.map string_of_norm_
         let ExT(aks, t) as s2 = freshen_extyp env s2 in
         aks, t, s2, zs2
       | _ -> error typ.at "non-wrapped type for unwrap" in
-    let t1, zs1, ex = elab_instvar env var in
+    let t1, zs1, ex = fully try_unroll avar (elab_instvar env var) in
     let s1 =
       match t1 with
       | WrapT(s1) -> s1
@@ -526,14 +542,13 @@ Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2));
 
   | EL.UnrollE(var, typ) ->
     let s, zs1 = elab_typ env typ l in
-    let rec_t, unroll_t, roll_t, ak = rec_from_extyp typ "unrolling" s in
+    let unroll_t, roll_t = rec_from_extyp typ "unrolling" s in
     let var_t = lookup_var env var in
     let _, zs2, f = try sub_typ env var_t roll_t [] with Sub e ->
       error var.at ("unrolled value does not match annotation:"
                     ^ "  " ^ Types.string_of_typ var_t ^ " "
                     ^ "<"
                     ^ "  " ^ Types.string_of_typ roll_t) in
-    let unroll_t = subst_typ (subst [ak] [rec_t]) unroll_t in
     ExT([], unroll_t), Pure, zs1 @ zs2,
     IL.UnrollE(IL.AppE(f, IL.VarE(var.it)))
 
@@ -631,7 +646,8 @@ and elab_bind env bind l =
         erase_extyp s))
 
   | EL.InclB(exp) ->
-    let ExT(aks, t) as s, p, zs, e = elab_instexp env exp l in
+    let ExT(aks, t) as s, p, zs, e =
+      fully try_peel anexp (elab_instexp env exp l) in
     (match t with
     | StrT(tr) -> ()
     | InferT(z) -> resolve_always z (StrT[])  (* TODO: row polymorphism *)

examples/fc.1ml

@@ -17,16 +17,13 @@ GADTs = {
         Succ       :      t int ~> case int
         Pair 'a 'b : t a ~> t b ~> case (a, b)
       }
-      type T (type t _) a = (m: I t) ~> m.case a
-      ...rec {type t _} => {type t a = wrap T t a}
-      T = T t
+      ...rec {type t _} => {type t a = wrap (m: I t) ~> m.case a}
       I = I t
-      mk (fn: T _) = fn :# wrap T _ :@ t _
     t
-    case (m: I) (e :# wrap T _ :@ t _) = e m
-    Zero     : t _ = mk fun (m: I) => m.Zero
-    Succ x   : t _ = mk fun (m: I) => m.Succ x
-    Pair l r : t _ = mk fun (m: I) => m.Pair l r
+    case (m: I) (e: t _) = e m
+    Zero     : t _ = fun (m: I) => m.Zero
+    Succ x   : t _ = fun (m: I) => m.Succ x
+    Pair l r : t _ = fun (m: I) => m.Pair l r
   }
 
   eval = rec (eval 'a: Exp.t a ~> a) =>

examples/hoas.1ml

@@ -18,9 +18,8 @@ let
   type T (type t _) x = (c: J t) ~> c.case x
   ...{
     ...rec {type t _} => {type t x = wrap T t x}
-    case 'x (type case _) (cs: I case t) (e :# wrap T t x :@ t _) =
-      e {case, ...cs}
-    mk 'x (fn: T t x) = fn :# wrap T t x :@ t _
+    case 'x (type case _) (cs: I case t) (e: t _) = e {case, ...cs}
+    mk (fn: T t _) = fn
   } :> {
     type t _
     case 'x: (type case _) -> I case t -> t x ~> case x

examples/trie.1ml

@@ -8,17 +8,14 @@ FunctionalTrie = {
       alt  'v 'k1 'k2 : t k1 v ~> t k2 v ~> case (alt k1 k2) v
       pair 'v 'k1 'k2 : t k1 (t k2 v)    ~> case (k1, k2) v
     }
-    type T (type t _ _) k v = (m: I t) ~> m.case k v
-    ...rec {type t _ _} => {type t k v = wrap T t k v}
-    T = T t
+    ...rec {type t _ _} => {type t k v = wrap (m: I t) ~> m.case k v}
     I = I t
-    mk (fn: T _ _) = fn :# wrap T _ _ :@ t _ _
 
   t
-  case (m: I) (e :# wrap T _ _ :@ t _ _) = e m
-  unit vO : t _ _ = mk fun (m: I) => m.unit vO
-  alt l r : t _ _ = mk fun (m: I) => m.alt l r
-  pair lr : t _ _ = mk fun (m: I) => m.pair lr
+  case (m: I) (e: t _ _) = e m
+  unit vO : t _ _ = fun (m: I) => m.unit vO
+  alt l r : t _ _ = fun (m: I) => m.alt l r
+  pair lr : t _ _ = fun (m: I) => m.pair lr
 
   lookup = rec (lookup 'k 'v: t k v ~> k ~> opt v) =>
     case {

import.ml

@@ -9,11 +9,6 @@ let sig_ext = ".1mls"
 let index_file = "index"
 let modules_dir = "node_modules"
 
-let (<|>) xO uxO =
-  match xO with
-  | None -> uxO ()
-  | some -> some
-
 let finish path =
   if Lib.Sys.file_exists_at path
      || Lib.Sys.file_exists_at (Lib.Filename.replace_ext mod_ext sig_ext path)
@@ -29,12 +24,13 @@ let complete path =
     finish (path ^ mod_ext)
 
 let rec search_modules prefix suffix =
-  complete (Filename.concat prefix modules_dir ^ "/" ^ suffix) <|> fun () ->
-  let parent = Filename.dirname prefix in
-  if parent = prefix then
-    None
-  else
-    search_modules parent suffix
+  complete (Filename.concat prefix modules_dir ^ "/" ^ suffix)
+   |> Lib.Option.orelse (fun () ->
+      let parent = Filename.dirname prefix in
+      if parent = prefix then
+        None
+      else
+        search_modules parent suffix)
 
 let resolve parent path =
   let path = Lib.Filename.canonic path in
@@ -50,5 +46,6 @@ let resolve parent path =
           || Lib.Sys.directory_exists_at parent then
     complete (Lib.Filename.canonic (Filename.dirname parent ^ "/" ^ path))
   else
-    search_modules (Filename.dirname parent) path <|> fun () ->
-    complete (std_dir ^ "/" ^ path)
+    search_modules (Filename.dirname parent) path
+     |> Lib.Option.orelse (fun () ->
+        complete (std_dir ^ "/" ^ path))

lib.ml

@@ -113,4 +113,8 @@ struct
       | [] -> Some ys
       | x::xs -> bind (xyO x) @@ fun y -> loop (y::ys) xs in
     loop [] xs |> map List.rev
+
+  let orelse alt = function
+    | None -> alt ()
+    | some -> some
 end

lib.mli

@@ -43,4 +43,5 @@ sig
   val map: ('a -> 'b) -> 'a option -> 'b option
   val bind: 'a option -> ('a -> 'b option) -> 'b option
   val traverse: ('a -> 'b option) -> 'a list -> 'b list option
+  val orelse: (unit -> 'a option) -> 'a option -> 'a option
 end

prelude/index.1ml

@@ -26,10 +26,10 @@ Alt :> {
   inr 'a 'b: b -> t a b
   case 'a 'b 'o: {inl: a ~> o, inr: b ~> o} -> t a b ~> o
 } = {
-  type t a b = wrap 'o -> {inl: a ~> o, inr: b ~> o} ~> o
-  inl x :# t _ _ = fun c => c.inl x
-  inr x :# t _ _ = fun c => c.inr x
-  case c (x :# t _ _) = x c
+  type t a b = wrap (type o) -> {inl: a ~> o, inr: b ~> o} ~> o
+  inl x (type o) c : o = c.inl x
+  inr x (type o) c : o = c.inr x
+  case c (x : t _ _) = x _ c
 }
 
 Alt = {
@@ -55,11 +55,10 @@ Pair = {
 }
 
 List = {
-  local ...Opt, ...Fun
   ...rec {type t _} => {type t x = Opt.t (x, t x)}
-  nil :@ t _ = none
-  hd :: tl :@ t _ = some (hd, tl)
-  case {nil, (::)} (x :@ t _) = x |> Opt.case {
+  nil = Opt.none
+  hd :: tl = Opt.some (hd, tl)
+  case {nil, (::)} = Opt.case {
     none = nil
     some (hd, tl) = hd :: tl
   }

readme.1ml

@@ -47,25 +47,25 @@ p = f (fun x => x)
 
 
 type stream = rec t => {hd : int, tl : () ~> opt t} ;; 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
+single x : stream = {hd = x, tl = fun () => none}  ;; b : t rolls value into t
+{hd = n} = single 5                    ;; pattern match rec value
 do Int.print n                         ;; or:
-do Int.print (single 7 @: stream).hd   ;; e @: t unrolls rec value directly
+do Int.print (single 7).hd             ;; access rec value
 
 
 
 
 count = rec self => fun i =>
   if i <> 0 then self (i - 1)
 
-repeat = rec self => fun x =>
-  {hd = x, tl = fun () => some (self x)} :@ stream
+repeat = rec self => fun x : stream =>
+  {hd = x, tl = fun () => some (self x)}
 
 
 
 {even, odd} = rec (self : {even : int ~> stream, odd : int ~> stream}) => {
-  even x :@ stream = {hd = x, tl = fun () => some (self.odd (x + 1))}
-  odd x :@ stream = {hd = x, tl = fun () => some (self.even (x + 1))}
+  even x : stream = {hd = x, tl = fun () => some (self.odd (x + 1))}
+  odd x : stream = {hd = x, tl = fun () => some (self.even (x + 1))}
 }
 
 
@@ -80,7 +80,7 @@ Opt :> OPT = {
   ;; Church encoding; it requires the abstract type opt a to be implemented
   ;; with a polymorphic (i.e., large) type. Thus, wrap the type.
   type opt a = wrap (b : type) -> b -> (a ~> b) ~> b
-  none :# opt _ = fun (b : type) (n : b) (s : _ ~> b) => n
-  some x :# opt _ = fun (b : type) (n : b) (s : _ ~> b) => s x
-  caseopt (xo :# opt _) = xo _
+  none (b : type) (n : b) (s : _ ~> b) = n
+  some x (b : type) (n : b) (s : _ ~> b) = s x
+  caseopt (xo : opt _) = xo _
 }