% Delimited continuations (shift) in CBN
% `Effect polymorphism'
% Regular, CBN functions, take arbitrary expressions as an argument.
% The type of the argument (annotation on the binder) is an arbitrary,
% possibly `effectful' type T. That type provides the _upper bound_
% on the `effectfulness' of the function argument: the function will
% accept any less effectful expression (for example, a pure one) but not
% a more effectful expression. See the TLCA07 paper for the definition of
% the order on effectful types (see also subtype predicate below).
% It follows then that a CBN function whose binder is annotated with a pure
% type U will not accept as an argument any expression that may possibly
% cause a control effect. That might be limiting at times. Therefore,
% we introduce a special category of `strict functions' (aka CBV functions).
% They can take only values as argument. We can write applications
% of such functions to any expression, no matter how effectful.
% That expression must first be evaluated before the application could
% proceed. In a sense, such strict functions are `effect-polymorphic'
% in that they can be applied to arguments with any effectfulness.
% Incidentally, the regular function application is such a `strict'
% function in its first argument.
% Hmm, a better idea occurred to me: instead of introducing a new type
% of expressions (strict functions) and new type of lambda (strict lambda),
% why not to introduce a new sort of applications, the one that is strict
% in both of its arguments? That turns out not too well: too many rules
% have to be introduced, one have to think of strict applications to be
% passed as arguments to CBN functions, etc.
%
% relationship with quotation and thunk translation?
% Types
pure: type. %name pure U.
tp: type. %name tp T.
cotp: type. %name cotp S.
int: pure. % one single primitive type for now.
% strict function (forces the evaluation of its argument)
*>: pure -> tp -> pure. %infix right 200 *>.
% General, non-strict function: may evaluate its argument many times or
% never
=>: tp -> tp -> pure. %infix right 200 =>.
pr: pure -> tp. %prefix 150 pr.
% for shift, answer-types are always pure
=v: cotp -> pure -> tp. %infix right 130 =v.
% co-types are isomorphic to _purest_ functions,
% Indeed, the `hole' in a context is in the position where a value
% is demanded. The range of co-type is also pure because of # at the end.
=^: pure -> pure -> cotp. %infix right 140 =^.
% ------------------------------------------------------------------------
% Expressions (see examples below)
exp: type. %name exp E.
fn!: type. %name fn! D. % strict functions
res: type. %name res C. % coterms
% primitive values: natural literals
nat: type. %name nat N.
0: nat.
1: nat -> nat. %prefix 200 1.
n: nat -> exp. %prefix 150 n.
% expressions (terms)
% first argument is the type of the bound variable
% (doesn't have to be a pure type)
l : tp -> (exp -> exp) -> exp. % lambda (x) body
@ : exp -> exp -> exp. %infix left 105 @.
! : fn! -> exp. %prefix 150 !.
xi : cotp -> (res -> exp) -> exp. % shift f. e
% strict functions; increment is a built-in constant
inc : fn!. % increment
l! : pure -> (exp -> exp) -> fn!. % lambda (x) body, CBV
!l : pure -> (exp -> exp) -> exp = [t] [f] ! l! t f.
!inc = ! inc.
% co-terms
# : res. % Top co-term
, : exp -> res -> res. %infix right 250 ,.
;!: res -> fn! -> res. %infix right 250 ;!.
% co-term application (aka, filling the hole)
< : res -> exp -> exp. %infix left 100 <.
% Abbreviation for reset
? : exp -> exp = [e] # < e. %prefix 150 ?. % reset
% The following `abstract term' isn't present in the
% regular terms (at run-time). It is only used for
% abstract interpretation.
% The abstract value is the `value' in the sense it is
% not inspectable and not traversable.
at: tp -> exp. %prefix 110 at.
% abstract co-term
ar: cotp -> res. %prefix 110 ar.
% introducing context for hypothetical reasoning:
% special co-term to hold the hypothesis (aka, type)
cl: tp -> res. %prefix 110 cl.
cl!: pure -> res. %prefix 110 cl!.
ct: cotp -> res. %prefix 110 ct.
cx: pure -> pure -> res.
% classification of expressions: values and non-values
val : exp -> type.
%mode val +E.
val-n: val (n N).
val-l: val (l _ E). % non-strict functions are values
val-s: val (! D). % so are the strict functions
%worlds () (val _).
%terminates (E) (val E).
% Non-values are used to `orient' the term equalities (which govern
% focusing and unfocusing)
nonval : exp -> type.
%mode nonval +E.
nval-@: nonval (E1 @ E2).
nval-<: nonval (C < E2).
nval-x: nonval (xi _ _).
%worlds () (nonval _).
%terminates (E) (nonval E).
% one-step reduction of non-values.
eval : exp -> exp -> type.
%mode eval +E1 -E2.
% general function: beta and application ctx accumulation
-: eval (C < l _ E1 @ E2) (C < E1 E2).
-: eval (C < E1 @ E2) ((E2 , C) < E1) <- nonval E1.
% strict functions
-: eval (C < ! inc @ (n N)) (C < n (1 N)).
-: eval (C < ! (l! _ E1) @ E2) (C < E1 E2) <- val E2.
-: eval (C < ! D @ E) ((C ;! D) < E) <- nonval E. % ctx accumulation
% reset, multiple context congruence
-: eval (# < E) E <- val E.
-: eval (C1 < (C2 < E)) (C1 < R) <- eval (C2 < E) R.
% shift
-: eval (C < xi _ E) (# < (E C)).
% ctx unwinding
-: eval ((E2 , C) < E1) (C < (E1 @ E2)) <- val E1.
-: eval ((C ;! D1) < E2) (C < (! D1 @ E2)) <- val E2.
%worlds () (eval _ _).
%terminates (E1) (eval E1 _).
% %covers eval +E1 -E2. None of the values are in the domain of eval...
% transitive reflexive closure of eval
eval* : exp -> exp -> type.
%mode eval* +E1 -E2.
-: eval* E E <- val E.
%% shift outside reset is not an error. Rather, it behaves as a (co)value.
% -: eval* (xi S E) (xi S E).
-: eval* E1 E2 <- eval E1 E1' <- eval* E1' E2.
% tests
t1 = ? (n 0).
t2 = ? (xi S [f] (f < (n 0))).
t3 = ? ((xi S [f] (f < (l T [x] x))) @ (n 0)).
t3' = ? ((xi S [f] (f < (!l T [x] (!inc @ x)))) @ (n 0)).
% Danvy/Filinski's famous example
t4 = ? (!inc @ (? (!inc @ (!inc @
(xi S [f] (!inc @ (!inc @ (f < (f < n 0))))))))).
%query 1 2 eval* t1 R.
%query 1 2 eval* t2 R.
%query 1 2 eval* t3 (n 0).
%query 1 2 eval* t3' (n 1 0).
%query 1 2 eval* t4 R.
%query 1 2 eval* t4 (n 1 1 1 1 1 1 1 0).
% CBN vs strict functions
t6 = (l T [x] n 1 0) @ (xi S [f] (f < (n 0))).
%query 1 2 eval* (? t6) (n 1 0). % CBN application: no effect
t6' = (!l T [x] n 1 0) @ (xi S [f] (n 0)). % CBV application: effect
%%query 1 2 eval* t6' R.
%query 1 2 eval* (? t6') (n 0).
% applying an effectful term
t7 = ((l T [x] (xi S1 [_] x)) @ (xi S2 [f] (f < (n 1 0)))).
%%query 1 2 eval* t7 R.
%query 1 2 eval* (? t7) (n 1 0).
% checking that our shift is shift indeed
ts01 = ? (xi S1 [f] (xi S2 [g] (n 0))).
%query 1 2 eval* ts01 (n 0).
ts02 = ? ((xi S1 [f] (f < !inc)) @ (xi S2 [g] (n 0))).
%query 1 2 eval* ts02 (n 0).
% This also shows the change in the answer-type...
ts03 = ? ((xi S1 [f] (f < !inc)) @ (xi S2 [g] (g < n 0))).
%query 1 2 eval* ts03 (n 1 0).
ts04 = ? ((xi S1 [f] (f < (xi S3 [f] !inc))) @ (xi S2 [g] (g < n 0))).
%query 1 2 eval* ts04 !inc.
% Check that we can pass an effectful term, which gets evaluated `inside'
ts05 = ? ((xi S1 [f] (f < (xi S3 [f] f < !inc))) @ (xi S2 [g] (g < n 0))).
%query 1 2 eval* ts05 (n 1 0).
% patent changing of the asnwer-type...
tc01 = ? (!inc @ (xi S1 [f] (l T [x] (f < x)))).
%query 1 2 eval* tc01 R.
% R = l T1 ([x:exp] # ;! inc < x).
% % (display (reset
% % (let ((x (shift f (cons 'a (f '())))))
% % (shift g x))))
% more examples
t8 = ? (!inc @ ((!l T [f] (f @ n 0)) @ (xi S [k] !inc @ (k < !inc)))).
% %define ti = R %solve _ : (eval t8 R).
% %define ti = R %solve _ : (eval ti R).
%query 1 2 eval* t8 (n 1 1 1 0).
t9 = ? ((l T1 [x] (!inc @ x)) @
((l T2 [f] (f @ n 0)) @ (xi S [k] !inc @ (k < !inc)))).
%query 1 2 eval* t9 (n 1 1 1 0).
% t10' = ? (!inc @ (xi S [k] (k < (xi S2 [_] n 0)))).
% %define ti = R %solve _ : (eval t10' R).
% %define ti = R %solve _ : (eval ti R).
% Passing an effectful term to a captured continuation
t10 = ? (!inc @ ((!l T [f] (f @ n 0)) @
(xi S [k] !inc @ (k < (xi S2 [_] n 0))))).
%query 1 2 eval* t10 (n 1 0).
% ------------------------------------------------------------------------
% Typing
% The deterministic predicate that decides subtyping.
% subtype T1 T2 asserts that T1 <= T2.
% Note that we don't explicitly assert T <= T for arbitrary T, since this
% is derivable from the rules below. There is no need to add more
% `choice points'.
subtype : tp -> tp -> type.
%mode subtype +T1 +T2.
% the following two declarations are for the sake of running %queries.
%deterministic subtype.
%tabled subtype.
% Primitive terms are the subtypes of themselves
-: subtype (pr int) (pr int).
% A pure type can always be converted to an impure one:
% a term that has no effect can be over-approximated to have (any)
% effect at all. In other words, U can be generalized to (U =^ T) =v T
% which is essentially the consequence that 'x' can be generalized to
% shift k. k x
% The following rule is a bit more general
-: subtype (pr U1) ((UA2 =^ UR1) =v UR2)
<- subtype (pr U1) (pr UA2)
<- subtype (pr UR1) (pr UR2).
% standard co-variance/contra-variance
-: subtype (pr U1 *> T1) (pr U2 *> T2)
<- subtype T1 T2
<- subtype (pr U2) (pr U1).
-: subtype (pr TA1 => T1) (pr TA2 => T2)
<- subtype T1 T2
<- subtype TA2 TA1.
% Given a function h == (l (U => T) [f] (f e)), where f is a general
% function that takes a pure argument, we can apply h
% to f' of the type U *> T instead. Indeed, the argument of f must be
% a non-effectful term, so (brushing aside non-termination), it doesn't
% matter if we evaluate the argument (as a strict function would require)
% or not. For a strongly-normalizing calculus, we can indeed brush aside
% the termination concerns.
-: subtype (pr U1 *> T1) (pr (pr U2) => T2)
<- subtype (pr U1 *> T1) (pr U2 *> T2).
% subtyping of impure terms. The over-arching idea: if a function
% or a continuation are prepared to deal with the type T2, one can always
% pass a `smaller' type T1.
% The reason for T2 <= T1 below: (U2 =^ T2) is what the body
% of the shift assumed of its context. The shift that assumes the worst
% of the context (the context is exceptional: has the bigger type)
% is always substitutable for the more optimistic shift.
-: subtype ((UA1 =^ U1) =v UR1) ((UA2 =^ U2) =v UR2)
<- subtype (pr UR1) (pr UR2)
<- subtype (pr UA1) (pr UA2)
<- subtype (pr U2) (pr U1).
%worlds () (subtype _ _).
%covers subtype +T1 -T2.
%%terminates {T2} (subtype _ T2).
% Just treating =^ just as a regular arrow...
subcotype : cotp -> cotp -> type.
%mode subcotype +T1 +T2.
-: subcotype (U1A =^ U1R) (U2A =^ U2R)
<- subtype (pr U1R) (pr U2R)
<- subtype (pr U2A) (pr U1A).
%worlds () (subcotype _ _).
%covers subcotype +T1 +T2.
% One-step type-checking relation: one-step abstract interpretation.
% Our goal is to progressively reduce a term to an abstract term.
%
% The drawback of this approach is the difficulty of proving type preservation.
% I don't think Twelf can see the canonical forms of a given type.
% So, preservation should be formulated as follows then:
% if we have a redex (e.g., (l _ E1) E2) which has the type T,
% then as we replace (l _ E1) and E2 with abstract terms at of some types
% and do teval, we obtain the abstract term of the type T.
% Note, (at T) is not in the domain of teval1. So (at T) is a
% `value' for the type-checker.
teval1 : exp -> exp -> type.
%mode teval1 +E1 -E2.
% abstraction of numbers
-: teval1 (n _) (at pr int).
% strict functions
-: teval1 (! inc) (at pr int *> pr int).
-: teval1 (! l! U E) (cl! U < (E at pr U)). % introduce the hypothesis U
% general lambdas
-: teval1 (l TA E) (cl TA < (E at TA)).
% applications
-: teval1 ((at pr U1 *> T1) @ (at pr U2)) (at T1)
<- subtype (pr U2) (pr U1).
-: teval1 ((at pr TA => T1) @ (at TA2)) (at T1)
<- subtype TA2 TA.
% effectful term in a partial context
-: teval1 ((at pr U1 *> T1) @ (at U2A =^ U2R =v UR))
((cx U2R UR) < ((at pr U1 *> T1) @ (at pr U2A))).
-: teval1 ((at U1A =^ U1R =v UR) @ (at T2))
((cx U1R UR) < ((at pr U1A) @ (at T2))).
% congruences. teval1 is somewhat like CBV: needs to `evaluate' both of
% arguments of the application...
-: teval1 ((at T) @ E2) ((at T) @ E2') <- teval1 E2 E2'.
-: teval1 (E1 @ E2) (E1' @ E2) <- teval1 E1 E1'.
% reset
-: teval1 (? (at pr U)) (at pr U).
-: teval1 (? (at U1 =^ U2 =v UR)) (at pr UR)
<- subtype (pr U1) (pr U2).
% ((at pr U2 *> pr UR) @ (? (at T))).
% or (pr U =^ UR) < ? (at T)
% contexts, hypotheses elimination
-: teval1 (cl! U < at T) (at pr U *> T).
-: teval1 (cl TA < at T) (at pr TA => T).
-: teval1 (ct S < at pr U) (at S =v U).
% Type-checking partial co-term.
-: teval1 ((cx UA UR) < at pr U) (at (U =^ UA) =v UR).
% The following is the most complex rule. The effectful term appears
% in the context that already has an effect, U1R
-: teval1 ((cx U1A U1R) < at S2 =v U2F) (at S2 =v U1R)
<- subtype (pr U2F) (pr U1A).
% context application rule, =^E
-: teval1 (ar (UA =^ UR) < at pr U2) (at pr UR)
<- subtype (pr U2) (pr UA).
-: teval1 (ar S1 < at (S2 =v UR)) (at pr UR)
<- subcotype S1 S2.
% congruences
-: teval1 ((E1 , C) < at T) (C < (at T) @ E1).
-: teval1 ((C ;! D1) < at T) (C < ! D1 @ (at T)).
-: teval1 (C < E) (C < E') <- teval1 E E'.
% shift
-: teval1 (xi S E) (ct S < ? (E (ar S))). % introduce co-hyp S
%worlds () (teval1 _ _).
% %terminates (E1) (teval1 E1 _).
% %covers teval1 +E1 -E2. % Only teval (at T) X should be uncovered.
% We can do something like the following. Alas, that means we need a lot
% of pattern-mathing on the result of teval -- which is greatly-inconvenient
% in Twelf (need to define a new type family for each such pattern-match).
% So, we use the equivalent of one-step reduction instead.
% -: teval (n _) (pr int).
% teval-app : tp -> tp -> tp -> type.
% %mode teval-app +T1 +T2 -T3.
% -: teval-app (pr U1 *> T1) (pr U1) T1. % generally, subtype...
%
%
% -: teval (E1 @ E2) T
% <- teval E1 T1
% <- teval E2 T2
% <- teval-app T1 T2 T.
% transitive reflexive closure of teval1: the typechecking relation
teval : exp -> tp -> type.
%mode teval +E1 -T.
-: teval (at T) T.
-: teval E T <- teval1 E E' <- teval E' T.
% tests
%query 1 2 teval t1 (pr int).
%query 1 2 teval (! inc @ n 0) (pr int).
%query 1 2 teval ((!l int [x] ! inc @ x)) (pr int *> (pr int)).
%query 1 2 teval ((!l int [x] ! inc @ x) @ n 0) (pr int).
% pure and impure solutions possible
%query 2 2 teval (l TF [f] l TX [x] f @ x) R.
%query 2 2 teval ((l TF [f] l TX [x] f @ x) @ (!l int [x] ! inc @ x)) R.
%query 2 2 teval ((l TF [f] l TX [x] f @ x) @ (!l int [x] ! inc @ x) @ n 0)
R.
%query 1 1 teval ((l TF [f] l TX [x] f @ x) @ (!l int [x] ! inc @ x) @ n 0)
(pr int).
%query 1 2 teval t2 (pr int).
int=>int = (pr int) => (pr int).
int*>int = int *> (pr int).
%query 1 2 teval (? ((xi (int=>int =^ U) [f] (f < (l (pr int) [x] x))))) R.
% t3 = ? ((xi S [f] (f < (l T [x] x))) @ (n 0)).
%query 1 1 teval (? ((xi (int=>int =^ U) [f] (f < (l (pr int) [x] x))) @
(n 0))) (pr int).
% t3' = ? ((xi S [f] (f < (!l T [x] (!inc @ x)))) @ (n 0)).
%query 1 1 teval (? ((xi (U2 =^ U) [f] (f < (!l T [x] (!inc @ x)))) @
(n 0))) (pr int).
%query 1 2 teval t4 (pr int).
% tests for subtyping
%query 0 2 teval ((l (pr int) [x] x) @ (xi S [_] (n 0))) R. % ill-typed
%query 1 2 teval ((l (S1 =v U) [x] x) @ (xi S [_] (n 0)))
(int =^ int =v int).
%query 1 2 teval ((!l int [x] x) @ (xi S [_] (n 0))) R.
% patent changing of the answer-type...
% tc01 = ? (!inc @ (xi S1 [f] (l T [x] (f < x)))).
%query 1 2 eval* (? (!inc @ (xi S1 [f] (l T [x] (f < x))))) R.
%query 2 2 teval (? (!inc @ (xi S1 [f] (l T [x] (f < x))))) R.
% eval: R = l T ([x:exp] # ;! inc < x)
% teval:
% R = pr (pr int) => (pr int);
% T = pr int;
% S1 = int =^ int.
% also: accepting an effectful term
% R = pr (int =^ int =v U1) => (pr U1);
% T = int =^ int =v U1;
% S1 = int =^ int.
% checking that our shift is shift indeed
% ts01 = ? (xi S1 [f] (xi S2 [g] (n 0))).
%query 1 1 teval ts01 (pr int).
% ts02 = ? ((xi S1 [f] (f < !inc)) @ (xi S2 [g] (n 0))).
% Some type annotations are needed: subtyping makes life complex...
%query 1 1 teval (? ((xi (int*>int =^ U) [f] (f < !inc)) @
(xi S2 [g] (n 0)))) (pr int).
% This also shows the change in the answer-type...
% ts03 = ? ((xi S1 [f] (f < !inc)) @ (xi S2 [g] (g < n 0))).
%query 1 1 teval (? ((xi (int*>int =^ U) [f] (f < !inc)) @
(xi S2 [g] (g < n 0))))
(pr int).
% ts04 = ? ((xi S1 [f] (f < (xi S3 [f] !inc))) @ (xi S2 [g] (g < n 0))).
% %query 1 2 eval* ts04 !inc.
%query 1 1 teval
((xi (int*>int =^ int) [f] (f < (xi (int*>int =^ U2) [f] !inc))) @
(n 0))
(int =^ int =v int *> (pr int)).
% ts04 does typecheck...
%query 1 1 teval
((xi (int*>int =^ int) [f] (f < (xi (int*>int =^ int) [f] !inc))) @
(xi (int =^ U3) [g] (g < n 0)))
(int =^ int =v int *> (pr int)).
% Check that we can pass an effectful term, which gets evaluated `inside'
% ts05 = ? ((xi S1 [f] (f < (xi S3 [f] f < !inc))) @ (xi S2 [g] (g < n 0))).
%query 1 2 teval
((xi (int*>int =^ U) [f] (f < (xi S3 [f] f < !inc))) @
(xi S2 [g] (g < n 0)))
(int =^ int =v int).
% teval
% (!l UA ([x:exp] xi (UA =^ UR) ([f:res] (f < x) @ x))
% @ xi (e =^ U2) ([f:res] c forall1 /tt (f < c c1))) R.
%query 1 1 teval
((!l int [x] xi S ([f:res] (f < x) @ x))
@ xi S2 [f] (!l (int*>int *> pr int) [x] (f < n 0))
)
R.
% CBN and strict functions
%query 1 2 teval t6 (pr int).
%query 1 2 teval t6' R.
% one solution, effectful type
% R = int =^ U1 =v int.
%query 1 2 teval (? t6') (pr int). % still several solutions, all ints
% applying an effectful term
%query 1 1 teval t7 (S1 =v int).
%query 1 1 teval (? t7) (pr int).
% more examples
% t8 = ? (!inc @ ((!l T [f] (f @ n 0)) @ (xi S [k] !inc @ (k < !inc)))).
%query 1 1 teval (? (!inc @ ((!l T [f] (f @ n 0)) @
(xi (int*>int =^ U) [k] !inc @ (k < !inc)))))
(pr int).
% t9 = ? ((l T1 [x] (!inc @ x)) @
% ((l T2 [f] (f @ n 0)) @ (xi S [k] !inc @ (k < !inc)))).
%query 1 1 teval (? ((l T1 [x] (!inc @ x)) @
((l ((int*>int =^ int) =v int) [f] (f @ n 0)) @
(xi (int*>int =^ int) [k] !inc @ (k < !inc)))))
(pr int).
% passing an effectful term to continuation...
% t10 = ? (!inc @ ((!l T [f] (f @ n 0)) @
% (xi S [k] !inc @ (k < (xi S2 [_] n 0))))).
%query 1 1 teval
(xi (U1 =^ int) [k] !inc @ (k < (xi S2 [_] n 0)))
(int =^ int =v int).
%query 1 1 teval
((!l T [f] (f @ n 0)) @
(xi (int*>int =^ int) [k] !inc @ (k < (xi S2 [_] n 0))))
(int =^ int =v int).
%query 1 1 teval (? (!inc @ ((!l T [f] (f @ n 0)) @
(xi (int*>int =^ int) [k]
!inc @ (k < (xi S2 [_] n 0))))))
(pr int).