3 people like it.

Session types

This snippet is a direct adaptation of Nick Palladinos' Session Types found in http://fssnip.net/j5. The implementation eschews the need for explicit declaration of duality objects by encoding all relevant information in the session signature itself.

  1: 
  2: 
  3: 
  4: 
  5: 
  6: 
  7: 
  8: 
  9: 
 10: 
 11: 
 12: 
 13: 
 14: 
 15: 
 16: 
 17: 
 18: 
 19: 
 20: 
 21: 
 22: 
 23: 
 24: 
 25: 
 26: 
 27: 
 28: 
 29: 
 30: 
 31: 
 32: 
 33: 
 34: 
 35: 
 36: 
 37: 
 38: 
 39: 
 40: 
 41: 
 42: 
 43: 
 44: 
 45: 
 46: 
 47: 
 48: 
 49: 
 50: 
 51: 
 52: 
 53: 
 54: 
 55: 
 56: 
 57: 
 58: 
 59: 
 60: 
 61: 
 62: 
 63: 
 64: 
 65: 
 66: 
 67: 
 68: 
 69: 
 70: 
 71: 
 72: 
 73: 
 74: 
 75: 
 76: 
 77: 
 78: 
 79: 
 80: 
 81: 
 82: 
 83: 
 84: 
 85: 
 86: 
 87: 
 88: 
 89: 
 90: 
 91: 
 92: 
 93: 
 94: 
 95: 
 96: 
 97: 
 98: 
 99: 
100: 
101: 
102: 
103: 
104: 
105: 
106: 
107: 
108: 
109: 
110: 
111: 
112: 
113: 
114: 
115: 
116: 
117: 
118: 
119: 
120: 
121: 
122: 
// Basic Operations
[<AbstractClass>]
type Ops = class end
type Eps = class inherit Ops end 
type Send<'T, 'Rest when 'Rest :> Ops> = class inherit Ops end 
type Recv<'T, 'Rest when 'Rest :> Ops> = class inherit Ops end 
type Choose<'Left, 'Right when 'Left :> Ops and 'Right :> Ops> = class inherit Ops end 
type Offer<'Left, 'Right when 'Left :> Ops and 'Right :> Ops> = class inherit Ops end

