Polymorphic Sessions

(* Need to type check using the latest ATS2 *)

staload "session.sats"

#define S 0

#define C 1

extern prfun service {r,r0:role} {p:stype} (!chan(r,prep(r0,p)) >> chan(r,pfix(lam s=>pbrch(r0,pmsg(r0,chan(1-r0,p))::s,pend(r0))))): void

stadef cloud = pquan2(C, lam (x:stype):stype => pmsg(C, chan(S,x)->void) :: prep(C,x))

extern fun cloudserver (chan (S, cloud)): void

implement cloudserver (ch) = let

val [x:stype] ch = exify2 ch

val f = recv {S,C} {prep(C,x)} {chan(S,x)->void} ch

prval _ = service ch

fun loop {x:stype} (ch:chan(S,pfix(lam s=>pbrch(C,pmsg(C,chan(1-C,x))::s,pend(C)))), f:chan(S,x)->void): void = let

prval _ = recurse ch

val choice = offer ch

in

case+ choice of

| ~Right() => wait ch

| ~Left() =>

let

val ep = recv ch

val _ = f ep

in

loop {x} (ch, f)

end

end

in

loop {x} (ch, f)

end

stadef sub = pmsg(C,string)::pend(C)

extern fun client (chan(C, cloud)): void

implement client (ch) = let

fun echo (c:chan(S,sub)): void = (println!(recv c); wait c)

prval _ = unify2 ch

val _ = send (ch, echo)

prval _ = service ch

fun loop (ch:chan(C,pfix(lam s=>pbrch(C,pmsg(C,chan(1-C,sub))::s,pend(C)))), n:int): void = let

prval _ = recurse ch

in

if n <= 0

then (choose(ch,Right()); close ch)

else

let

val _ = choose(ch,Left())

val ep = create {S,C} {sub} (llam x => (send(x, "hello"); close x))

val _ = send (ch, ep)

in

loop (ch, n-1)

end

end

in

loop (ch, 10)

end

extern fun test (): void

implement test () = let

val ch = create {C,S} {cloud} (llam ch => cloudserver ch)

in

client ch

end