% lambda-circle-1 with shift/reset % Two-level stage calculus with delimited control: % the calculus \Meta in our paper. % The calculus is designed so that we could write Gibonacci, % staged Gibonacci, and let-insertion. % We use the intrinsic encoding of \Meta in LF. The code in this file is % the extension of % Mechanized proofs of type soundness of delimited control % http://okmij.org/ftp/formalizations/index.html#shift % to staging. For simplicity, we don't consider the answer-type modification % however. % Unlike the earlier version of the calculus in circle-shift.elf, % we no longer distinguish between `pure' and `impure' computations % and types. Therefore, the answer-type is always present. % Sometimes, we may have to insert `reset' to emulate % the answer-type polymorphism. % Notational conventions: % we use suffix 0 to indicate the present stage; and suffix + % for the future stage. For very popular terms and term constructors % such as l (lambda), ? (reset) and @ (application), we drop the suffix 0. % So l means a present-stage lambda and l+ means a future-stage % lambda. Some term constructors like cons are level-polymorphic; % (cons e1 e2) may refer to either present or future computation, depending % on the context. % Primitive types: one so far, integer. % A term N of type nat is a nonnegative integer. % Constructors: 0, 1. nat: type. %name nat N. 0: nat. 1: nat -> nat. %prefix 200 1. % implementation of the addition of two naturals plus : nat -> nat -> nat -> type. %mode plus +N1 +N2 -N3. -: plus 0 N N. -: plus (1 N1) N2 (1 N3) <- plus N1 N2 N3. %worlds () (plus _ _ _). %total {N} (plus N _ _). %unique (plus +N1 +N2 -N3). % predecessor % We make the predecessor total by setting pred 0 to 0 pred : nat -> nat -> type. %mode pred +N1 -N2. -: pred 0 0. -: pred (1 N) N. %worlds () (pred _ _). %total {} (pred _ _). %unique (pred +N1 -N2). % Types % The following is a faithful transcription of the figure % ``Type system of \Meta'' in our paper. tp: type. %name tp T. int: tp. % one single primitive type for now. % the arrow type: arr t1 t2 t3 is written t1 -> t2/t3 in the paper. % t3 is the answer-type of the body of the function. arr: tp -> tp -> tp -> tp. % product type *: tp -> tp -> tp. %infix none 225 *. % code type. Ta is the answer-type & : tp -> tp -> tp. % Expressions % Expressions are tagged with the stage level: present stage or future % stage. % We use the intrinsic encoding of the \Meta language in LF, and so % our expressions are typed and bear the explicit type. % Since all expressions are potentially effectful, they are % marked with an answer-type, usually denoted Ta or Ua. % Furthermore, future-stage expressions have two answer-types, one for each % stage. Therefore, we distinguish present vs. future stage expressions % by the number of answer-types, one or two. We do not need any further % stage level annotations. % The definitions below specify not only the syntax of the language, % but also its type system. Type inference is syntax-directed, and % it is indeed tied to syntax. Type judgements are literally specified % alongside the syntax. % fix is an applicative fixpoint combinator, defined as a _polymorphic_ % constant, with the type forall TV. (TV -> TV) -> TV. % Here TV is generally a an arrow type. % The decrement is not in the paper (and is generally expressible via addition) % but we add it anyway. It is convenient, letting us avoid introducing % negative numbers. % Answer type or types; their number indicates the staging level atp: type. %name atp A. at0: tp -> atp. % present stage %prefix 170 at0. at1: tp -> tp -> atp. % future stage exp: tp -> atp -> type. %name exp E. value: exp T A -> type. %name value V. n : nat -> exp int A. %prefix 170 n. % Integer literal + : exp int A -> exp int A -> exp int A. %infix left 100 +. dec: exp int A -> exp int A. % Decrement % Types for bound variables % Variables represent values, in CBV, and hence are % answer-type polymorphic. arg0 and arg+ let us abstract away % the answer type. arg0: tp -> type. arg0-: value (_:exp T (at0 _)) -> arg0 T. arg+: tp -> type. % We do not have any constructors for arg+. % Since our calculus does not have the `run' form to run the % constructed code, future-stage variables are indeed never substituted % for and we don't need any data constructors for arg+. % We do use arg+ hypothetically, in the lambda form l+ and hence % in type-checking. % present-stage lambda l : (arg0 T1 -> exp T2 (at0 T2a)) -> exp (arr T1 T2 T2a) (at0 _). % future-stage lambda. The present-stage answer-type polymorphism % betrays an explicit reset l+ : (arg+ U1 -> exp U2 (at1 (& U2 U2a) U2a)) -> exp (arr U1 U2 U2a) (at1 _ _). % Variable rules: Implicit answer-type polymorphism v : arg0 T -> exp T (at0 _). %prefix 170 v. v+ : arg+ T -> exp T (at1 _ _). %prefix 170 v+. % fix: the polymorphic constant fix: exp (arr (arr (arr T T1 T2) (arr T T1 T2) T2) (arr T T1 T2) _) A. % present-stage application @ : exp (arr T1 T2 Ta) (at0 Ta) -> exp T1 (at0 Ta) -> exp T2 (at0 Ta). %infix left 154 @. % future-stage application @+ : exp (arr T1 T2 Ua) (at1 Ta Ua) -> exp T1 (at1 Ta Ua) -> exp T2 (at1 Ta Ua). %infix left 154 @+. cons: exp T1 A -> exp T2 A -> exp (T1 * T2) A. % standard pair stuff fst : exp (arr (T1 * T2) T1 Ta) A. % constants snd : exp (arr (T1 * T2) T2 Ta) A. % constants ifz: exp int A -> exp T1 A -> exp T1 A -> exp T1 A. % if zero % Delimited control % deru is used in the bubble-up semantics, internally % The user normally uses 'de' defined below % The typing rule is more general than common because deru % describes the current `bubble'. % Deru exists only at the present-stage, the stage at which % evaluation is happening. % Note that Ta1 is arbitrary: the continuation captured by % shift is a pure function. deru : (arg0 T -> exp TW (at0 Ta)) -> % continuation being captured. exp (arr (arr T Ta Ta1) Ta Ta) (at0 Ta) -> exp TW (at0 Ta). % In the user code, shift is a polymorphic constant de : exp (arr (arr (arr T Ta Ta1) Ta Ta) T Ta) A. ? : exp T (at0 T) -> exp T (at0 _). %prefix 150 ?. % reset ?+ : exp U (at1 Ta U) -> exp U (at1 Ta _). %prefix 150 ?+. % reset % Staging constructs: brackets and escape ^ : exp U1 (at1 Ta Ua) -> exp (& U1 Ua) (at0 Ta). %prefix 170 ^. % aka next ~ : exp (& U1 Ua) (at0 Ta) -> exp U1 (at1 Ta Ua). %prefix 150 ~. % aka prev % Abbreviations n0 = n 0. n1 = n 1 0. n2 = n 1 1 0. n3 = n 1 1 1 0. n4 = n 1 1 1 1 0. n5 = n 1 1 1 1 1 0. n6 = n 1 1 1 1 1 1 0. n7 = n 1 1 1 1 1 1 1 0. n8 = n 1 1 1 1 1 1 1 1 0. % ======================================================================== % examples % dec x + 1> tt1 = (^ (l+ [x] dec (v+ x) + n1)). % Various fragments of Gibonacci, to test typing tt20 : exp (arr (arr int int T1) (arr int int T1) T2) (at0 T3) = (l [self] l [k] (v self @ (dec (dec (v k))) + v self @ (dec (v k)))). tt2 : exp (arr int int T1) (at0 T2) = (fix @ l [self] l [k] (v self @ (dec (dec (v k))) + v self @ (dec (v k)))). tt2+ : exp (arr int (& int T1) T2) (at0 T3) = (fix @ l [self] l [k] ^ ((~ (v self @ dec (dec (v k)))) + ~ (v self @ dec (v k)))). tt3 : exp (arr int (arr int (arr int int T1) T2) T3) (at0 T4) = l [x] l [y] fix @ l [self] l [k] ifz (v k) (v x) (ifz (dec (v k)) (v y) n0). % The Gibonacci function gib = l [x] l [y] fix @ l [self] l [k] (ifz (v k) (v x) (ifz (dec (v k)) (v y) (v self @ dec (dec (v k)) + v self @ dec (v k)))). % Staged Gibonacci gibs = l [x] l [y] fix @ l [self] l [k] (ifz (v k) (v x) (ifz (dec (v k)) (v y) (^ (~ (v self @ dec (dec (v k))) + ~ (v self @ dec (v k)))))). % The inferred type: % gibs : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} {T5:tp} % exp (arr (& int T1) (arr (& int T1) (arr int (& int T1) T2) T3) T4) % (at0 T5) gibs3 : exp (& (arr int (arr int int T1) T2) T3) (at0 T4) = ^ (l+ [x] l+ [y] ~ (gibs @ ^ (v+ x) @ ^ (v+ y) @ n3)). % ======================================================================== % Dynamic Semantics % ---------------------------------------------------------------------- % Some expressions are classified as values. See the figure % ``Values and contexts'' of the paper. The valuehood depends on the % stage. % value: exp T A -> type. %name value V. %mode value +E. %block bl-ev : some {T:tp} block {e:arg+ T}. val-n: value (n _). % Literals are values at any level val-f: value fix. % A constant: trivially a value val-r: value de. % A constant: trivially a value val-F: value fst. % A constant: trivially a value val-S: value snd. % A constant: trivially a value % values at the empty level val-l0: value (l _). val-c: value (cons E1 E2) % A pair of values is a value, at <- value E2 % every level. <- value E1. % Homomorphisms at any level val-^: value (^ E) <- value E. val-V+: value (v+ _). % Future variable references aren't % evaluated at the present stage % Values at the non-empty level: basically, the absence of 0-level escapes % homomorphisms... val-l+: value (l+ E) <- {x:arg+ T1} value (E x). val-@+: value (E1 @+ E2) <- value E2 <- value E1. val-++: value ((E1 + E2) : exp _ (at1 _ _)) <- value E2 <- value E1. val-d+: value ((dec E) : exp _ (at1 _ _)) <- value E. val-i+: value ((ifz E1 E2 E3) : exp _ (at1 _ _)) <- value E3 <- value E2 <- value E1. val-?+: value (?+ E) <- value E. %worlds (bl-ev) (value _). %terminates {E} (value E). % Since values aren't further evaluated, they can't cause any effect % and so are (present-stage) answer-type polymorphic. % In other words, we can change the present-stage answer-type % to some other one. The following function does the conversion, % witnessing the answer-type polymorphism. val-new-at+: value (_:exp T (at1 Ta Ua)) -> {TaN:tp} exp T (at1 TaN Ua) -> type. %mode val-new-at+ +V +T -E. -: val-new-at+ (val-n: value (n N)) _ (n N). -: val-new-at+ val-f _ fix. -: val-new-at+ val-r _ de. -: val-new-at+ val-F _ fst. -: val-new-at+ val-S _ snd. -: val-new-at+ (val-V+ : value (v+ V)) _ (v+ V). -: val-new-at+ (val-c VE1 VE2) TaN (cons E1 E2) <- val-new-at+ VE1 TaN E1 <- val-new-at+ VE2 TaN E2. -: val-new-at+ ((val-l+ _): value (l+ E)) TaN (l+ E). -: val-new-at+ (val-@+ VE1 VE2) TaN (E1 @+ E2) <- val-new-at+ VE1 TaN E1 <- val-new-at+ VE2 TaN E2. -: val-new-at+ (val-d+ VE) TaN (dec E) <- val-new-at+ VE TaN E. -: val-new-at+ (val-++ VE1 VE2) TaN (E1 + E2) <- val-new-at+ VE1 TaN E1 <- val-new-at+ VE2 TaN E2. -: val-new-at+ (val-i+ VE1 VE2 VE3) TaN (ifz E1 E2 E3) <- val-new-at+ VE1 TaN E1 <- val-new-at+ VE2 TaN E2 <- val-new-at+ VE3 TaN E3. -: val-new-at+ (val-?+ VE) TaN (?+ E) <- val-new-at+ VE TaN E. %worlds (bl-ev) (val-new-at+ _ _ _). %total {V} (val-new-at+ V _ _). %unique (val-new-at+ +V +T -E). val-new-at: value (_:exp T (at0 Ta)) -> {TaN:tp} exp T (at0 TaN) -> type. %mode val-new-at +V +T -E. -: val-new-at (val-n: value (n N)) _ (n N). -: val-new-at val-f _ fix. -: val-new-at val-r _ de. -: val-new-at val-F _ fst. -: val-new-at val-S _ snd. -: val-new-at (val-l0 : value (l E)) _ (l E). -: val-new-at (val-c VE1 VE2) TaN (cons E1 E2) <- val-new-at VE1 TaN E1 <- val-new-at VE2 TaN E2. -: val-new-at (val-^ VE) TaN (^ E) <- val-new-at+ VE TaN E. %worlds (bl-ev) (val-new-at _ _ _). %total {V} (val-new-at V _ _). %unique (val-new-at +V +T -E). % ---------------------------------------------------------------------- % Some expressions are classified as non-values. The present-stage % deru (the continuation bubble) is neither a value nor a non-value. % Naming conventions for the rules in the code below: % suffix: C is for congruence rule % R for bubble propagating through the present-stage code % S for bubble propagating through the future-stage code non-value: exp T A -> type. %name non-value R. %mode non-value +E. nv-d: non-value ((dec E): exp _ (at0 _)) <- value E. nv-dC: non-value (dec E) <- non-value E. nv-dR: non-value (dec (deru C E)). nv-dS: non-value (dec ~ (deru C E)). nv-+: non-value ((E1 + E2): exp _ (at0 _)) <- value E2 <- value E1. nv-+C1: non-value (E1 + E2) <- non-value E1. nv-+C2: non-value (E1 + E2) <- non-value E2 <- value E1. nv-+R1: non-value ((deru C1 E1) + E2). nv-+R2: non-value (E1 + (deru C2 E2)) <- value E1. nv-+S1: non-value (~ (deru C1 E1) + E2). nv-+S2: non-value (E1 + ~ (deru C2 E2)). % This is the last clause: no need % to ensure that E1 is a value % because the cases of E1 being % a value or deru have been covered % already. % nv-+S2: non-value (E1 + ~ (deru C2 E2)) % This clause is better (non- % <- value E1. % overlapping), but slower. nv-V: non-value (v _). nv-cC1: non-value (cons E1 E2) <- non-value E1. nv-cC2: non-value (cons E1 E2) <- non-value E2 <- value E1. nv-cR1: non-value (cons (deru C1 E1) E2). nv-cR2: non-value (cons E1 (deru C2 E2)) <- value E1. nv-cS1: non-value (cons (~ (deru C1 E1)) E2). nv-cS2: non-value (cons E1 (~ (deru C2 E2))) <- value E1. nv-i: non-value ((ifz E E1 E2): exp _ (at0 _)) <- value E. nv-iC: non-value (ifz E E1 E2) <- non-value E. nv-iC1: non-value ((ifz E E1 E2): exp _ (at1 _ _)) <- non-value E1 <- value E. nv-iC2: non-value ((ifz E E1 E2): exp _ (at1 _ _)) <- non-value E2 <- value E1 <- value E. nv-iR: non-value (ifz (deru C E) E1 E2). nv-iS: non-value (ifz (~ (deru C E)) E1 E2). nv-iS1: non-value (ifz E (~ (deru C1 E1)) E2) <- value E. nv-iS2: non-value (ifz E E1 (~ (deru C2 E2))) <- value E1 <- value E. nv-@: non-value (E1 @ E2) <- value E2 <- value E1. nv-@C1: non-value (E1 @ E2) <- non-value E1. nv-@C2: non-value (E1 @ E2) <- non-value E2 <- value E1. nv-@R1: non-value ((deru C1 E1) @ E2). nv-@R2: non-value (E1 @ (deru C2 E2)) <- value E1. nv-?: non-value ((? E): exp _ (at0 _)) <- value E. nv-?C: non-value (? E) <- non-value E. nv-?R: non-value (? (deru C E)). nv-~: non-value (~ E) <- value E. nv-~C: non-value (~ E) <- non-value E. nv-^C: non-value (^ E) <- non-value E. nv-^S: non-value (^ ~ (deru C E)). nv-?+C: non-value (?+ E) <- non-value E. nv-?+S: non-value (?+ ~ (deru C E)). nv-l+C: non-value (l+ E) <- {x:arg+ T} non-value (E x). nv-l+S: non-value (l+ [x] ~ (deru ([x1:arg0 TC] _) ((EB x): exp (arr (arr TC _ T6) _ _) _))). % Inferred type: % nv-l+S : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} {T5:tp} {TC:tp} {T6:tp} % {E1:arg+ T1 -> arg0 TC -> exp (& T2 T3) (at0 & T2 T3)} % {EB:arg+ T1 % -> exp (arr (arr TC (& T2 T3) T6) (& T2 T3) (& T2 T3)) % (at0 & T2 T3)} % non-value (l+ ([x:arg+ T1] ~ deru ([x1:arg0 TC] E1 x x1) (EB x))). % E1 and E2 depend on x! That's important for the coverage of vclassify nv-@+C1: non-value (E1 @+ E2) <- non-value E1. nv-@+C2: non-value (E1 @+ E2) <- non-value E2 <- value E1. nv-@+S1: non-value ((~ (deru C1 E1)) @+ E2). nv-@+S2: non-value (E1 @+ (~ (deru C2 E2))) <- value E1. %worlds (bl-ev) (non-value _). %terminates {E} (non-value E). % ---------------------------------------------------------------------- % The following constructively proves that each expression is % either a value, deru, or non-value. % The following is purely automatic, and auxiliary % relations vclassify-@ and vclassify-z are defined only because % Twelf's output coverage checker can't deal with pattern-matching % on output arguments . vhood: exp T A -> type. a-value : vhood E <- value E. a-deru0 : vhood (deru _ _). a-deru+ : vhood (~ (deru _ _)). a-non-value : vhood E <- non-value E. vclassify: {E:exp T A} vhood E -> type. %mode vclassify +E -P. -: vclassify _ a-deru0. -: vclassify _ (a-value val-n). % Classify the constants -: vclassify _ (a-value val-f). -: vclassify _ (a-value val-r). -: vclassify _ (a-value val-F). -: vclassify _ (a-value val-S). -: vclassify _ (a-value val-l0). -: vclassify _ (a-non-value nv-V). -: vclassify _ (a-value val-V+). vclassify-dec: vhood E -> vhood (dec E) -> type. %mode vclassify-dec +VE1 -VE. -: vclassify-dec (a-value V) (a-value (val-d+ V)). -: vclassify-dec (a-value V) (a-non-value (nv-d V)). -: vclassify-dec (a-non-value NV) (a-non-value (nv-dC NV)). -: vclassify-dec a-deru0 (a-non-value nv-dR). -: vclassify-dec a-deru+ (a-non-value nv-dS). %worlds (bl-ev) (vclassify-dec _ _). %total {} (vclassify-dec _ _). %unique (vclassify-dec +VE1 -VE). -: vclassify (dec E) VH <- vclassify E VE <- vclassify-dec VE VH. vclassify-?: vhood E -> {Ta:tp} non-value ((? E): exp _ (at0 Ta)) -> type. %mode vclassify-? +VE1 +Ta -VE. -: vclassify-? (a-value V) _ (nv-? V). -: vclassify-? (a-non-value NV) _ (nv-?C NV). -: vclassify-? a-deru0 _ nv-?R. %worlds (bl-ev) (vclassify-? _ _ _). %total {} (vclassify-? _ _ _). %unique (vclassify-? +VE1 +Ta -VE). -: vclassify ((? E): exp _ (at0 Ta)) (a-non-value NV) <- vclassify E VE <- vclassify-? VE Ta NV. vclassify-?+: vhood E -> {Ua:tp} vhood ((?+ E): exp _ (at1 _ Ua)) -> type. %mode vclassify-?+ +VE1 +Ua -VE. -: vclassify-?+ (a-value V) _ (a-value (val-?+ V)). -: vclassify-?+ (a-non-value NV) _ (a-non-value (nv-?+C NV)). -: vclassify-?+ a-deru+ _ (a-non-value nv-?+S). %worlds (bl-ev) (vclassify-?+ _ _ _). %total {} (vclassify-?+ _ _ _). %unique (vclassify-?+ +VE1 +Ua -VE). -: vclassify (?+ E) VH <- vclassify E VE <- vclassify-?+ VE _ VH. vclassify-@0: vhood E1 -> vhood E2 -> non-value (E1 @ E2) -> type. %mode vclassify-@0 +VE1 +VE2 -VE. -: vclassify-@0 (a-value V1) (a-value V2) (nv-@ V1 V2). -: vclassify-@0 a-deru0 _ nv-@R1. -: vclassify-@0 (a-value V1) a-deru0 (nv-@R2 V1). -: vclassify-@0 (a-non-value NV1) _ (nv-@C1 NV1). -: vclassify-@0 (a-value V1) (a-non-value NV2) (nv-@C2 V1 NV2). %worlds (bl-ev) (vclassify-@0 _ _ _). %total {} (vclassify-@0 _ _ _). %unique (vclassify-@0 +VE1 +VE2 -VE). -: vclassify (E1 @ E2) (a-non-value NV) <- vclassify E1 VE1 <- vclassify E2 VE2 <- vclassify-@0 VE1 VE2 NV. vclassify-@+: vhood E1 -> vhood E2 -> vhood (E1 @+ E2) -> type. %mode vclassify-@+ +VE1 +VE2 -VE. -: vclassify-@+ (a-non-value NV1) _ (a-non-value (nv-@+C1 NV1)). -: vclassify-@+ (a-value V1) (a-non-value NV2) (a-non-value (nv-@+C2 V1 NV2)). -: vclassify-@+ (a-value V1) (a-value V2) (a-value (val-@+ V1 V2)). -: vclassify-@+ a-deru+ _ (a-non-value nv-@+S1). -: vclassify-@+ (a-value V1) a-deru+ (a-non-value (nv-@+S2 V1)). %worlds (bl-ev) (vclassify-@+ _ _ _). %total {} (vclassify-@+ _ _ _). %unique (vclassify-@+ +VE1 +VE2 -VE). -: vclassify (E1 @+ E2) VH <- vclassify E1 VE1 <- vclassify E2 VE2 <- vclassify-@+ VE1 VE2 VH. vclassify-+: vhood E1 -> vhood E2 -> vhood (E1 + E2) -> type. %mode vclassify-+ +VE1 +VE2 -VE. -: vclassify-+ (a-value V1) (a-value V2) (a-non-value (nv-+ V1 V2)). -: vclassify-+ a-deru0 _ (a-non-value nv-+R1). -: vclassify-+ (a-value V1) a-deru0 (a-non-value (nv-+R2 V1)). -: vclassify-+ (a-non-value NV1) _ (a-non-value (nv-+C1 NV1)). -: vclassify-+ (a-value V1) (a-non-value NV2) (a-non-value (nv-+C2 V1 NV2)). -: vclassify-+ (a-value V1) (a-value V2) (a-value (val-++ V1 V2)). -: vclassify-+ a-deru+ _ (a-non-value nv-+S1). -: vclassify-+ (a-value V1) a-deru+ (a-non-value nv-+S2). %worlds (bl-ev) (vclassify-+ _ _ _). %total {} (vclassify-+ _ _ _). %unique (vclassify-+ +VE1 +VE2 -VE). -: vclassify (E1 + E2) VH <- vclassify E1 VE1 <- vclassify E2 VE2 <- vclassify-+ VE1 VE2 VH. vclassify-c: vhood E1 -> vhood E2 -> vhood (cons E1 E2) -> type. %mode vclassify-c +VE1 +VE2 -VE. -: vclassify-c (a-value V1) (a-value V2) (a-value (val-c V1 V2)). -: vclassify-c a-deru0 _ (a-non-value nv-cR1). -: vclassify-c (a-value V1) a-deru0 (a-non-value (nv-cR2 V1)). -: vclassify-c (a-non-value NV1) _ (a-non-value (nv-cC1 NV1)). -: vclassify-c (a-value V1) (a-non-value NV2) (a-non-value (nv-cC2 V1 NV2)). -: vclassify-c a-deru+ _ (a-non-value nv-cS1). -: vclassify-c (a-value V1) a-deru+ (a-non-value (nv-cS2 V1)). %worlds (bl-ev) (vclassify-c _ _ _). %total {} (vclassify-c _ _ _). %unique (vclassify-c +VE1 +VE2 -VE). -: vclassify (cons E1 E2) VH <- vclassify E1 VE1 <- vclassify E2 VE2 <- vclassify-c VE1 VE2 VH. vclassify-i: vhood E -> vhood E1 -> vhood E2 -> vhood (ifz E E1 E2) -> type. %mode vclassify-i +VE +VE1 +VE2 -VER. -: vclassify-i (a-value V) _ _ (a-non-value (nv-i V)). -: vclassify-i a-deru0 _ _ (a-non-value nv-iR). -: vclassify-i (a-non-value NV) _ _ (a-non-value (nv-iC NV)). -: vclassify-i (a-value V) (a-value V1) (a-value V2) (a-value (val-i+ V V1 V2)). -: vclassify-i (a-value V) (a-non-value NV1) _ (a-non-value (nv-iC1 V NV1)). -: vclassify-i (a-value V) (a-value V1) (a-non-value NV2) (a-non-value (nv-iC2 V V1 NV2)). -: vclassify-i a-deru+ _ _ (a-non-value nv-iS). -: vclassify-i (a-value V) a-deru+ _ (a-non-value (nv-iS1 V)). -: vclassify-i (a-value V) (a-value V1) a-deru+ (a-non-value (nv-iS2 V V1)). %worlds (bl-ev) (vclassify-i _ _ _ _). %total {} (vclassify-i _ _ _ _). %unique (vclassify-i +VE +VE1 +VE2 -VER). -: vclassify (ifz E E1 E2) VH <- vclassify E VE <- vclassify E1 VE1 <- vclassify E2 VE2 <- vclassify-i VE VE1 VE2 VH. vclassify-~: vhood E -> vhood (~ E) -> type. %mode vclassify-~ +VE1 -VE. -: vclassify-~ (a-value V) (a-non-value (nv-~ V)). -: vclassify-~ a-deru0 a-deru+. -: vclassify-~ (a-non-value NV) (a-non-value (nv-~C NV)). %worlds (bl-ev) (vclassify-~ _ _). %total {} (vclassify-~ _ _). %unique (vclassify-~ +VE1 -VE). -: vclassify (~ E) VH <- vclassify E VE <- vclassify-~ VE VH. vclassify-^: vhood E -> vhood (^ E) -> type. %mode vclassify-^ +VE1 -VE. -: vclassify-^ (a-value V) (a-value (val-^ V)). -: vclassify-^ a-deru+ (a-non-value nv-^S). -: vclassify-^ (a-non-value NV) (a-non-value (nv-^C NV)). %worlds (bl-ev) (vclassify-^ _ _). %total {} (vclassify-^ _ _). %unique (vclassify-^ +VE1 -VE). -: vclassify (^ E) VH <- vclassify E VE <- vclassify-^ VE VH. vclassify-l+: ({x:arg+ T} vhood (E x)) -> {Ta:tp} {Ua:tp} vhood ((l+ E) : exp _ (at1 Ta Ua)) -> type. %mode vclassify-l+ +VE1 +Ta +Ua -VE. -: vclassify-l+ ([x] (a-value (V x))) _ _ (a-value (val-l+ V)). -: vclassify-l+ ([x] (a-non-value (NV x))) _ _ (a-non-value (nv-l+C NV)). -: vclassify-l+ ([x] a-deru+) _ _ (a-non-value nv-l+S). %worlds (bl-ev) (vclassify-l+ _ _ _ _). %total {} (vclassify-l+ _ _ _ _). %unique (vclassify-l+ +VE1 +Ta +Ua -VE). -: vclassify (l+ E) VH <- ({x:arg+ T} vclassify (E x) (VE x)) <- vclassify-l+ VE _ _ VH. %worlds (bl-ev) (vclassify _ _). %total {E} (vclassify E _). %unique (vclassify +E -P). % ---------------------------------------------------------------------- % Transitions % The function eval is only defined on non-values. Since deru is % not a non-value, the naked shift cannot be reduced. % Since we use the intrinsic encoding, the type of eval expresses % the subject reduction property. eval : {E: exp T A} non-value E -> exp T A -> type. %mode eval +E1 +NV -E2. ev-dZ: eval (dec (n 0)) (nv-d _) (n 0). % to keep dec total, we assume ev-dN: eval (dec (n (1 N))) (nv-d _) (n N). % that dec 0 is 0 ev-dC: eval (dec E) (nv-dC NV) (dec E') <- eval E NV E'. ev-dR: eval (dec (deru C E)) nv-dR (deru ([x] dec (C x)) E). ev-dS: eval (dec ~ (deru C E)) nv-dS (~ (deru ([x] ^ dec ~ (C x)) E)). % When a bound variable is used in an expression, we assign % expression's answer-type to the value being substituted. ev-V: eval (v (arg0- V)) nv-V E' <- val-new-at V _ E'. % beta-rule ev-@: eval ((l E1) @ E2) (nv-@ _ V2) (E1 (arg0- V2)). % delta-rules ev-@F: eval (fst @ cons E1 E2) (nv-@ _ (val-c _ _)) E1. ev-@S: eval (snd @ cons E1 E2) (nv-@ _ (val-c _ _)) E2. % the following darn subtle example shows the need for val-new-at % in the ev-@f rule below: % ti = (? (fix @ (l [self] l [_] n1))). % The naive rule % ev-@f: eval (fix @ E) (nv-@ _ V) (l [x] E @ (fix @ E) @ (v x)). % Gives the signature % ev-@f : % {T1:tp} {T2:tp} {T3:tp} % {E:exp (arr (arr T1 T2 T3) (arr T1 T2 T3) T3) (at0 T3)} {V1:value fix} % {V:value E} % eval (fix @ E) (nv-@ V1 V) (l ([x:arg0 T1] E @ (fix @ E) @ v x)). % and fails the coverage % (essentially, type preservation: the result type is not as general % as the type before the reduction). % {T1:tp} {T2:tp} {T3:tp} {T4:tp} % {E1:arg0 (arr T1 T2 T3) -> exp (arr T1 T2 T3) (at0 T3)} % {E2:exp (arr T1 T2 T3) (at0 T4)} % |- eval (fix @ l ([x:arg0 (arr T1 T2 T3)] E1 x)) (nv-@ val-f val-l0) E2. % % In general, fix @ e has the type % t = [e] fix @ e. % t : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} % exp (arr (arr T1 T2 T3) (arr T1 T2 T3) T3) (at0 T4) % -> exp (arr T1 T2 T3) (at0 T4) % The naive reduction rule forces T3 = T4: the answer type % of producing the recursive function T4 is equated to the answer-type % of the function's body, T3. % The better rule, taking advantage of the fact E must be a value. % ev-@f: eval (fix @ E) (nv-@ _ V) (l [x] E' @ (fix @ E') @ (v x)) % <- val-new-at V _ E'. % The inferred type % ev-@f : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} % {E:exp (arr (arr T1 T2 T3) (arr T1 T2 T3) T3) (at0 T4)} {V:value E} % {E':exp (arr (arr T1 T2 T3) (arr T1 T2 T3) T3) (at0 T3)} {V1:value fix} % val-new-at V T3 E' % -> eval (fix @ E) (nv-@ V1 V) (l ([x:arg0 T1] E' @ (fix @ E') @ v x)). % Note T4. Now, T3 and T4 are kept distinct. % Other unsuccessful attempts: % ev-@f: eval (fix @ l E) (nv-@ _ _) ((l E) @ (l [x] fix @ (l E) @ (v x))). % Inferred type: % ev-@f : % {T1:tp} {T2:tp} {T3:tp} % {E:arg0 (arr T1 T2 T3) -> exp (arr T1 T2 T3) (at0 T3)} {V1:value fix} % {V2:value (l ([x:arg0 (arr T1 T2 T3)] E x))} % eval (fix @ l ([x:arg0 (arr T1 T2 T3)] E x)) (nv-@ V1 V2) % (l ([x:arg0 (arr T1 T2 T3)] E x) % @ l ([x:arg0 T1] fix @ l ([x1:arg0 (arr T1 T2 T3)] E x1) @ v x)). % However, we get around the problem of implicit types being entangled % by using (l E) instead of E % An optimization: we take advantage of the fact that the argument of fix % is a lambda-expression. ev-@f: eval (fix @ l E) (nv-@ _ _) (l [x] (l E) @ (fix @ (l E)) @ (v x)). % Now % ev-@f : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} % {E:arg0 (arr T1 T2 T3) -> exp (arr T1 T2 T3) (at0 T3)} {V1:value fix} % {V2:value (l ([x:arg0 (arr T1 T2 T3)] E x))} % eval (fix @ l ([x:arg0 (arr T1 T2 T3)] E x)) (nv-@ V1 V2) % (l % ([x:arg0 T1] % l ([x1:arg0 (arr T1 T2 T3)] E x1) % @ (fix @ l ([x1:arg0 (arr T1 T2 T3)] E x1)) @ v x)). % Notice {T4:tp}, which was not present before. We need it! % The initial bubble ev-@r: eval (de @ E) (nv-@ _ _) (deru ([x] (v x)) E). ev-@C1: eval (E1 @ E2) (nv-@C1 NV1) (E1' @ E2) <- eval E1 NV1 E1'. ev-@C2: eval (E1 @ E2) (nv-@C2 _ NV2) (E1 @ E2') <- eval E2 NV2 E2'. ev-@R1: eval ((deru C E) @ E2) nv-@R1 (deru ([x] (C x) @ E2) E). ev-@R2: eval (E1 @ (deru C E)) (nv-@R2 _) (deru ([x] E1 @ (C x)) E). ev-+: eval ((n N1) + (n N2)) (nv-+ _ _) (n N3) <- plus N1 N2 N3. ev-+C1: eval (E1 + E2) (nv-+C1 NV1) (E1' + E2) <- eval E1 NV1 E1'. ev-+C2: eval (E1 + E2) (nv-+C2 _ NV2) (E1 + E2') <- eval E2 NV2 E2'. ev-+R1: eval ((deru C E) + E2) nv-+R1 (deru ([x] (C x) + E2) E). ev-+R2: eval (E1 + (deru C E)) (nv-+R2 _) (deru ([x] E1 + (C x)) E). ev-+S1: eval (~ (deru C E) + E2) nv-+S1 (~ (deru ([x] ^ (~ (C x) + E2)) E)). ev-+S2: eval (E1 + ~ (deru C E)) nv-+S2 (~ (deru ([x] ^ (E1 + ~ (C x))) E)). ev-cC1: eval (cons E1 E2) (nv-cC1 NV1) (cons E1' E2) <- eval E1 NV1 E1'. ev-cC2: eval (cons E1 E2) (nv-cC2 _ NV2) (cons E1 E2') <- eval E2 NV2 E2'. ev-cR1: eval (cons (deru C E) E2) nv-cR1 (deru ([x] cons (C x) E2) E). ev-cR2: eval (cons E1 (deru C E)) (nv-cR2 _) (deru ([x] cons E1 (C x)) E). ev-cS1: eval (cons (~ (deru C E)) E2) nv-cS1 (~ (deru ([x] ^ (cons (~ (C x)) E2)) E)). ev-cS2: eval (cons E1 ~ (deru C E)) (nv-cS2 _) (~ (deru ([x] ^ (cons E1 ~ (C x))) E)). ev-iZ: eval (ifz (n 0) E1 E2) (nv-i _) E1. ev-iN: eval (ifz (n 1 _) E1 E2) (nv-i _) E2. ev-iC: eval (ifz E E1 E2) (nv-iC NV) (ifz E' E1 E2) <- eval E NV E'. ev-iC1: eval (ifz E E1 E2) (nv-iC1 _ NV1) (ifz E E1' E2) <- eval E1 NV1 E1'. ev-iC2: eval (ifz E E1 E2) (nv-iC2 _ _ NV2) (ifz E E1 E2') <- eval E2 NV2 E2'. ev-iR: eval (ifz (deru C E) E1 E2) nv-iR (deru ([x] ifz (C x) E1 E2) E). ev-iS: eval (ifz (~ (deru C E)) E1 E2) nv-iS (~ (deru ([x] ^ (ifz (~ (C x)) E1 E2)) E)). ev-iS1: eval (ifz E (~ (deru C1 E1)) E2) (nv-iS1 _) (~ (deru ([x] ^ (ifz E (~ (C1 x)) E2)) E1)). ev-iS2: eval (ifz E E1 (~ (deru C2 E2))) (nv-iS2 _ _) (~ (deru ([x] ^ (ifz E E1 (~ (C2 x)))) E2)). % Reset brings answer-type polymorphism, constructively ev-?: eval (? E) (nv-? V) E' <- val-new-at V _ E'. ev-?C: eval (? E) (nv-?C NV) (? E') <- eval E NV E'. ev-?R: eval (? (deru C E)) nv-?R (? (E @ (l [x] (? (C x))))). ev-~: eval (~ ^ E) (nv-~ _) E. ev-~C: eval (~ E) (nv-~C NV) (~ E') <- eval E NV E'. ev-^C: eval (^ E) (nv-^C NV) (^ E') <- eval E NV E'. ev-^S: eval (^ ~ (deru C E)) nv-^S (deru C E). ev-?+C: eval (?+ E) (nv-?+C NV) (?+ E') <- eval E NV E'. ev-?+S: eval (?+ ~ (deru C E)) nv-?+S (~ deru ([x] ^ (?+ ~ (C x))) E). ev-@+C1: eval (E1 @+ E2) (nv-@+C1 NV1) (E1' @+ E2) <- eval E1 NV1 E1'. ev-@+C2: eval (E1 @+ E2) (nv-@+C2 _ NV2) (E1 @+ E2') <- eval E2 NV2 E2'. ev-@+S1: eval ((~ (deru C E)) @+ E2) nv-@+S1 (~ (deru ([x] ^ ((~ (C x)) @+ E2)) E)). ev-@+S2: eval (E1 @+ ~ (deru C E)) (nv-@+S2 _) (~ (deru ([x] ^ (E1 @+ ~ (C x))) E)). ev-l+C: eval (l+ E) (nv-l+C NV) (l+ E') <- {x:arg+ T} eval (E x) (NV x) (E' x). ev-l+S: eval (l+ [x] ~ (deru (C x) (E x))) nv-l+S (l+ [x] ~ (? (deru (C x) (E x)))). %worlds (bl-ev) (eval _ _ _). %total {E} (eval E _ _). %% Eval is total! we have proven progress: %% Every typed non-value can be reduced. %unique (eval +E1 +NV -E2). % transitive reflexive closure of eval to a value eval* : exp T (at0 Ta) -> exp T (at0 Ta) -> type. %mode eval* +E1 -E2. eval*-value : exp T (at0 Ta) -> {E2: exp T (at0 Ta)} value E2 -> type. %mode eval*-value +E1 -E2 -V2. eval*-vclassify : {E1: exp T A} vhood E1 -> {E2: exp T A} value E2 -> type. %mode eval*-vclassify +E1 +VH -E2 -V2. -: eval*-vclassify E (a-value V) E V. -: eval*-vclassify E1 (a-non-value NV) E2 V2 <- eval E1 NV E1' <- eval*-value E1' E2 V2. -: eval*-value E1 E2 V2 <- vclassify E1 VH <- eval*-vclassify E1 VH E2 V2. %worlds () (eval*-value _ _ _) (eval*-vclassify _ _ _ _). %unique (eval*-vclassify +E1 +VH -E2 -V2) (eval*-value +E1 -E2 -V2). -: eval* E1 E2 <- eval*-value E1 E2 V2. %worlds () (eval* _ _). %unique (eval* +E1 -E2). % ------------------------------------------------------------------------ % Running sample code %query 1 2 eval* (gib @ n1 @ n1 @ n1) n1. %query 1 2 eval* (gib @ n1 @ n1 @ n3) n3. % %query 1 2 eval* (gib @ n1 @ n1 @ n4) n5. % %query 1 2 eval* (gib @ n1 @ n1 @ n5) n8. % takes a bit of time % takes a while % %query 1 1 eval* (gibs @ ^ n2 @ ^ n3 @ n3) R. % R = ^ (n3 + (n2 + n3)). % takes too long!! % %query 1 1 eval* gibs3 % (^ l+ ([x:arg+ int] l+ ([x1:arg+ int] v+ x1 + (v+ x + v+ x1)))). % tests of shift ts1 = ? n0. ts2 = ? (de @ (l [f] (v f @ n0))). ts3 = ? ((de @ (l [f] (v f @ (l [x] (v x + n1))))) @ (n 0)). %query 1 2 eval* ts1 n0. %query 1 2 eval* ts2 n0. %query 1 2 eval* ts3 n1. % Danvy/Filinski's famous example ts4 = ? (n1 + (? (n1 + (de @ (l [f] (n1 + (n1 + (v f @ (v f @ n0)))))) + n1))). %query 1 2 eval* ts4 n7. % Checking CBV: the argument must be evaluated before the substitution ts6' = (l [x] n1) @ (de @ (l [f] n0)). %%query 1 2 eval* ts6' R. %query 1 2 eval* (? ts6') n0. % checking that our shift is shift indeed % We have to fix the answer-type in g, to anything, because there % is no context to determine it, and Twelf doesn't like the remaining variable. ts01 = ? (de @ (l [f] (de @ (l [g:arg0 (arr _ _ int)] n0)))). %query 1 2 eval* ts01 n0. ts02 = ? ((de @ (l [f] (n2 + (v f @ (l [x] v x + n1))))) @ (de @ (l [_] n1))). %query 1 2 eval* ts02 n3. % This also shows the change in the answer-type... ts03 = ? ((de @ (l [f] (v f @ (l [x] v x + n1)))) @ (de @ (l [g] (v g @ n1)))). %query 1 2 eval* ts03 n2. ts04 = ? ((de @ (l [f] (v f @ (de @ (l [f:arg0 (arr _ _ T3)] (l [x] v x + n1)))))) @ (de @ (l [g] (v g @ n0)))). %query 1 2 eval* ts04 (l [x] v x + n1). ts05 = ? ((de @ (l [f] (v f @ (de @ (l [f] v f @ (l [x] v x + n1)))))) @ (de @ (l [g] (v g @ n0)))). %query 1 2 eval* ts05 n1. % patent changing of the answer-type... % Therefore, it does not type-check %% tc01 = ? (n1 + (de @ (l [f] (l [x] (v f @ v x))))). %% %query 1 2 eval* tc01 R. % R = l U1 ([x:exp q0] l U2 ([x1:exp q0] ? (n1 + x1)) @ x). ts8 = ? (n1 + ((l [f] (v f @ n0)) @ (de @ (l [k] (v k @ (l [x] v x + n1)) + n1)))). % %define ti = R %solve _ : (eval t8 R). % %define ti = R %solve _ : (eval ti R). %query 1 2 eval* ts8 (n 1 1 1 0). ts10 = ? (n1 + ((l [f] (v f @ n0)) @ (de @ (l [k] n1 + (v k @ (de @ (l [_: arg0 (arr (arr int int int) int int)] n0))))))). %query 1 2 eval* ts10 n0. % In CBN: (n 1 0). % shift across stages % The following requires the change in the answer-type % It won't type-check %% tss1 = ? ^ (dec ~(de @ (l [f] v f))). %% tss2 = tss1 @ ^ n2. %% %query 1 2 eval* tss1 R. %% R = l U1 ([x:exp q0] ? ^ (~ ^ dec (~ x))). %% %query 1 2 eval* tss2 (^ dec n2). tss21 : exp (& int T1) (at0 T2) = ? ^ (dec ~(de @ (l [f] v f @ ^ n2))). %query 1 3 eval* tss21 (^ dec n2). tss3 : exp (& (arr int int T1) T2) (at0 T3) = ^ (l+ [x] dec ~(de @ (l [f] ^((~ (v f @ ^ v+ x)) + (~ (v f @ ^ v+ x)))))). %query 1 2 eval* tss3 R. % R = ^ l int ([e:exp q1] dec e + dec e). % Making the (pure) function polymorphic in the answer-type of % its body, by doing eta-expansion and introducing reset. % Note the type of f below and the resulting type % of the expression. The result is fully answer-type % polymorphic! % We could use the abbreviation below: % %abbrev % eta-poly1 : {f:exp (arr T1 T2 T2) (at0 T2)} exp (arr T1 T2 T3) (at0 T4) % = [f] l [y] ? f @ v y. % However, the following definition as an (object level) constant % improves the performance, since abbreviations are expanded but % definitions are not. Therefore, definitions are shared. % That means a lot in Twelf repeatedly rebuilding of terms. eta-poly1 = l [f] l [y] ? v f @ v y. % realistic example seemingly requiring answer-type polymorphism tpoly = de @ (l [k] l [table] v k @ (eta-poly1 @ (v table @ n1)) @ (v table)). % tpoly : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} {T5:tp} % exp (arr T1 T2 T3) (at0 arr (arr int (arr T1 T2 T2) (arr T1 T2 T2)) T4 T5) % the result is the pure function, whose body is pure: arr T1 T2 T3. % The answer-type T3 can be instantiated to anything. % Therefore, tpoly1 and tpoly2 below type-check. tpoly1 = tpoly @ n2. % tpoly1 : % {T1:tp} {T2:tp} {T3:tp} % exp T1 (at0 arr (arr int (arr int T1 T1) (arr int T1 T1)) T2 T3) tpoly2 : exp int (at0 T1) = (? ((l [x] l [table] v x) @ tpoly1)) @ (l [u1] l [u2] v u1 + v u2). %query 1 2 eval* tpoly2 n3. % A few examples demonstrating congruences, suggested by Ken tcong1 = fix @ ((l [f] v f) @ (l [self] l [_] n1)). %% %query 1 2 eval* tcong1 R. %query 1 2 eval* (tcong1 @ n7) n1. % The subtle example %query 1 2 eval* (? (fix @ (l [self] l [_] n1))) R. tcong2 = ? fix @ (de @ (l [k] v k @ (l [self] l [x] v x + n1))). % %define tn = R %solve _ : vclassify tcong2 (a-non-value R). % %define ti = R %solve _ : (eval tcong2 tn R). % %define tn = R %solve _ : vclassify ti (a-non-value R). % %define ti = R %solve _ : (eval ti tn R). %query 1 2 eval* (tcong2 @ n7) n8. % pairs tpair1 = ? (fst @ (cons (de @ (l [k] v k @ n1)) (de @ (l [k] v k @ n2)))). %query 1 2 eval* tpair1 n1. tpair2 = ? (snd @ (cons (de @ (l [k] v k @ n1)) (de @ (l [k] v k @ n2)))). %query 1 2 eval* tpair2 n2. % Examples from the paper % Section on delimited continuations and staging t_const : exp (arr T1 (arr T2 T1 T3) T4) (at0 T5) = l [y] l [z] v y. t_get : exp T1 (at0 arr T1 T2 T3) = de @ (l [k] l [z] v k @ v z @ v z). t_put : exp (arr T1 T1 (arr T1 T2 T3)) (at0 T4) = l [z'] de @ (l [k] l [z] v k @ v z' @ v z'). paper_ex0 : exp (& int T1) (at0 T2) = (? (t_const @ ^ (~ t_get + ~ t_get))) @ ^(n1 + n4). %query 1 1 eval* paper_ex0 (^ (n1 + n4 + (n1 + n4))). paper_ex1 : exp (& int T1) (at0 T2) = (? (t_const @ ^ (~ (t_put @ ^(n1 + n4)) + ~ t_get))) @ ^ n0. %query 1 1 eval* paper_ex1 (^ (n1 + n4 + (n1 + n4))). % t_put with memoization t_put' : exp (arr (& T1 T2) (& T1 T3) (arr (& T1 T4) (& T5 T2) (& T5 T2))) (at0 T6) = l [z'] de @ (l [k] l [z] ^((l+ [x] ~(v k @ ^ v+ x @ ^ v+ x)) @+ (~ v z'))). paper_ex3 : exp (& int T1) (at0 & int T1) = (? (t_const @ ^ (~ (t_put' @ ^(n1 + n4)) + ~ t_get))) @ ^ n0. %% %query 1 2 teval* paper_ex2 (apure &int). %query 1 1 eval* paper_ex3 (^ (l+ ([x:arg+ int] v+ x + v+ x) @+ (n1 + n4))). % Attempt to smuggle out the binding % It is ill-typed % paper_ex2 = (? (t_const @ ((l [x] t_get) @ ^(l+ [y] ~(t_put @ ^ v+ y))))) @ % ^ n0. % paper_ex0 with a binding. The binding `cuts' the mutation and makes the % state inaccessible. The example becomes stuck and won't type either. %{ paper_ex0' = (? (t_const @ ^(l+ [x] %% the only change (~ t_get + ~ t_get)))) @ ^(n1 + n4). }% % ------------------------------------------------------------------------ % Staged Gibonacci with memoization and let insertion % Please see fib.ml % Performance % Performance is awful. It seems my Twelf installation % (binary Linux distribution, compiled by MLTon?) has bad GC: % once the program allocated more than certain threshold, everything % slows down to a crawl. The twelf server may allocate 2GB of heap space, % never giving up any memory to OS. % Declaring the eval predicate deterministic is bad: it slows everything down. % Tabling eval, value, non-value predicates is extremely bad. % Even the simplest queries (see test-memo1) would run then about % 10 minutes, in 2GB of space. % It seems there is only one sure optimization method: use a lot % of abbreviations and definitions. This is the only way to achieve % sharing as Twelf repeatedly rebuilds terms. % compare two integers, return 0 if they are equal. Otherwise, return non-zero. int-compare : exp (arr int (arr int int T1) T1) (at0 T2) = fix @ l [self] l [i1] l [i2] (ifz (v i1) (v i2) (ifz (v i2) (v i1) (v self @ (dec v i1) @ (dec v i2)))). %query 1 2 eval* (int-compare @ n1 @ n2) n1. %query 1 2 eval* (int-compare @ n2 @ n1) n1. %query 1 2 eval* (int-compare @ n2 @ n2) n0. % Memoization table, with int keys and values of the type TV % It is a function of the signature %% memo-sig = [TV] int => (int * (int => TV)). % (memo key) reduces to % (0, fun _ => omega) if the value is not found % (1, fun _ => v) if the value is found. % The second component of the return value is an assuredly pure % function (so we are safe to apply eta-poly1 to it). omega = (fix @ l [self] v self) @ n0. % The inferred type shows that the term has any type: % omega : {T1:tp} {T2:tp} exp T1 (at0 T2) memo-empty = l [key:arg0 int] (cons n0 (l [_] omega)). % memo-empty : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} {T5:tp} % exp (arr int (int * arr T1 T2 T3) T4) (at0 T5) % Extending the memo table memo-ext = l [memo] l [key0] l [val0] l [key:arg0 int] (ifz (int-compare @ v key @ v key0) (cons n1 (l [_] v val0)) (v memo @ v key)). % Catch requests for memoization; feed the initially empty table const = (l [u] l [table] v u). top-fn : exp T1 (at0 arr (arr int (int * arr T2 T3 T4) T5) T1 T6) -> exp T1 (at0 T6) = [body] (? (const @ body)) @ memo-empty. %abbrev let = [e] [body:arg0 T1 -> exp T2 (at0 T3)] (l body) @ e. %abbrev let+ = [e] [body:arg+ T1 -> exp T2 (at1 (& T2 T4) T4)] (l+ body) @+ e. % Testing the table, standalone test-memo1 = l [key] let (memo-ext @ memo-empty @ n0 @ n5) ([t] let (memo-ext @ v t @ n2 @ n7) ([t] v t @ v key)). %query 1 2 eval* (snd @ (test-memo1 @ n0) @ n8) n5. %query 1 2 eval* (snd @ (test-memo1 @ n2) @ n8) n7. %query 1 2 eval* (top-fn (test-memo1 @ n1)) (cons (n 0) (l ([x:arg0 T1] omega))). % The following expanded version of the above is notable slower. % Do use abbreviations! % %query 1 2 eval* % ((? ( (l [u] l [table] v u) @ (test-memo1 @ n1))) @ memo-empty) % R. % Memoizing fixpoint combinator, unstaged % Table is not an effectful function, all the resets around table % are justified fix-memo = l [f] (v f @ % memo (fix @ l [memo] l [x] % do lookup x first let (de @ (l [k] l [table] (v k @ (v table @ v x)) @ v table)) ([r] ifz (fst @ v r) % value not found (let (v f @ v memo @ v x) % compute the needed value ([u] % extend the table de @ (l [k] l [table] (v k @ v u) @ (memo-ext @ v table @ v x @ v u)))) % value found (? snd @ v r @ n0)))). % Inferred type: % fix-memo : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} % exp % (arr % (arr % (arr int T1 % (arr (arr int (int * arr int T1 T1) (int * arr int T1 T1)) % T2 T3)) % (arr int T1 % (arr (arr int (int * arr int T1 T1) (int * arr int T1 T1)) % T2 T3)) % (arr (arr int (int * arr int T1 T1) (int * arr int T1 T1)) T2 % T3)) % (arr int T1 % (arr (arr int (int * arr int T1 T1) (int * arr int T1 T1)) T2 % T3)) % (arr (arr int (int * arr int T1 T1) (int * arr int T1 T1)) T2 T3)) % (at0 T4) % The following test is stupid. And yet it takes a while to evaluate % (test-fix-memo1 @ n2) % It is so depressing. test-fix-memo1 = fix-memo @ l [self] l [x] (ifz (v x) n1 (v self @ (dec v x))). %query 1 2 eval* (top-fn (test-fix-memo1 @ n0)) n1. % This takes about a minute! %%query 1 2 eval* (top-fn (test-fix-memo1 @ n2)) n1. % Type checking the memoizing combinator %% %query 1 1 teval* fix-memo R. % R = apure (((int *> int / (memo-sig int => U1)) => int => int) => int => int). % The Gibonacci function with memoization gib-memo = l [x] l [y] fix-memo @ l [self] l [k] (ifz (v k) (v x) (ifz (dec (v k)) (v y) (v self @ dec (dec (v k)) + v self @ dec (v k)))). % gib-memo : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} % exp % (arr int % (arr int % (arr int int % (arr % (arr int (int * arr int int int) % (int * arr int int int)) T1 T2)) % (arr (arr int (int * arr int int int) (int * arr int int int)) % T1 T2)) % T3) % (at0 T4) % Inferred type shows that the expression produces an int gmemo-ex1 : exp int (at0 T1) = (top-fn (gib-memo @ n1 @ n1 @ n2)). % %query 1 1 eval* (top-fn (gib-memo @ n1 @ n1 @ n1)) R. % Even the following is slow! % It takes more than 15 mins and 1GB of space. % %query 1 1 eval* (top-fn (gib-memo @ n1 @ n1 @ n2)) R. % The following takes obscene time and space! % The intrinsic encoding is great, but it seems hardly efficient. % %query 1 1 eval* (top-fn (gib-memo @ n1 @ n1 @ n3)) n3. % The following queries would probably finish in the next century... %%query 1 1 eval* (top-fn int (gib-memo @ n1 @ n1 @ n4)) n5. %%query 1 1 eval* (top-fn int (gib-memo @ n1 @ n1 @ n5)) n8. % Staged memoizing fixpoint combinator fix-memo-staged = l [f] (v f @ % memo (fix @ l [memo] l [x] % do lookup x first; the same as in the unstaged case let (de @ (l [k] l [table] (v k @ (v table @ v x)) @ (v table))) ([r] ifz (fst @ v r) % value not found (let (v f @ v memo @ v x) % compute the needed value ([u] % extend the table de @ (l [k] l [table] % let-insertion ^ (let+ (~ v u) [z] ~ (v k @ (^ v+ z) @ (memo-ext @ v table @ v x @ (^ v+ z))))))) % value found (? snd @ v r @ n0)))). % Inferred type is large (due to the answer-types) % fix-memo-staged : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} {T5:tp} % exp % (arr % (arr % (arr int (& T1 T2) % (arr % (arr int (int * arr int (& T1 T2) (& T1 T2)) % (int * arr int (& T1 T2) (& T1 T2))) (& T3 T4) % (& T3 T4))) % (arr int (& T1 T4) % (arr % (arr int (int * arr int (& T1 T2) (& T1 T2)) % (int * arr int (& T1 T2) (& T1 T2))) (& T3 T4) % (& T3 T4))) % (arr % (arr int (int * arr int (& T1 T2) (& T1 T2)) % (int * arr int (& T1 T2) (& T1 T2))) (& T3 T4) % (& T3 T4))) % (arr int (& T1 T4) % (arr % (arr int (int * arr int (& T1 T2) (& T1 T2)) % (int * arr int (& T1 T2) (& T1 T2))) (& T3 T4) % (& T3 T4))) % (arr % (arr int (int * arr int (& T1 T2) (& T1 T2)) % (int * arr int (& T1 T2) (& T1 T2))) (& T3 T4) % (& T3 T4))) % (at0 T5) % In the old version of the code, we got the following type: % R = apure % (((int *> &int / (memo-sig &int => & U1)) => int => &int) => int => &int); % TSE = & int => (int => int * (int => &int)) => & U1; % TSL = int * (int => &int) => memo-sig &int => & U1; % TL = int * (int => &int); % TF = int *> &int / (memo-sig &int => & U1); % TIF = (int *> &int / (memo-sig &int => & U1)) => int => &int. % The staged Gibonacci function with memoization gibs-memo = l [x] l [y] fix-memo-staged @ l [self] l [k] (ifz (v k) (v x) (ifz (dec v k) (v y) (^ (~ (v self @ dec (dec v k)) + ~ (v self @ dec v k))))). % if we ignore answer types, the inferred type is % (&int => &int => int => &int) % The inferred type is (int -> int -> int) code gibs1-memo : exp (& (arr int (arr int int T1) T2) T3) (at0 T4) = ^ (l+ [x] l+ [y] ~ (top-fn (gibs-memo @ ^ v+ x @ ^ v+ y @ n1))). gibs3-memo = ^ (l+ [x] l+ [y] ~ (top-fn (gibs-memo @ ^ v+ x @ ^ v+ y @ n3))). gibs4-memo = ^ (l+ [x] l+ [y] ~ (top-fn (gibs-memo @ ^ v+ x @ ^ v+ y @ n4))). % %query 1 1 eval* gibs1-memo R. % R = ^ l+ ([x:arg+ int] l+ ([x1:arg+ int] v+ x1)). % Earlier result % %query 1 1 eval* gibs3-memo % (^ % l int % ([e:exp q1] % l int % ([e1:exp q1] % l int % ([e2:exp q1] % l int % ([e3:exp q1] % l int ([e4:exp q1] e2 + e4) @ (e3 + e2)) @ e) % @ e1))). % % I took the result produced by gibs3-memo, and removed the quotation mark: % % and replaced q1 with q0: % gibs3-memo-unquoted = % l int % ([e:exp q0] % l int % ([e1:exp q0] % l int % ([e2:exp q0] % l int % ([e3:exp q0] % l int ([e4:exp q0] e2 + e4) @ (e3 + e2)) @ e) % @ e1)). % %query 1 2 teval* gibs3-memo-unquoted (apure (int => int => int)). % %query 1 1 eval* (gibs3-memo-unquoted @ n1 @ n2) n5. % x + 2y = 1 + 2*2 %%query 1 1 eval* gibs4-memo R. %{ takes a while to compute R = ^ l int ([e:exp q1] l int ([e1:exp q1] l int ([e2:exp q1] l int ([e3:exp q1] l int ([e4:exp q1] l int ([e5:exp q1] e4 + e5) @ (e3 + e4)) @ (e2 + e3)) @ e1) @ e)). }% % Here is the unsafe example gibs3-memo-bad, from the end of fib.ml % It is like gibs3-memo, only gibs-memo is placed inside a binding form gibs3-memo-ok = ^ (l+ [x] l+ [y] ~ (top-fn ^(n1 + ~(gibs-memo @ ^ v+ x @ ^ v+ y @ n3)))). % The following no longer typechecks: % gibs3-memo-bad = ^ (l+ [x] l+ [y] % ~ (top-fn % ^((l+ [t] (v+ t) + ~(gibs-memo @ ^ v+ x @ ^ v+ y @ n3)) @+ n1))). % % Expected: arg+ int -> exp T2 (at1 (& T2 T1) T1) % Inferred: {t:arg+ int} % exp int % (at1 % (arr % (arr int % (int * arr ... % because answer-types do no match up... % if- and assertion-insertion % the generator in a direct style gen = l [suba] ^(l+ [arr] l+ [i:arg+ int] (n1 + n2) % simulating a complex expression + ~(v suba @ ^ v+ arr @ ^ v+ i)). omega+ = (fix @+ l+ [self] v+ self) @+ n0. % to emulate assertion failure suba = l [arr] l [i] (de @ (l [k] ^(ifz (~ v i) omega+ ~(v k @ ^( (~ v arr) @+ (~ v i)))))). % suba : % suba : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} {T5:tp} % exp (arr (& (arr int T1 T2) T2) (arr (& int T2) (& T1 T2) (& T3 T2)) T4) % (at0 T5) gen-suba : exp (& (arr (arr int int T1) (arr int int T1) T2) T3) (at0 T4) = gen @ suba. % It type-checks! % The inferred type is pure, without any need for the explicit reset. % This is because a future-level binder has the implicit reset. % And runs. if- is inserted at the front (under the most recent binder). %query 1 1 eval* gen-suba R. %{ R = ^ l+ ([x:arg+ (arr int int T1)] l+ ([x1:arg+ int] ifz (v+ x1) (fix @+ l+ ([x2:arg+ (arr int int T1)] v+ x2) @+ n 0) (n 1 0 + n 1 1 0 + v+ x @+ v+ x1))). }%