Last active
October 29, 2017 21:42
-
-
Save ctford/129fd7f0e096e459f222301e003190a2 to your computer and use it in GitHub Desktop.
A simple example of dual client/server session types.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Data.FSM.Channel | |
import Data.List | |
%default total | |
data Protocol : Type | |
where | |
Out : a -> Protocol -> Protocol | |
In : a -> Protocol -> Protocol | |
Accept : Protocol -> Protocol -> Protocol | |
Select : Protocol -> Protocol -> Protocol | |
Empty : Protocol | |
dual : Protocol -> Protocol | |
dual (Out x p) = In x $ dual p | |
dual (In x p) = Out x $ dual p | |
dual (Accept p1 p2) = Select (dual p1) (dual p2) | |
dual (Select p1 p2) = Accept (dual p1) (dual p2) | |
dual Empty = Empty | |
data Channel : (a:Type) -> Protocol -> (a -> Protocol) -> Type | |
where | |
Send : a -> Channel () (Out a remaining) (const remaining) | |
Receive : Channel a (In a remaining) (const remaining) | |
Choose : (x:Bool) -> Channel () (Select p1 p2) (\r => if x then p1 else p2) | |
Offer : Channel Bool (Accept p1 p2) (\r => if r then p1 else p2) | |
Return : a -> Channel a Empty (const Empty) | |
(>>=) : Channel a p1 next -> ((x:a) -> Channel b (next x) finally) -> Channel b p1 finally | |
Server : Protocol -> Type -> Type | |
Server p a = Channel a p (const Empty) | |
Client : Protocol -> Type -> Type | |
Client p a = Channel a (dual p) (const Empty) | |
Addition : Protocol | |
Addition = In Nat $ In Nat $ Out Nat $ Empty | |
adder : Server Addition String | |
adder = do | |
x <- Receive | |
y <- Receive | |
Send (x+y) | |
Return $ "Added " ++ show x ++ " and " ++ show y ++ "." | |
addee : Nat -> Nat -> Client Addition String | |
addee x y = do | |
Send x | |
Send y | |
sum <- Receive | |
Return $ "The sum is " ++ show sum ++ "." | |
Negation : Protocol | |
Negation = In Nat $ Out Integer $ Empty | |
negator : Server Negation String | |
negator = do | |
x <- Receive | |
Send $ toIntegerNat x * -1 | |
Return $ "Negated " ++ show x ++ "." | |
Calculation : Protocol | |
Calculation = Accept Addition Negation | |
calculator : Server Calculation String | |
calculator = do | |
x <- Offer | |
case x of | |
True => adder | |
False => negator | |
calculatee : Nat -> Client Calculation String | |
calculatee x = do | |
Choose False | |
Send x | |
y <- Receive | |
Return $ "The negation is " ++ show y ++ "." |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment