Change and generalize syntax of annotations, (un)wraps, (un)rolls

    exp  :  t     ;; annot
    exp  :> t     ;; seal
    exp  :@ t     ;; wrap
    exp  :# t     ;; roll
    exp @:  t     ;; unroll
    exp #:  t     ;; unwrap

    bind  :  t = exp   :=   bind = exp  :  t
    bind  :> t = exp   :=   bind = exp  :> t
    bind  :@ t = exp   :=   bind = exp  :@ t
    bind  :# t = exp   :=   bind = exp  :# t
    bind @:  t = exp   :=   bind = exp @:  t
    bind #:  t = exp   :=   bind = exp #:  t

    pat :  t      ;; annot pat
    pat :@ t      ;; roll pat -> binding unrolled
    pat :# t      ;; wrap pat -> binding unwrapped

Author: polytypic

README.md

@@ -115,11 +115,11 @@ E ::=
     fun '(X : T) => E       (implicit function/functor/constructor)
     E E                     (application)
     if E then E else E : T  (conditional)
-    wrap E : T              (impredicative wrapping)
-    unwrap E : T            (unwrapping)
+    E :# T                  (impredicative wrapping)
+    E #: T                  (unwrapping)
     rec (X : T) => E        (recursion)
-    @T E                    (recursive type roll)
-    E.@T                    (recursive type unroll)
+    E :@ T                  (recursive type roll)
+    E @: T                  (recursive type unroll)
     import "path"           (static import of module from file at path)
 
 (bindings)
@@ -192,7 +192,7 @@ E ::= ...
     E1 || E2                        ~> if E1 then true else E2
     E1 && E2                        ~> if E1 then E2 else false
     E : T                           ~> (fun (X : T) => X) E
-    E :> T                          ~> unwrap (wrap E : T) : T
+    E :> T                          ~> E :# T #: T
     let B in E                      ~> {B , X = E}.X
     rec P => E                      ~> rec (X : TP) => let P = X in E  [2]
     E1 ; E2                         ~> let _ = E1 in E2
@@ -209,8 +209,8 @@ P ::=
     (P1, ..., Pn)                   ~> {_1 = P1, ..., _n = Pn}
     (type X A1 ... An)              ~> (X : A1 -> ... -> An -> type)
     (type (A1 SYM A2) A3 ... An)    ~> (type (SYM) A1 ... An)
-    wrap P : T                      ~> ...let $ = unwrap $ : T in {P = $}
-    @T P                            ~> ...let $ = $.@T in {P = $}
+    P :# T                          ~> ...let $ = $ #: T in {P = $}
+    P :@ T                          ~> ...let $ = $ @: T in {P = $}
     P : T                           ~> P = $ : T
     P1 as P2                        ~> P1, P2
 
@@ -344,11 +344,11 @@ There are no datatype definitions, recursive types have to be defined
 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}   ;; @(t) e rolls value into t
-@stream{hd = n} = single 5             ;; @(t) p pattern matches on rec value
+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
+do Int.print (single 7 @: stream).hd   ;; e @: t unrolls rec value directly
 ```
 
 #### Recursive Functions
@@ -360,15 +360,15 @@ count = rec self => fun i =>
   if i == 0 then () else self (i - 1)
 
 repeat = rec self => fun x =>
-  @stream{hd = x, tl = fun () => some (self x)}
+  {hd = x, tl = fun () => some (self x)} :@ stream
 ```
 
 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,14 +392,13 @@ 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 = wrap (fun (b : type) (n : b) (s : _ ~> b) => n) : opt _
