(* CATCHCONT AND FRIENDS *)
(* NJ-SML source file.
John Longley, October 2007 *)
(* This file contains implementations of some (rather tortuous) operators
of theoretical importance for the Eriskay programming language.
In our paper "Eriskay: an experiment in semantically inspired
language design" we make various claims that certain operations
are programmable given certain other operations.
In this source file we substantiate some of these claims by providing
implementations of the relevant operations (or as close as possible)
in New Jersey SML.
There are two main sections, corresponding to Sections 4 and 5 of
the paper.
*)
(* SECTION 4 of paper: Linear types and continuations *)
(* First the catchcont operators considered in Section 4.
We show how to implement catchcont3 using callcc; it's clear that
using catchcont3 we can program catchcont1 and catchcont2 as well.
Obviously, issues of linearity don't show up in this implementation,
since NJ-SML doesn't have linear types. Thus, this version doesn't
actually enforce linear use of continuations, but otherwise it's
the same operator as in the paper. *)
fun rebuild() = use "catchcont-demo.sml" ;
datatype ('a,'b) Sum = inl of 'a | inr of 'b
type ('r,'s,'t0,'t1) Catchcont =
( {result :'t0, more :('r->'s)->'t1} ,
{arg :'r, resume :'s->('r->'s)->('t0*'t1)} ) Sum
local open SMLofNJ.Cont in
fun catchcont3 (F:(''r->'s)->(''t0*'t1)) =
let val gStore = ref (NONE : (''r -> 's) option)
val returnAddress = ref (NONE : (''t0 * 't1) cont option)
in
callcc (fn k =>
let val answer as (ground, rest) =
F (fn i:''r =>
case !gStore of
SOME g => g i
| NONE => callcc (fn l =>
throw k (inr {arg = i,
resume = fn j => fn g =>
callcc (fn m =>
(gStore := SOME g ;
returnAddress := SOME m ;
throw l j))})))
in case !returnAddress of
NONE => inl {result = ground,
more = fn g => (gStore := SOME g ; rest)}
| SOME m => throw m answer
end)
end
end ;
(* Check type: *)
catchcont3 : ((''r->'s)->(''t0*'t1)) -> (''r,'s,''t0,'t1) Catchcont ;
(* Now let's use this to define some retractions involving the universal type.
(Again, issues of linearity don't show up in this implementation.)
We start by working with a "functional" version of this type, essentially
the type of lazy forests representing strategies for the !(int->int) game.
*)
datatype forest = forest of int -> int * forest ;
(* one should think of the -> here as a LINEAR arrow *)
infix % %%
fun (forest f) % i = f i ;
(* The retraction (Forest->Forest) <| Forest.
To regard a Forest as coding an operation Forest->Forest,
we need some coding/decoding operations corresponding to a bijection
between int+int and int. *)
fun pack (inl n) = 2 * n | pack (inr n) = 2 * n + 1
fun unpack n = (if n mod 2 = 0 then inl else inr) (n div 2) ;
fun F %% i =
let val (n,F) = F % i in (unpack n, F) end ;
(* The "application" operation: only requires linear PCF *)
fun apply F G = forest (fn i => apply'' (F %% i) G)
and apply'' (inl n, F) G = (n, apply F G)
| apply'' (inr n, F) G = (case G % n of (j,G') => apply'' (F %% j) G') ;
(* Typecheck: *)
apply : forest -> forest -> forest ;
(* Much harder is the "lambda" operation, which requires catchcont3.
Some "error handling" is need here to cope with non-linear behaviour
where it can't arise. *)
type branch = int -> int * forest ;
exception NonLinearError ;
val errorBr : branch = fn i => raise NonLinearError ;
fun lambda Phi = lambda' (Phi o forest)
and lambda' (P : branch->forest) =
forest (fn h => lambda'' (fn g => P g % h))
and lambda'' (R : branch->int*forest) =
(case catchcont3 R of
inl {result=ans, more=P'} => (pack (inl ans), lambda' P')
| inr {arg=quest, resume=Q} =>
(pack (inr quest),
forest (fn a => lambda'' (fn br => Q (a, forest br) errorBr)))) ;
(* Typecheck: *)
lambda : (forest -> forest) -> forest ;
(* Actually, this shows we could get away with a catchcont operator
of simpler type, where the test function (''r->'s) was treated as
non-reusable, so the type of "resume" didn't need the (''r->'s) argument.
This is essentially the difference between catchcont1 and catchcont2.
A small worry therefore arises because our catchcont3 requires a
reusable test variable. However, in Eriskay (using linear classes)
one can perform the following useful hack for converting a non-reusable
function into one of reusable type that "expires" after its first use:
*)
exception Expired ;
fun makeReusable (f:''r->'s) =
let val f_opt = ref (SOME f) in
fn x => (case !f_opt of
SOME f' => (f_opt := NONE ; f' x)
| NONE => raise Expired)
end ;
(* Now let's relate our functional representation of the universal type
(via "linearly used" forests) to the imperative one, i.e.
reusable functions int->int with internal state. *)
type object = int -> int
fun forestToObject F : object =
let val Fstore = ref F in
fn i => let val (n,F') = !Fstore % i
in (Fstore := F' ; i)
end
end ;
(* note that the method argument i is of ground type, and that
F is used linearly. *)
fun objectToForest (O:object) =
forest (fn i => (O i, objectToForest O)) ;
(* note non-linearity in O! *)
(* The next task is to implement the retraction (!forest) <| forest *)
(* Crude pairing and unpairing for integers: *)
fun pair (m,n) = if m > n then m*m+n else n*n+n+m
fun sqrt p =
let val n = floor (Math.sqrt (real p)) in
if (n+1)*(n+1) > p then n else n+1
end ;
fun unpair p =
let val m = sqrt p ; val n = p-(m*m) in
if n < m then (m,n) else (n-m,m)
end ;
fun pack' (inl n) =
2 * n | pack' (inr (m,n)) = 2 * pair (m,n) + 1 ;
fun unpack' n =
if n mod 2 = 0 then inl (n div 2) else inr (unpair (n div 2)) ;
(* embed : !forest -> forest *)
exception IndexOutOfRange
fun replace lst pos new =
List.take (lst,pos) @ [new] @ List.drop (lst,pos+1) ;
local
fun embed' F subforests h =
case unpair h of (i,j) =>
if i < List.length subforests then
(case List.nth (subforests,i) % j of
(k,G) => (k, forest (embed' F (replace subforests i G))))
else if i = List.length subforests then
(case F % j of
(k,G) => (k, forest (embed' F (subforests @ [G]))))
else raise IndexOutOfRange ; (* strictly, should diverge *)
in fun embed F = forest (embed' F [])
end ;
(* For the reverse direction, it's convenient to exploit the "object" view
of a strategy. The use of state here is crucial. *)
fun projectObject (O:object) =
let fun copy' i j = (O (pair (i,j)), forest (copy' i))
val counter = ref ~1
in forest (fn j => (counter := !counter + 1 ; copy' (!counter) j))
end ;
fun project F = projectObject (forestToObject F) ;
(* To summarize: thinking of forest "linearly", i.e. as the type
U = \mu \alpha. \int \lolly (\int \times \alpha)_\bot
we now have linearly definable retractions
(U \lolly U) \retract U
!U \retract U
as well as a linearly definable isomorphism
U \iso \bang (\int \lolly \int)
The remaining retractions
\int \retract U, U \times U \retract U, U \plus U \retract U
are straightforward, so we omit them here.
(However, it's worth pointing out that the mapping U -> U \times U
requires a bit of internal state.)
*)
(* [Note to self: would be interesting to include the *coroutine operators*
of intuitionistic type here, although they're not mentioned in the paper.]
*)
(* SECTION 5 of paper: Class implementations *)
(* Let's try and approximate some classimpl types as best we can in SML
(e.g. in the absence of genuine System F polymorphism).
We introduce a couple of abstract classimpl types, along with the
associated representing types.
- classimpl1 has a single field of type object, a single object->object
method, and the constructor argument type is also object.
- classimpl2 (more polymorphic) has a single field of type object
and an additional field of type 'd1 (which the user can choose).
It has two methods, both of type object->object, and the constructor
argument is object * object.
In addition, both classes involve another type variable ('d for classimpl1,
'd2 for classimpl2) which we would like to be bound but isn't. This is
to account for "future state". Note that when we extend from classimpl1
to classimpl2, 'd gets instantiated as 'd1*'d2. *)
(* Some type declarations to set up *)
type argType = object
type stateType = object
type returnType = object
type constrType1 = object ;
type objType1 = argType -> returnType ;
type 'd methodImpl1 =
argType * stateType * 'd -> returnType * stateType * 'd ;
type 'd classrep1 =
{methodImpl1 : 'd methodImpl1 -> 'd methodImpl1,
constrImpl1 : constrType1 -> stateType} ;
type 'd objType2 = (argType -> returnType) *
(argType -> returnType * stateType * 'd) ;
type ('d1,'d2) methodImpl2 =
argType * stateType * 'd1 * 'd2 -> returnType * stateType * 'd1 * 'd2 ;
type ('d1,'d2,'c2) classrep2 =
{methodImpl2 : (('d1,'d2) methodImpl2 * ('d1,'d2) methodImpl2) ->
(('d1,'d2) methodImpl2 * ('d1,'d2) methodImpl2),
constrImpl2 : 'c2 -> stateType * 'd1} ;
fun repack (m:('d1,'d2)methodImpl2) : ('d1*'d2)methodImpl1 =
fn (arg,state,(d1,d2)) =>
case m (arg,state,d1,d2) of (return,state',d1',d2') =>
(return,state',(d1,d2)) ;
fun repack' (m:('d1*'d2)methodImpl1) : ('d1,'d2)methodImpl2 =
fn (arg,state,d1,d2) =>
case m (arg,state,(d1,d2)) of (return,state',(d1',d2')) =>
(return,state',d1,d2) ;
fun addUnit (m:'d methodImpl1) : ('d * unit) methodImpl1 =
fn (arg,state,(d1,())) =>
case m (arg,state,d1) of (return,state',d1') =>
(return,state',(d1,())) ;
(* Some machinery involving in the "new" operations *)
fun fix1 F x = F (fix1 F) x ;
fun thread1 init methodImpl : objType1 =
let val State = ref init
in fn arg =>
let val (return,state',_) = methodImpl (arg,!State,())
in State := state' ; return
end
end ;
fun fix2 (F : (('a->'b)*('c->'d)) -> (('a->'b)*('c->'d))) =
(fn x => #1 (F (fix2 F)) x,
fn y => #2 (F (fix2 F)) y) ;
fun thread2 (init,moreInit) (method1,method2) : 'd objType2 =
let val State = ref init
val MoreState = ref moreInit
in (fn arg =>
let val (return,state',moreState',_) =
method1 (arg,!State,!MoreState,())
in State := state' ; MoreState := moreState' ; return
end,
fn arg =>
let val (return,state',moreState',_) =
method2 (arg,!State,!MoreState,())
in State := state' ; MoreState := moreState' ;
(return,state',moreState')
(* we cheat slightly by building in the fact that the second
method also acts as a read method, whereas this information
really belongs in the method implementation itself *)
end)
end ;
(* Now the presentation of the two classimpl types as abstract types *)
abstype 'd classimpl1 = classimpl1 of 'd classrep1
and ('d1,'d2,'c2) classimpl2 = classimpl2 of ('d1,'d2,'c2) classrep2
with
fun extend1 meth constr = classimpl1 {methodImpl1 = meth, constrImpl1 = constr}
fun new1 (classimpl1 {methodImpl1 = meth, constrImpl1 = constr}) k1 =
thread1 (constr k1) (fix1 meth)
fun extend2 (classimpl1 {methodImpl1 = meth1, constrImpl1 = constr1})
meth2 constr2 =
classimpl2 {methodImpl2 = fn self as (self1,_)
=> meth2 (meth1 (repack self1)) self,
constrImpl2 = fn k2 =>
let val (k1,filler) = constr2 k2 ;
val state1 = constr1 k1
in filler state1
end}
fun new2 (classimpl2 {methodImpl2 = meth, constrImpl2 = constr}) k2 =
thread2 (constr k2) (fix2 meth)
end ;
(* Next, let's code up the isomorphisms between classrep1 and classimpl1.
We first give "nearly right" versions that give the main idea,
then discuss how they need fixing.
One direction is seemingly straightforward: *)
fun repToImpl ({methodImpl1 = meth, constrImpl1 = constr} : 'd classrep1)
: 'd classimpl1 = extend1 meth constr ;
(* Now the main PROGRAMMING TRICK for extracting the underlying
representation from a class implementation. *)
val dummyConstrArg = (fn x => x) : constrType1 ;
val dummyArg = (fn x => x) : argType ;
fun diverge() = diverge() ;
fun implToRep (c : ('d*unit) classimpl1) : 'd classrep1 =
{methodImpl1 = fn sourceImpl =>
let val c' = extend2 c
(fn super => fn (self1,self2) =>
(repack' (addUnit sourceImpl),
repack' super))
(fn (s,d) => (dummyConstrArg, fn _=>(s,d)))
in (fn (a,s,d) => let val o2:'d objType2 = new2 c' (s,d) in (#2 o2)a end)
: 'd methodImpl1
end,
constrImpl1 =
let val c'' = extend2 c
(fn super => fn self =>
(fn (a,s,d1,d2) => (s,s,d1,d2) (* read method *),
fn _ => diverge())) (* dummy method, not used *)
(fn (k,d) => (k, fn t=>(t,d)))
in fn k => let val o2:'d objType2 = new2 c'' (k, diverge()) (* !!! *)
in (#1 o2) dummyArg end
end} ;
(* Minor problem: at the point !!!, we would like a dummy value of type 'd
instead of "diverge()". This is a glitch in the ML version caused by the
fact that 'd isn't localized to the method part.
It's not a problem in Eriskay where we have System F polymorphism. *)
(* One can also write a (more perspicuous?) Java program
illustrating the same idea. I may make one available soon! *)
(* Actually, neither half of the isomorphism is quite right yet,
because we need to force method implementations supplied to
extend1 or extend2 to be (typecheckably) argument-safe.
This can be arranged by means of a RETRACTION which maps arbitrary
method implementations to (best approximating) argument-safe ones.
Let's see how to program this retraction in such a way that the result
is *typecheckably* argument-safe.
First, we massage all our argument, state and result types to
the universal type "forest" using the retractions explained in
the first half of this file. We also translate the method implementation
itself to the type "forest".
Let's suppose we have a strategy (S:forest) for an operation of type
forest * forest -> forest * forest , (arg,state) |-> (result,state')
which happens to behave in an argument-safe way.
We apply this strategy to a pair (arg,state) in a manifestly
argument-safe way as follows: *)
exception NotImplemented ;
exception ArgSafetyViolation ;
exception BadLookup ;
type address = int list
fun lookup f [n] = (case f % n of (m,_) => m)
| lookup f (n::rest) = (case f % n of (_,f') => lookup f' rest)
| lookup f [] = raise BadLookup ;
fun subtree f [] = f
| subtree f (n::rest) = (case f % n of (_,f') => subtree f' rest) ;
fun runArgSafeStrategy S (arg,state) =
(* S managed imperatively for convenience (could be done functionally) *)
let val Sref = ref S
fun nextMove i =
let val (a,S') = (!Sref)%%i in
Sref := S' ; a
end
(* For "first half" of computation, up to the return point.
Here, crucially, we don't pass around forests for arg and state,
only addresses recording our current position in these forests. *)
fun playToReturn argAddr stateAddr q =
(case nextMove q of
inl a =>
(case unpack a of
inl b => playToReturn (argAddr@[b]) stateAddr
(lookup arg (argAddr@[b]))
| inr b => playToReturn argAddr (stateAddr@[b])
(lookup state (stateAddr@[b])))
| inr a => (argAddr,stateAddr,a))
(* For "second half": separate computations of result and state' *)
fun run_S_left (_:forest,_:forest) : forest = raise NotImplemented
fun run_S_right(_:forest,_:forest) : forest = raise NotImplemented
val dummyTree = forest (fn _ => raise ArgSafetyViolation)
(* Now the crucial "ground type funnel" between the two halves: *)
val (argAddr,stateAddr,_) = (* discard dummy termination signal *)
playToReturn [] [] 0 (* arbitrary termination question *)
in
(run_S_left (subtree arg argAddr, subtree state stateAddr),
run_S_right (dummyTree, subtree state stateAddr))
(* We stick in a dummy argument knowing it will never be consulted *)
(* N.B. Dependence of RHS on arg is funnelled through stateAddr *)
end ;
(* This means that, in effect, we can regard the set of argument-safe
method bodies as just another type, which semantically and syntactically
is a retract of the type of all method bodies, so that we have definability
and full abstraction for this type too. We give these "types"
just enough syntactic status in our type system to allow us to
redefine the type 'd classrep1 to be
{methodImpl1 : 'd SAFEmethodImpl1 -> 'd SAFEmethodImpl1,
constrImpl1 : constrType1 -> stateType} ;
(and similarly for classrep2). This allows the classimpl <-> classrep
bijection to be rewritten in such a way that the gadgets passed to
extend1 and extend2 are manifestly argument-safe. *)
(* This gives us the required retractions "pointwise on types" rather
than "uniformly in 'd", but it turns out that this is enough to
give us full abstraction for class types as claimed in the paper.
This is because if we have two strategies for a polymorphic game
that differ at some odd position, we can find a denotable monomorphic
instance that contains this position, and an Opponent strategy that
gets us there. [There's a slight subtlety here about what class of
games we "intersect" over when we interpret polymorphism, but we can
make this choice at our convenience...] If the types of fields, methods etc.
are themselves within the class of types considered in Section 4,
then this Opponent strategy will be language definable. So the
two strategies are observationally distinguishable within the language. *)
(* FURTHER THOUGHTS (not needed to back up the paper):
It is natural to ask whether we can achieve even more,
by doing things more "uniformly in 'd".
(Since the type 'd isn't given along with a retraction into the
universal type, we would really have to make our code work directly
with values of type 'd.)
We can do some such thing by make use of a rather nice fact: if 'd is a
*non-reusable* type variable (which for us it is), then a polymorphic
function of the kind
F : polytype 'd => !(X * 'd -> Y * 'd) -> (X * 'd -> Y * 'd)
can be reconstructed from any of its instances! This is because
in effect we have just a single "token" of type 'd which has to get
passed through the computation, forcing calls to (X*'d -> Y*'d) to be
performed sequentially, and given an instance of F like F,
there's only one possibility for the way F manages the token.
So (roughly speaking), we can take a monomorphic instance of our
polymorphic gadget; extract the underlying strategy in the universal type;
re-polymorphize this strategy; and then execute it (polymorphically)
using a variant of runArgSafeStrategy that also passes around actual
values of type 'd.
*)