Change to attempt to infer wrapped and folded types

Author: polytypic

README.md

@@ -346,9 +346,9 @@ explicitly, and require explicit injection/projection.
 ```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
-do Int.print n                         ;; or:
-do Int.print (single 7 @: stream).hd   ;; e @: t unrolls rec value directly
+({hd = n} :@ _) = single 5        ;; p :@ t pattern matches on rec value
+do Int.print n                    ;; or:
+do Int.print (single 7 @: _).hd   ;; e @: t unrolls rec value directly
 ```
 
 #### Recursive Functions
@@ -392,8 +392,8 @@ 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
+  none :# _ = fun (b : type) (n : b) (s : _ ~> b) => n
+  some x :# _ = fun (b : type) (n : b) (s : _ ~> b) => s x
   caseopt (xo :# opt _) = xo _
 }
 ```

elab.ml

@@ -125,7 +125,8 @@ and paths_row ta ps = function
 let rec_from_extyp typ label s =
   match s with
   | ExT([], t) ->
-    let rec find_rec = function
+    let rec find_rec t =
+      match follow_typ t with
       | 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
@@ -399,13 +400,18 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain
     IL.genE(erase_bind aks, IL.LamE(var.it, erase_typ t, e2))
 
   | EL.WrapE(var, typ) ->
+    let var_t = lookup_var env var in
     let s, zs1 =
       match elab_typ env typ "" with
       | ExT([], WrapT(s)), zs1 -> s, zs1
+      | ExT([], InferT(z)), zs1 ->
+        let s = ExT([], var_t) in
+        resolve_always z (WrapT(s));
+        s, zs1
       | _ -> error typ.at "non-wrapped type for wrap"
     in
     let _, zs2, f =
-      try sub_extyp env (ExT([], lookup_var env var)) s []
+      try sub_extyp env (ExT([], var_t)) s []
       with Sub e -> error exp.at
         ("wrapped type does not match annotation: " ^ Sub.string_of_error e)
     in
@@ -499,11 +505,18 @@ Trace.debug (lazy ("[AppE] ts = " ^ String.concat ", " (List.map string_of_norm_
     IL.AppE(IL.instE(ex1, List.map erase_typ ts), IL.AppE(f, IL.VarE(var2.it)))
 
   | EL.UnwrapE(var, typ) ->
+    let t1, zs1, ex = elab_instvar env var in
     let aks, t, s2, zs2 =
       match elab_typ env typ l with
       | ExT([], WrapT(ExT(aks, t) as s2)), zs2 -> aks, t, s2, zs2
+      | ExT([], InferT(z)), zs2 ->
+        (match t1 with
+         | WrapT(s2) ->
+           resolve_always z t1;
+           [], t1, s2, zs2
+         | _ ->
+           error typ.at "could not infer type for unwrap")
       | _ -> error typ.at "non-wrapped type for unwrap" in
-    let t1, zs1, ex = elab_instvar env var in
     let s1 =
       match t1 with
       | WrapT(s1) -> s1
@@ -519,9 +532,16 @@ Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2));
     IL.AppE(f, IL.DotE(ex, "wrap"))
 
   | 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 var_t = lookup_var env var in
+    let s, zs1 =
+      match elab_typ env typ l with
+      | ExT([], InferT(z)), zs1 ->
+        let s = ExT([], var_t) in
+        resolve_always z var_t;
+        s, zs1
+      | s, zs1 ->
+        s, zs1 in
+    let rec_t, unroll_t, roll_t, ak = rec_from_extyp typ "unrolling" s 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 ^ " "

paper.1ml

@@ -266,7 +266,7 @@ type OPT = {
 }
 Opt :> OPT = {
   type opt a = wrap (b : type) -> b -> (a ~> b) ~> b
-  none 'a :# opt a = fun (b : type) (n : b) (s : a ~> b) => n
-  some 'a x :# opt a = fun (b : type) (n : b) (s : a ~> b) => s x
+  none 'a :# _ = fun (b : type) (n : b) (s : a ~> b) => n
+  some 'a x :# _ = fun (b : type) (n : b) (s : a ~> b) => s x
   caseopt 'a 'b (xo :# opt a) = xo b
 }

prelude.1ml

@@ -112,8 +112,8 @@ type OPT = {
 }
 Opt :> OPT = {
   type opt a = wrap (b : type) -> (() ~> b) -> (a ~> b) ~> b
-  none 'a :# opt a = fun (b : type) (n : () ~> b) (s : a ~> b) => n ()
-  some 'a x :# opt a = fun (b : type) (n : () ~> b) (s : a ~> b) => s x
+  none 'a :# _ = fun (b : type) (n : () ~> b) (s : a ~> b) => n ()
+  some 'a x :# _ = fun (b : type) (n : () ~> b) (s : a ~> b) => s x
   caseopt (xo :# opt _) = xo _
 }
 ...Opt
@@ -129,9 +129,9 @@ type ALT = {
 }
 Alt :> ALT = {
   type alt a b = wrap (c : type) -> (a ~> c) -> (b ~> c) ~> c
-  left 'a 'b x :# alt a b =
+  left 'a 'b x :# _ =
     fun (c : type) (l : a ~> c) (r : b ~> c) => l x
-  right 'a 'b x :# alt a b =
+  right 'a 'b x :# _ =
     fun (c : type) (l : a ~> c) (r : b ~> c) => r x
   casealt (xy :# alt _ _) = xy _
 }
@@ -163,8 +163,8 @@ type LIST = {
 List :> LIST = {
   ...{
     type list a = wrap (b : type) -> b -> (a ~> b ~> b) ~> b
-    nil 'a :# list _ = fun (b : type) (n : b) (c : a ~> b ~> b) => n
-    cons x (xs :# list _) :# list _ =
+    nil 'a :# _ = fun (b : type) (n : b) (c : a ~> b ~> b) => n
+    cons x (xs :# list _) :# _ =
       fun (b : type) (n : b) (c : _ ~> b ~> b) =>
         c x (xs b n c)
     foldr (xs :# list _) = xs _

prelude/index.1ml

@@ -33,8 +33,8 @@ Alt :> {
   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
+  inl x :# _ = fun c => c.inl x
+  inr x :# _ = fun c => c.inr x
   case c (x :# t _ _) = x c
 }
 

readme.1ml

@@ -48,9 +48,9 @@ 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
-do Int.print n                         ;; or:
-do Int.print (single 7 @: stream).hd   ;; e @: t unrolls rec value directly
+({hd = n} :@ _) = single 5        ;; p :@ t pattern matches on rec value
+do Int.print n                    ;; or:
+do Int.print (single 7 @: _).hd   ;; e @: t unrolls rec value directly
 
 
 
@@ -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
+  none :# _ = fun (b : type) (n : b) (s : _ ~> b) => n
+  some x :# _ = fun (b : type) (n : b) (s : _ ~> b) => s x
   caseopt (xo :# opt _) = xo _
 }

regression.1ml

@@ -44,17 +44,14 @@ Equivalence: {
   to   'a 'b: t a b -> a ~> b
   from 'a 'b: t a b -> b ~> a
 } = {
-  type T a b = (type p _) ~> p a ~> p b
-  type t a b = wrap T a b
-  wr (eq: T _ _) :# t _ _ = eq
-  un (eq :# t _ _) = eq
-  transitivity 'a 'b 'c (ab: t a b) (bc: t b c) =
-    wr fun (type p _) => un bc p << un ab p
-  reflexivity = wr fun (type p _) => id
-  to eq a = un eq (type fun x => x) a
-  from 'a 'b (eq: t a b) b = un eq (type fun b => b ~> a) id b
-  symmetry 'a 'b (eq: t a b) : t b a =
-    wr fun (type p _) => un eq (type fun b => p b ~> p a) id
+  type t a b = wrap (type p _) ~> p a ~> p b
+  transitivity (ab:# t _ _) (bc:# t _ _) :# _ =
+    fun (type p _) => bc p << ab p
+  reflexivity:# _ = fun (type p _) => id
+  to (eq:# t _ _) a = eq (type fun x => x) a
+  from (eq:# t _ _) b = eq (type fun b => b ~> _) id b
+  symmetry (eq:# t _ _) :# _ =
+    fun (type p _) => eq (type fun b => p b ~> p _) id
 }
 
 ;;
@@ -173,6 +170,12 @@ Both = {
   ({x, y = _} as {x = _, y}) = {x = 1, y = 2}
 }
 
+type_error {
+  cannot_infer_unwrap t = t #: _
+}
+
+type_error {cannot_infer_unroll t = t @: _}
+
 ;;
 
 type_error { type_error 101 }
@@ -301,17 +304,13 @@ ListN = let
     nil     :               p N.Z
     (::) 'n : x ~> t x n ~> p (N.S n)
   }
-  type T x n (type t _ _) = (type p _) -> I x p t ~> p n
 in {
-  ...rec {type t _ _} => {type t x n = wrap T x n t}
+  ...rec {type t _ _} => {type t x n = wrap (type p _) -> I x p t ~> p n}
 
-  case 'x 'n (type p _) (cs: I x p t) (e :# wrap T x n t :@ t x n) =
-    e p cs
+  case (type p _) (cs: I _ p t) (e :# _ :@ t _ _) = e p cs
 
-  let mk 'x 'n (c: T x n t) = c :# wrap T x n t :@ t x n in {
-    nil  'x                     = mk fun (type p _) (r: I x p t) => r.nil
-    'x (v: x) :: 'n (vs: t x n) = mk fun (type p _) (r: I x p t) => r.:: v vs
-  }
+  nil     :# _ :@ t _ _ = fun (type p _) (r: I _ p t) => r.nil
+  v :: vs :# _ :@ t _ _ = fun (type p _) (r: I _ p t) => r.:: v vs
 } :> {
   type t _ _
 

russo.1ml

@@ -82,13 +82,13 @@ sift (S : STREAM) :> STREAM = {
 
 Sieve :> STREAM = {
   type state = wrap STREAM
-  start :# state = {
+  start :# _ = {
     type state = int
     start = 2
     next n = n + 1
     value s = s
   }
-  next (S :# state) :# state = sift S
+  next (S :# state) :# _ = sift S
   value (S :# state) = S.value S.start
 }
 

talk.1ml

@@ -116,7 +116,7 @@ newpoint = rec (newpoint : int -> int -> point) => fun x y :@ point => {
 }
 
 p = newpoint 3 4
-p' @: point = (p @: point).move 1 2
+p' @: _ = (p @: _).move 1 2
 do Int.print (p'.getX ())
 do print " "
 do Int.print (p'.getY ())

test.1ml

@@ -83,8 +83,8 @@ type OPT = {
 }
 Opt :> OPT = {
   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
+  none :# _ = fun (b : type) (n : b) (s : _ ~> b) => n
+  some x :# _ = fun (b : type) (n : b) (s : _ ~> b) => s x
   caseopt (xo :# opt _) = xo _
 }
 ...Opt
@@ -99,8 +99,8 @@ type ALT = {
 }
 Alt :> ALT = {
   type alt a b = wrap (c : type) -> (a ~> c) -> (b ~> c) ~> c
-  left x :# alt _ _ = fun (c : type) (l : _ ~> c) (r : _ ~> c) => l x
-  right x :# alt _ _ = fun (c : type) (l : _ ~> c) (r : _ ~> c) => r x
+  left x :# _ = fun (c : type) (l : _ ~> c) (r : _ ~> c) => l x
+  right x :# _ = fun (c : type) (l : _ ~> c) (r : _ ~> c) => r x
   casealt (xy :# alt _ _) = xy _
 }
 ...Alt
@@ -130,8 +130,8 @@ type LIST = {
 List :> LIST = {
   ...{
     type list a = wrap (b : type) -> b -> (a ~> b ~> b) ~> b
-    nil :# list _ = fun (b : type) (n : b) (c : _ ~> b ~> b) => n
-    cons x (xs :# list _) :# list _ =
+    nil :# _ = fun (b : type) (n : b) (c : _ ~> b ~> b) => n
+    cons x (xs :# list _) :# _ =
       fun (b : type) (n : b) (c : _ ~> b ~> b) =>
         c x (xs b n c)
     foldr (xs :# list _) = xs _
@@ -277,10 +277,10 @@ in {
 type int = primitive "int"
 type t = rec a => int
 v = 3 :@ t
-n = v @: t
-(m :@ t) = v
+n = v @: _
+(m :@ _) = v
 type u a = rec _ => a
 w = 4 :@ u int
-(x :@ u int) = w
-((x :@ t, y) :@ u (_, _)) = (6 :@ t, 7) :@ u (_, _)
-((x' :@ t, y') :@ u _) = (6 :@ t, 7) :@ u _
+(x :@ _) = w
+((x :@ _, y) :@ _) = (6 :@ t, 7) :@ u _
+((x' :@ _, y') :@ _) = (6 :@ t, 7) :@ u _