Skip to content

Commit

Permalink
Change to infer (un)roll, (un)wrap, and un(roll|wrap) in elim forms
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
polytypic committed Jul 26, 2020
1 parent fcaa0d5 commit e3b14bd
Show file tree
Hide file tree
Showing 17 changed files with 190 additions and 126 deletions.
26 changes: 14 additions & 12 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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))}
}
```

Expand All @@ -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.

---

Expand Down
68 changes: 42 additions & 26 deletions elab.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down Expand Up @@ -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 ->
Expand All @@ -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) -> ()
Expand All @@ -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, []
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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)))

Expand Down Expand Up @@ -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 *)
Expand Down
13 changes: 5 additions & 8 deletions examples/fc.1ml
Original file line number Diff line number Diff line change
Expand Up @@ -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) =>
Expand Down
5 changes: 2 additions & 3 deletions examples/hoas.1ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
13 changes: 5 additions & 8 deletions examples/trie.1ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
23 changes: 10 additions & 13 deletions import.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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
Expand All @@ -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))
4 changes: 4 additions & 0 deletions lib.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
1 change: 1 addition & 0 deletions lib.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
15 changes: 7 additions & 8 deletions prelude/index.1ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {
Expand All @@ -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
}
Expand Down
20 changes: 10 additions & 10 deletions readme.1ml
Original file line number Diff line number Diff line change
Expand Up @@ -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))}
}


Expand All @@ -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 _
}
Loading

0 comments on commit e3b14bd

Please sign in to comment.