sortdef role = {a:int|a==0||a==1} datasort stype = | pmsg of (int, vt@ype) // | pseq of (stype, stype) // please compare this line | pend of (int) stacst pseq: (stype, stype) -> stype // with this line, by running the code #define :: pseq absvtype chan (int, stype) = ptr extern fun create {r1,r2:role} {p:stype} {r1 != r2} (chan(r2,p) -<lincloptr1> void): chan(r1,p) extern fun send {r,r0:role} {p:stype} {a:vt@ype} {r0 == r} (!chan(r, pmsg(r0,a)::p) >> chan(r,p), a): void extern fun recv {r,r0:role} {p:stype} {a:vt@ype} {r0 != r} (!chan(r, pmsg(r0,a)::p) >> chan(r,p)): a extern fun close {r,r0:role} {p:stype} (chan(r, pend r0)): void stadef pi = pmsg(1,int)::pend(1) extern fun server (chan(0,pi)): void extern fun client (chan(1,pi)): void implement server (chan) = let val n = recv chan val _ = $showtype n in close chan end implement client (chan) = let val _ = send (chan, 42) in close chan end