(1) I can't see why the triv argument to kapp (defined on page 6) is ordered rather than unrestricted.
(2) In fact, I don't see why you can't completely keep separate the trivs that are closed, non-substructural values, (all those mentioned in the types of kapp and lam) from the trivs that are ordered and act as intermediate values on the stack. (all those mentioned in the types of app and vlam). Like, make them totally separate types.
I tried to twelf this up, using my thesis-hammer to view it as a nail and extract out the ordered logic stuff as world manipulations. Since I don't have an HLF implementation for ordered logic, I wasn't expecting this to work without hacks. I started out by manually defining a world-type and a star like
w : type. * : w -> w -> w. %infix none 30 *.
and I thought I'd eventually need to put in some bullshit terms like
terrible_hack : type_family (A * (B * C)) -> type_family ((A * B) * C).
for a type family or two to take care of the fact that I can't really represent associativity correctly.
But, a miracle (well, actually, a "stack discipline") occurred, and I observed
(3) I don't need associativity! Or a unit, come to think of it! Apparently the whole Polakow-Pfenning idea also works in (to use Bourbaki's term for an algebra with a binary operator and nothing else) "magma logic". Which I can already reason about in vanilla twelf!
Specifically, the following twelf code SERVER OKs:
% Direct-style types
dr : type. % roots
de : type. % expressions
dt : type. % terms
% Direct-style terms
t2e : dt -> de.
e2r : de -> dr.
dapp : de -> de -> de.
dlam : (dt -> dr) -> dt.
% Substructural logic
w : type.
* : w -> w -> w. %infix none 30 *.
% CPS-style types
cr : type. % roots
ce : w -> type. % expressions
ci : w -> type. % intermediate value on the stack
ct : type. % closed trivial value
cc : w -> type. % continuations
% CPS-style terms
klam : ({x} cc x -> ce x) -> cr.
% (cc ->> ce) -> cr
kapp : ct -> cc X -> ce X. % throw to continuation
% ct -> cc ->> ce
app : cc X -> ci Y -> ci Z -> ce ((X * Y) * Z).
% cc ->> ci ->> ci ->> ce
% or equivalently, since we're at the top level
% cc >-> ci ->> ci ->> ce
lam : (ct -> cr) -> ct.
vlam : ({w} ci w -> ce (X * w)) -> cc X.
% (ci ->> ce) ->> cc
% or equivalently, since we're at the top level
% (ci ->> ce) >-> cc
% CPS translation
cps/r : dr -> cr -> type.
cps/e : de -> cc X -> ce X -> type.
cps/t : dt -> ct -> type.
/ : cps/r (e2r E) (klam E')
<- {qc}{c} cps/e E c (E' qc c).
/ : cps/e (t2e T) C (kapp T' C)
<- cps/t T T'.
/ : cps/e (dapp E1 E2) C E1'
<- ({qf:w} {f:ci qf} cps/e E2 (vlam [qx] [x] app C f x) (E2' qf f))
<- cps/e E1 (vlam [qf] [f] E2' qf f) E1'.
/ : cps/t (dlam B) (lam B')
<- {x:dt} {x':ct} {d: cps/t x x'} cps/r (B x) (B' x').
% Theorem: CPS translation is total
%mode
(cps/r +R -R')
(cps/e +E +C -E')
(cps/t +T -T').
%block b1 : block {x:dt} {x':ct} {d: cps/t x x'}.
%block b2 : block {qx:w} {x:ci qx}.
%block b3 : block {qc:w} {x:cc qc}.
%worlds (b1 | b2 | b3)
(cps/r R R')
(cps/e E C E')
(cps/t T T').
%total (R E T)
(cps/r R R')
(cps/e E C E')
(cps/t T T').
Anyway, I wish it had occurred to me to think of this example when I was working on thesis. It would have been a nice addition.
