by Keigo IMAI @ Nagoya University
if you find any bugs please send an email to the above address. any other comments are also appreciated.
or, you can install it by
cabal update cabal install full-sessions
{-# LANGUAGE NoMonomorphismRestriction #-}
p =
new >>>= \ch ->
forkIO (send ch 123) >>>
recv ch >>>= \x ->
io (print x)
*Main> runS p
123
{-# OPTIONS_GHC -F -pgmF ixdopp #-}
server conn = ixdo
x <- recv conn
y <- recv conn
if y==0
then ixdo
sel1 conn -- error case
send conn "division by 0!!"
else ixdo
sel2 conn -- normal case
send conn (x `div` y::Int)
() <- recv conn
ireturn ()
client conn = ixdo
x <- io (do putStr "x:"; readLn)
y <- io (do putStr "y:"; readLn)
send conn (x::Int)
send conn (y::Int)
offer conn
(ixdo -- error case
err <- recv conn
io (putStrLn $ "server returned an error : "++err)
send conn ()
) (ixdo -- normal case
ans <- recv conn
io (putStrLn $ "result: "++(show (ans::Int)))
send conn ()
)
divSystem = ixdo
conn <- new
forkIO $ server conn
client conn
*Main> runS divSystem
x:100
y:20
result: 5
*Main> runS divSystem
x:100
y:0
server returned an error : division by 0!!
sendS and recvS are channel-passing primitives.enter on a channel, next use it, then zero on the channel, and recur the process
clientS chan = ixdo
conn <- sendS_new chan
client conn
zero chan
recur clientS chan
serverS i listen = ixdo
conn <- recvS listen
forkIO $ ixdo
io (putStrLn $ "connection established. "++show i)
server conn
io (putStrLn "disconnect.")
zero listen
recur (serverS (i+1)) listen
divSystemS = ixdo
k <- new
forkIO $ ixdo enter k; serverS 0 k
enter k
clientS k
you can inspect the session types of channels in a Session if it does not contain any free channel vairable
ghci> :type new >>>= \ch -> forkIO (send ch True)
new >>>= \ch -> forkIO (send ch True)
:: (IsEnded ss T, Ended l ss, Length tt' l, Length ss l) =>
Session t tt' (Cap Nil (Recv Bool End) :|: tt') GHC.Conc.ThreadId
the context (IsEnded ss T, Ended l ss, Length ss l) does not mean anything but the type-level list ss contains only
Ended session types
otherwise, with the functions below you can obtain session types of the channels in a Session (though they are not included in the package yet):
typecheck1
:: (Length ss l) =>
(Channel t l -> Session t (u:|:ss) (u':|:ss') a)
-> Session t (u:|:ss) (u':|:ss') a
typecheck1 = error "typecheck cannot be used to describe a process!"
typecheck2
:: (Length ss l) =>
(Channel t (S l) -> Channel t l -> Session t (u1:|:u:|:ss) (u1':|:u':|:ss') a)
-> Session t (u1:|:u:|:ss) (u1':|:u':|:ss') a
typecheck2 = error "typecheck cannot be used to describe a process!"
typecheck3
:: (Length ss l) =>
(Channel t (S (S l)) -> Channel t (S l) -> Channel t l -> Session t (u2:|:u1:|:u:|:ss) (u2':|:u1':|:u':|:ss') a)
-> Session t (u2:|:u1:|:u:|:ss) (u2':|:u1':|:u':|:ss') a
typecheck3 = error "typecheck cannot be used to describe a process!"
ghci> :type typecheck1 (\c -> send c 1)
typecheck1 (\c -> send c 1)
:: (Num t1, Length ss' n) =>
Session t (Cap e (Send t1 s) :|: ss') (Cap e s :|: ss') ()
ghci> :type typecheck2 (\d -> \c -> recv d >>>= \x -> send c x)
typecheck2 (\d -> \c -> recv d >>>= \x -> send c x)
:: (Length ss' l) =>
Session
t
(Cap e (Recv a s) :|: (Cap e1 (Send a s1) :|: ss'))
(Cap e s :|: (Cap e1 s1 :|: ss'))
()