(* 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<unit>,
   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.
*)