// Session Parameterized Monad
type Msg = Msg of (obj * AsyncReplyChannel<unit>)
// session contains phantom types describing both its own and dual structure
type Session<'S1, 'S2, 'RS1, 'RS2, 'T> = Session of (MailboxProcessor<Msg> -> Async<'T>) 
type SessionBuilder() = 
    member self.Return (value : 'T) : Session<'S, 'S, 'RS, 'RS, 'T> = 
        Session (fun _ -> async { return value })
    member self.Bind (session : Session<'S1, 'S2, 'RS1, 'RS2, 'T>, f : 'T -> Session<'S2, 'S3, 'RS2, 'RS3, 'R>) 
        : Session<'S1, 'S3, 'RS1, 'RS3, 'R> =
        Session (fun mailBox ->
            async {
                let (Session r) = session
                let! x = r mailBox
                let (Session r') = f x
                return! r' mailBox
            }) 

let session = new SessionBuilder()

// Basic Operations
let send (value : 'T) : Session<Send<'T, 'Rest>, 'Rest, Recv<'T, 'RRest>, 'RRest, unit> = 
    Session (fun mailBox -> 
        async { return! mailBox.PostAndAsyncReply (fun reply -> Msg (value :> obj, reply)) })

let recv () : Session<Recv<'T, 'Rest>, 'Rest, Send<'T, 'RRest>, 'RRest, 'T> = 
    Session (fun mailBox -> 
        async { 
            let! (Msg (value, reply)) = mailBox.Receive()
            reply.Reply ()
            return value :?> 'T 
        })

let sel1 () : Session<Choose<'First, 'Second>, 'First, Offer<'RFirst, 'RSecond>, 'RFirst, unit> =
    Session (fun mailBox -> 
        async { return! mailBox.PostAndAsyncReply (fun reply -> Msg (true :> obj, reply)) })

let sel2 () : Session<Choose<'First, 'Second>, 'Second, Offer<'RFirst, 'RSecond>, 'RSecond, unit> =
    Session (fun mailBox -> 
        async { return! mailBox.PostAndAsyncReply (fun reply -> Msg (false :> obj, reply)) })

let cases (left : Session<'First, 'Rest, 'RFirst, 'RRest, 'T>) (right : Session<'Second, 'Rest, 'RSecond, 'RRest, 'T>) 
    : Session<Offer<'First, 'Second>, 'Rest, Choose<'RFirst, 'RSecond>, 'RRest, 'T> = 
    Session (fun mailBox -> 
        async {
            let! (Msg (value, reply)) = mailBox.Receive()
            reply.Reply ()
            match value :?> bool with
            | true ->
                let (Session r) = left
                return! r mailBox 
            | false ->
                let (Session r) = right
                return! r mailBox
        })

let run (client : Session<'Client, Eps, 'Server, Eps, 'T>)
        (server : Session<'Server, Eps, 'Client, Eps, unit>) = 
    let mailBox = MailboxProcessor.Start(fun _ -> async { () })
    let (Session r) = server
    let (Session r') = client
    let result  = 
        [|async { let! _ = r mailBox in return Unchecked.defaultof<'T> }; r' mailBox|] 
        |> Async.Parallel |> Async.RunSynchronously 
    result.[1]

let clientAdd() = 
    session {
        do! send 1
        do! send 2
        let! result = recv ()
        return result
    }


let serverAdd() = 
    session {
        let! first = recv ()
        let! second = recv ()
        do! send (first + second)
    }

let clientStringToInt() = 
    session {
        do! send "42"
        let! result = recv ()
        return result
    }

let serverStringToInt() = 
    session {
        let! value = recv ()
        do! send (System.Int32.Parse value)
    }
    
let client (input : int) = 
    session {
        if input = 1 then
            do! sel1 ()
            let! value = clientAdd()
            return value
        else
            do! sel2 ()
            let! value = clientStringToInt()
            return value
    }

let server () =
    cases (serverAdd()) (serverStringToInt())

run  (clientAdd()) (serverAdd()) // 3
run  (clientStringToInt()) (serverStringToInt()) // 42
run  (client 1) (server()) // 3
run  (client 2) (server()) // 42
Multiple items
type AbstractClassAttribute =
  inherit Attribute
  new : unit -> AbstractClassAttribute

Full name: Microsoft.FSharp.Core.AbstractClassAttribute

--------------------
new : unit -> AbstractClassAttribute
type Ops

Full name: Script.Ops
type Eps =
  inherit Ops

Full name: Script.Eps
type Send<'T,'Rest (requires 'Rest :> Ops)> =
  inherit Ops

Full name: Script.Send<_,_>
type Recv<'T,'Rest (requires 'Rest :> Ops)> =
  inherit Ops

Full name: Script.Recv<_,_>
type Choose<'Left,'Right (requires 'Left :> Ops and 'Right :> Ops)> =
  inherit Ops

Full name: Script.Choose<_,_>
type Offer<'Left,'Right (requires 'Left :> Ops and 'Right :> Ops)> =
  inherit Ops

Full name: Script.Offer<_,_>
Multiple items
union case Msg.Msg: (obj * AsyncReplyChannel<unit>) -> Msg

--------------------
type Msg = | Msg of (obj * AsyncReplyChannel<unit>)

Full name: Script.Msg
type obj = System.Object

Full name: Microsoft.FSharp.Core.obj
type AsyncReplyChannel<'Reply>
member Reply : value:'Reply -> unit

Full name: Microsoft.FSharp.Control.AsyncReplyChannel<_>
type unit = Unit

Full name: Microsoft.FSharp.Core.unit
Multiple items
union case Session.Session: (MailboxProcessor<Msg> -> Async<'T>) -> Session<'S1,'S2,'RS1,'RS2,'T>

--------------------
type Session<'S1,'S2,'RS1,'RS2,'T> = | Session of (MailboxProcessor<Msg> -> Async<'T>)

Full name: Script.Session<_,_,_,_,_>
Multiple items
type MailboxProcessor<'Msg> =
  interface IDisposable
  new : body:(MailboxProcessor<'Msg> -> Async<unit>) * ?cancellationToken:CancellationToken -> MailboxProcessor<'Msg>
  member Post : message:'Msg -> unit
  member PostAndAsyncReply : buildMessage:(AsyncReplyChannel<'Reply> -> 'Msg) * ?timeout:int -> Async<'Reply>
  member PostAndReply : buildMessage:(AsyncReplyChannel<'Reply> -> 'Msg) * ?timeout:int -> 'Reply
  member PostAndTryAsyncReply : buildMessage:(AsyncReplyChannel<'Reply> -> 'Msg) * ?timeout:int -> Async<'Reply option>
  member Receive : ?timeout:int -> Async<'Msg>
  member Scan : scanner:('Msg -> Async<'T> option) * ?timeout:int -> Async<'T>
  member Start : unit -> unit
  member TryPostAndReply : buildMessage:(AsyncReplyChannel<'Reply> -> 'Msg) * ?timeout:int -> 'Reply option
  ...

Full name: Microsoft.FSharp.Control.MailboxProcessor<_>

--------------------
new : body:(MailboxProcessor<'Msg> -> Async<unit>) * ?cancellationToken:System.Threading.CancellationToken -> MailboxProcessor<'Msg>
Multiple items
type Async
static member AsBeginEnd : computation:('Arg -> Async<'T>) -> ('Arg * AsyncCallback * obj -> IAsyncResult) * (IAsyncResult -> 'T) * (IAsyncResult -> unit)
static member AwaitEvent : event:IEvent<'Del,'T> * ?cancelAction:(unit -> unit) -> Async<'T> (requires delegate and 'Del :> Delegate)
static member AwaitIAsyncResult : iar:IAsyncResult * ?millisecondsTimeout:int -> Async<bool>
static member AwaitTask : task:Task<'T> -> Async<'T>
static member AwaitWaitHandle : waitHandle:WaitHandle * ?millisecondsTimeout:int -> Async<bool>
static member CancelDefaultToken : unit -> unit
static member Catch : computation:Async<'T> -> Async<Choice<'T,exn>>
static member FromBeginEnd : beginAction:(AsyncCallback * obj -> IAsyncResult) * endAction:(IAsyncResult -> 'T) * ?cancelAction:(unit -> unit) -> Async<'T>
static member FromBeginEnd : arg:'Arg1 * beginAction:('Arg1 * AsyncCallback * obj -> IAsyncResult) * endAction:(IAsyncResult -> 'T) * ?cancelAction:(unit -> unit) -> Async<'T>
static member FromBeginEnd : arg1:'Arg1 * arg2:'Arg2 * beginAction:('Arg1 * 'Arg2 * AsyncCallback * obj -> IAsyncResult) * endAction:(IAsyncResult -> 'T) * ?cancelAction:(unit -> unit) -> Async<'T>
static member FromBeginEnd : arg1:'Arg1 * arg2:'Arg2 * arg3:'Arg3 * beginAction:('Arg1 * 'Arg2 * 'Arg3 * AsyncCallback * obj -> IAsyncResult) * endAction:(IAsyncResult -> 'T) * ?cancelAction:(unit -> unit) -> Async<'T>
static member FromContinuations : callback:(('T -> unit) * (exn -> unit) * (OperationCanceledException -> unit) -> unit) -> Async<'T>
static member Ignore : computation:Async<'T> -> Async<unit>
static member OnCancel : interruption:(unit -> unit) -> Async<IDisposable>
static member Parallel : computations:seq<Async<'T>> -> Async<'T []>
static member RunSynchronously : computation:Async<'T> * ?timeout:int * ?cancellationToken:CancellationToken -> 'T
static member Sleep : millisecondsDueTime:int -> Async<unit>
static member Start : computation:Async<unit> * ?cancellationToken:CancellationToken -> unit
static member StartAsTask : computation:Async<'T> * ?taskCreationOptions:TaskCreationOptions * ?cancellationToken:CancellationToken -> Task<'T>
static member StartChild : computation:Async<'T> * ?millisecondsTimeout:int -> Async<Async<'T>>
static member StartChildAsTask : computation:Async<'T> * ?taskCreationOptions:TaskCreationOptions -> Async<Task<'T>>
static member StartImmediate : computation:Async<unit> * ?cancellationToken:CancellationToken -> unit
static member StartWithContinuations : computation:Async<'T> * continuation:('T -> unit) * exceptionContinuation:(exn -> unit) * cancellationContinuation:(OperationCanceledException -> unit) * ?cancellationToken:CancellationToken -> unit
static member SwitchToContext : syncContext:SynchronizationContext -> Async<unit>
static member SwitchToNewThread : unit -> Async<unit>
static member SwitchToThreadPool : unit -> Async<unit>
static member TryCancelled : computation:Async<'T> * compensation:(OperationCanceledException -> unit) -> Async<'T>
static member CancellationToken : Async<CancellationToken>
static member DefaultCancellationToken : CancellationToken

Full name: Microsoft.FSharp.Control.Async

--------------------
type Async<'T>

Full name: Microsoft.FSharp.Control.Async<_>
Multiple items
type SessionBuilder =
  new : unit -> SessionBuilder
  member Bind : session:Session<'S1,'S2,'RS1,'RS2,'T> * f:('T -> Session<'S2,'S3,'RS2,'RS3,'R>) -> Session<'S1,'S3,'RS1,'RS3,'R>
  member Return : value:'T -> Session<'S,'S,'RS,'RS,'T>

Full name: Script.SessionBuilder

--------------------
new : unit -> SessionBuilder
val self : SessionBuilder
member SessionBuilder.Return : value:'T -> Session<'S,'S,'RS,'RS,'T>

Full name: Script.SessionBuilder.Return
val value : 'T
val async : AsyncBuilder

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.async
member SessionBuilder.Bind : session:Session<'S1,'S2,'RS1,'RS2,'T> * f:('T -> Session<'S2,'S3,'RS2,'RS3,'R>) -> Session<'S1,'S3,'RS1,'RS3,'R>

Full name: Script.SessionBuilder.Bind
val session : Session<'S1,'S2,'RS1,'RS2,'T>
val f : ('T -> Session<'S2,'S3,'RS2,'RS3,'R>)
val mailBox : MailboxProcessor<Msg>
val r : (MailboxProcessor<Msg> -> Async<'T>)
val x : 'T
val r' : (MailboxProcessor<Msg> -> Async<'R>)
val session : SessionBuilder

Full name: Script.session
val send : value:'T -> Session<Send<'T,'Rest>,'Rest,Recv<'T,'RRest>,'RRest,unit> (requires 'Rest :> Ops and 'RRest :> Ops)

Full name: Script.send
member MailboxProcessor.PostAndAsyncReply : buildMessage:(AsyncReplyChannel<'Reply> -> 'Msg) * ?timeout:int -> Async<'Reply>
val reply : AsyncReplyChannel<unit>
val recv : unit -> Session<Recv<'T,'Rest>,'Rest,Send<'T,'RRest>,'RRest,'T> (requires 'Rest :> Ops and 'RRest :> Ops)

Full name: Script.recv
val value : obj
member MailboxProcessor.Receive : ?timeout:int -> Async<'Msg>
member AsyncReplyChannel.Reply : value:'Reply -> unit
val sel1 : unit -> Session<Choose<'First,#Ops>,'First,Offer<'RFirst,#Ops>,'RFirst,unit> (requires 'First :> Ops and 'RFirst :> Ops)

Full name: Script.sel1
val sel2 : unit -> Session<Choose<#Ops,'Second>,'Second,Offer<#Ops,'RSecond>,'RSecond,unit> (requires 'Second :> Ops and 'RSecond :> Ops)

Full name: Script.sel2
val cases : left:Session<'First,'Rest,'RFirst,'RRest,'T> -> right:Session<'Second,'Rest,'RSecond,'RRest,'T> -> Session<Offer<'First,'Second>,'Rest,Choose<'RFirst,'RSecond>,'RRest,'T> (requires 'First :> Ops and 'RFirst :> Ops and 'Second :> Ops and 'RSecond :> Ops)

Full name: Script.cases
val left : Session<#Ops,'Rest,#Ops,'RRest,'T>
val right : Session<#Ops,'Rest,#Ops,'RRest,'T>
type bool = System.Boolean

Full name: Microsoft.FSharp.Core.bool
val run : client:Session<'Client,Eps,'Server,Eps,'T> -> server:Session<'Server,Eps,'Client,Eps,unit> -> 'T

Full name: Script.run
val client : Session<'Client,Eps,'Server,Eps,'T>
val server : Session<'Server,Eps,'Client,Eps,unit>
static member MailboxProcessor.Start : body:(MailboxProcessor<'Msg> -> Async<unit>) * ?cancellationToken:System.Threading.CancellationToken -> MailboxProcessor<'Msg>
val r : (MailboxProcessor<Msg> -> Async<unit>)
val r' : (MailboxProcessor<Msg> -> Async<'T>)
val result : 'T []
module Unchecked

from Microsoft.FSharp.Core.Operators
val defaultof<'T> : 'T

Full name: Microsoft.FSharp.Core.Operators.Unchecked.defaultof
static member Async.Parallel : computations:seq<Async<'T>> -> Async<'T []>
static member Async.RunSynchronously : computation:Async<'T> * ?timeout:int * ?cancellationToken:System.Threading.CancellationToken -> 'T
val clientAdd : unit -> Session<Send<int,Send<int,Recv<'a,'b>>>,'b,Recv<int,Recv<int,Send<'a,'c>>>,'c,'a> (requires 'b :> Ops and 'c :> Ops)

Full name: Script.clientAdd
val result : 'a
val serverAdd : unit -> Session<Recv<int,Recv<int,Send<int,'a>>>,'a,Send<int,Send<int,Recv<int,'b>>>,'b,unit> (requires 'a :> Ops and 'b :> Ops)

Full name: Script.serverAdd
val first : int
val second : int
val clientStringToInt : unit -> Session<Send<string,Recv<'a,'b>>,'b,Recv<string,Send<'a,'c>>,'c,'a> (requires 'b :> Ops and 'c :> Ops)

Full name: Script.clientStringToInt
val serverStringToInt : unit -> Session<Recv<string,Send<int,'a>>,'a,Send<string,Recv<int,'b>>,'b,unit> (requires 'a :> Ops and 'b :> Ops)

Full name: Script.serverStringToInt
val value : string
namespace System
type Int32 =
  struct
    member CompareTo : value:obj -> int + 1 overload
    member Equals : obj:obj -> bool + 1 overload
    member GetHashCode : unit -> int
    member GetTypeCode : unit -> TypeCode
    member ToString : unit -> string + 3 overloads
    static val MaxValue : int
    static val MinValue : int
    static member Parse : s:string -> int + 3 overloads
    static member TryParse : s:string * result:int -> bool + 1 overload
  end

Full name: System.Int32
System.Int32.Parse(s: string) : int
System.Int32.Parse(s: string, provider: System.IFormatProvider) : int
System.Int32.Parse(s: string, style: System.Globalization.NumberStyles) : int
System.Int32.Parse(s: string, style: System.Globalization.NumberStyles, provider: System.IFormatProvider) : int
val client : input:int -> Session<Choose<Send<int,Send<int,Recv<'a,'b>>>,Send<string,Recv<'a,'b>>>,'b,Offer<Recv<int,Recv<int,Send<'a,'c>>>,Recv<string,Send<'a,'c>>>,'c,'a> (requires 'b :> Ops and 'c :> Ops)

Full name: Script.client
val input : int
Multiple items
val int : value:'T -> int (requires member op_Explicit)

Full name: Microsoft.FSharp.Core.Operators.int

--------------------
type int = int32

Full name: Microsoft.FSharp.Core.int

--------------------
type int<'Measure> = int

Full name: Microsoft.FSharp.Core.int<_>
val value : 'a
val server : unit -> Session<Offer<Recv<int,Recv<int,Send<int,'a>>>,Recv<string,Send<int,'a>>>,'a,Choose<Send<int,Send<int,Recv<int,'b>>>,Send<string,Recv<int,'b>>>,'b,unit> (requires 'a :> Ops and 'b :> Ops)

Full name: Script.server

More information

Link:http://fssnip.net/jJ
Posted:4 years ago
Author:Eirik Tsarpalis
Tags: session types , reversible computation