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.

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

@@ -121,24 +121,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 *)
@@ -416,9 +432,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 ->
@@ -430,7 +445,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) -> ()
@@ -449,7 +464,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, []
@@ -474,7 +490,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
@@ -507,7 +523,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
@@ -524,14 +540,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)))
 
@@ -629,7 +644,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 _
 }