-  some x = wrap (fun (b : type) (n : b) (s : _ ~> b) => s x) : opt _
-  caseopt xo = (unwrap xo : opt _) _
+  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 _
 }
 ```
 
-Note how values of type `wrap T` have to be wrapped and unwrapped explicitly,
-with a type annotation.
+Note how values of type `wrap T` have to be wrapped and unwrapped explicitly.
 
 ---
 

lexer.mll

@@ -253,12 +253,14 @@ rule token = parse
   | "rec" { REC }
   | "then" { THEN }
   | "type" { TYPE }
-  | "unwrap" { UNWRAP }
   | "with" { WITH }
-  | "@" { AT }
   | "=" { EQUAL }
   | ":" { COLON }
   | ":>" { SEAL }
+  | ":@" { ROLL_OP }
+  | "@:" { UNROLL_OP }
+  | ":#" { WRAP_OP }
+  | "#:" { UNWRAP_OP }
   | "->" { ARROW }
   | "~>" { SARROW }
   | "=>" { DARROW }

paper.1ml

@@ -87,7 +87,7 @@ f (id : (a : type) -> a ~> a) = {x = id int 5, y = id bool true}
 
 type SHAPE = {type t, area : t ~> int, v : t}
 volume (height : int) (s : SHAPE) = height * s.area s.v
-area ss = List.foldl ss 0 (fun a (wrap s : wrap SHAPE) => a + s.area s.v)
+area ss = List.foldl ss 0 (fun a (s :# wrap SHAPE) => a + s.area s.v)
 
 type COLL c = {
   type key
@@ -266,7 +266,7 @@ type OPT = {
 }
 Opt :> OPT = {
   type opt a = wrap (b : type) -> b -> (a ~> b) ~> b
-  none 'a = wrap (fun (b : type) (n : b) (s : a ~> b) => n) : opt a
-  some 'a x = wrap (fun (b : type) (n : b) (s : a ~> b) => s x) : opt a
-  caseopt 'a 'b xo = (unwrap xo : opt a) 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
+  caseopt 'a 'b (xo :# opt a) = xo b
 }

parser.mly

@@ -26,17 +26,19 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %}
 
 %token HOLE PRIMITIVE
-%token FUN REC LET IN DO WRAP UNWRAP TYPE ELLIPSIS
+%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 LPAR RPAR
 %token LBRACE RBRACE
-%token DOT AT TICK
+%token DOT TICK
 %token COMMA SEMI
 %token TYPE_ERROR
 %token LOCAL
 %token IMPORT
+%token WRAP_OP UNWRAP_OP
+%token ROLL_OP UNROLL_OP
 
 %token EOF
 
@@ -262,10 +264,6 @@ dotpathexp :
     { $1 }
   | dotpathexp DOT label
     { DotE($1, $3)@@at() }
-  | dotpathexp DOT AT attyp
-    { unrollE($1, $4)@@at() }
-  | dotpathexp DOT AT name
-    { unrollE($1, PathT(VarE($4)@@ati 4)@@ati 4)@@at() }
 ;
 atpathexp :
   | name
@@ -280,10 +278,6 @@ apppathexp :
     { appE($1, $2)@@at() }
   | apppathexp attyp
     { appE($1, TypE($2)@@ati 2)@@at() }
-  | AT attyp atexp
-    { rollE($3, $2)@@at() }
-  | AT name atexp
-    { rollE($3, PathT(VarE($2)@@ati 2)@@ati 2)@@at() }
 ;
 infpathexp :
   | apppathexp
@@ -303,10 +297,6 @@ dotexp :
     { $1 }
   | dotexp DOT label
     { DotE($1, $3)@@at() }
-  | dotexp DOT AT attyp
-    { unrollE($1, $4)@@at() }
-  | dotexp DOT AT name
-    { unrollE($1, PathT(VarE($4)@@ati 4)@@ati 4)@@at() }
 ;
 atexp :
   | name
@@ -339,10 +329,6 @@ appexp :
     { $1 }
   | appexp dotexp
     { appE($1, $2)@@at() }
-  | AT attyp atexp
-    { rollE($3, $2)@@at() }
-  | AT name atexp
-    { rollE($3, PathT(VarE($2)@@ati 2)@@ati 2)@@at() }
 ;
 infexp :
   | appexp
@@ -356,17 +342,27 @@ infexp :
   | infexp LOGICAL_AND appexp
     { andE($1, $3)@@at() }
 ;
+annexp_op :
+  | COLON
+    { annotE }
+  | SEAL
+    { sealE }
+  | ROLL_OP
+    { rollE }
+  | UNROLL_OP
+    { unrollE }
+  | WRAP_OP
+    { wrapE }
+  | UNWRAP_OP
+    { unwrapE }
+;
 annexp :
-  | infexp optannot
-    { opt annotE($1, $2)@@at() }
+  | infexp
+    { $1 }
   | TYPE typ
     { TypE($2)@@at() }
-  | annexp SEAL typ
-    { sealE($1, $3)@@at() }
-  | WRAP infexp COLON typ
-    { wrapE($2, $4)@@at() }
-  | UNWRAP infexp COLON typ
-    { unwrapE($2, $4)@@at() }
+  | annexp annexp_op typ
+    { $2($1, $3)@@at() }
 ;
 inexp :
   | annexp
@@ -403,18 +399,42 @@ funbind :
     { ($3, $2 @ $4 @ $6) }
 ;
 
+bindann_op :
+  | COLON
+    { annotE }
+  | SEAL
+    { sealE }
+  | ROLL_OP
+    { rollE }
+  | UNROLL_OP
+    { unrollE }
+  | WRAP_OP
+    { wrapE }
+  | UNWRAP_OP
+    { unwrapE }
+;
+bindann :
+  | bindann_op typ
+    { fun e -> $1(e, $2)@@span[ati 2; e.at] }
+;
+bindanns :
+  | bindann
+    { $1 }
+  | bindanns bindann
+    { fun e -> $2 ($1 e) }
+;
+bindanns_opt :
+  |
+    { fun e -> e }
+  | bindanns
+    { $1 }
+;
+
 atbind :
-  | funbind optannot EQUAL exp
-    { let (head, params) = $1 in
-      VarB(head, funE(params,
-        opt annotE($4, $2)@@span[ati 2; ati 4])@@at())@@at() }
-  | funbind SEAL typ EQUAL exp
-    { let (head, params) = $1 in
-      VarB(head, funE(params, sealE($5, $3)@@span[ati 3; ati 5])@@at())@@at() }
-  | head SEAL typ EQUAL exp
-    { VarB($1, sealE($5, $3)@@span[ati 3; ati 5])@@at() }
-  | pat EQUAL exp
-    { patB($1, $3)@@at() }
+  | funbind bindanns_opt EQUAL exp
+    { let (head, params) = $1 in VarB(head, funE(params, $2($4))@@at())@@at() }
+  | atpat bindanns_opt EQUAL exp
+    { patB($1, $2($4))@@at() }
   | name
     { VarB($1, VarE($1.it@@at())@@at())@@at() }
   | typpat EQUAL typ
@@ -461,19 +481,19 @@ atpat :
       annotP(headP(head)@@head.at,
         funT(typparams, TypT@@at(), Pure@@at())@@at())@@at() }
 ;
-apppat :
-  | atpat
-    { $1 }
-  | AT attyp atpat
-    { rollP($3, $2)@@at() }
-  | AT name atpat
-    { rollP($3, PathT(VarE($2)@@ati 2)@@ati 2)@@at() }
+annpat_op :
+  | COLON
+    { annotP }
+  | ROLL_OP
+    { rollP }
+  | WRAP_OP
+    { wrapP }
 ;
 annpat :
-  | apppat optannot
-    { opt annotP($1, $2)@@at() }
-  | WRAP apppat COLON typ
-    { wrapP($2, $4)@@at() }
+  | atpat
+    { $1 }
+  | annpat annpat_op typ
+    { $2($1, $3)@@at() }
 ;
 pat :
   | annpat

prelude.1ml

@@ -112,9 +112,9 @@ type OPT = {
 }
 Opt :> OPT = {
   type opt a = wrap (b : type) -> (() ~> b) -> (a ~> b) ~> b
-  none 'a = wrap (fun (b : type) (n : () ~> b) (s : a ~> b) => n ()) : opt a
-  some 'a x = wrap (fun (b : type) (n : () ~> b) (s : a ~> b) => s x) : opt a
-  caseopt xo = (unwrap xo : opt _) _
+  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
+  caseopt (xo :# opt _) = xo _
 }
 ...Opt
 
@@ -129,11 +129,11 @@ type ALT = {
 }
 Alt :> ALT = {
   type alt a b = wrap (c : type) -> (a ~> c) -> (b ~> c) ~> c
-  left 'a 'b x =
-    wrap (fun (c : type) (l : a ~> c) (r : b ~> c) => l x) : alt a b
-  right 'a 'b x =
-    wrap (fun (c : type) (l : a ~> c) (r : b ~> c) => r x) : alt a b
-  casealt xy = (unwrap xy : alt _ _) _
+  left 'a 'b x :# alt a b =
+    fun (c : type) (l : a ~> c) (r : b ~> c) => l x
+  right 'a 'b x :# alt a b =
+    fun (c : type) (l : a ~> c) (r : b ~> c) => r x
+  casealt (xy :# alt _ _) = xy _
 }
 ...Alt
 
@@ -163,11 +163,11 @@ type LIST = {
 List :> LIST = {
   ...{
     type list a = wrap (b : type) -> b -> (a ~> b ~> b) ~> b
-    nil 'a = wrap (fun (b : type) (n : b) (c : a ~> b ~> b) => n) : list _
-    cons x xs =
-      wrap (fun (b : type) (n : b) (c : _ ~> b ~> b) =>
-        c x ((unwrap xs : list _) b n c)) : list _
-    foldr xs = (unwrap xs : list _) _
+    nil 'a :# list _ = fun (b : type) (n : b) (c : a ~> b ~> b) => n
+    cons x (xs :# list _) :# list _ =
+      fun (b : type) (n : b) (c : _ ~> b ~> b) =>
+        c x (xs b n c)
+    foldr (xs :# list _) = xs _
   } :> LIST_CORE
   isNil xs = foldr xs true (fun _ _ => false)
   head xs = foldr xs none (fun x _ => some x)

prelude/index.1ml

@@ -33,9 +33,9 @@ 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 = wrap (fun c => c.inl x): t _ _
-  inr x = wrap (fun c => c.inr x): t _ _
-  case c (wrap x: t _ _) = x c
+  inl x :# t _ _ = fun c => c.inl x
+  inr x :# t _ _ = fun c => c.inr x
+  case c (x :# t _ _) = x c
 }
 
 Alt = {
@@ -69,9 +69,9 @@ 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, (::)} (@(t _) x) = x |> Opt.case {
+  nil :@ t _ = none
+  hd :: tl :@ t _ = some (hd, tl)
+  case {nil, (::)} (x :@ t _) = x |> Opt.case {
     none = nil
     some (hd, tl) = hd :: tl
   }