Protocol.fs

(*

    Towards verifying message-passing protocols.

    Protocol typically involves two parties, let us call Client and Server,
    a number of states and state transitions involving passing of messages.
    Client has agency - non-deterministic process in process calculi.
    Server is deterministic, but it should handle all possible clients.

    Ideally, we would take a DSL for the protocol, and spit out F# code that
    makes it easy to construct clients and servers, while verifying that the
    protocol is being observed correctly using combination of types and contract
    checking.

    For example, here's a protocol:

    Start
        op1 -> S1
        op2 -> S2

    S1
        stopS1 -> Stopped

    S2
        toS3 -> S3
        toS4 -> S4

    S3
        stopS3 -> Stopped

    s4
        back -> Start
        stopS4 -> Stopped

    Apparently computation expressions can encode the needed state transitions
    for the client. Perhaps here is how the generated code might look for the client.

    TODO: do the counerpart for the Server.
    TODO: is it possible to do this *without* codegen, just in F# typesystem?

*)

type Start = class end
type Stopped = class end

type S0 = class end
type S1 = class end
type S2 = class end
type S3 = class end
type S4 = class end

type M<'S1,'S2,'T> = | M

let U<'T> = Unchecked.defaultof<'T>

let op1 : M<Start,S1,unit> = U
let op2 : M<Start,S2,unit> = U
let stopS1 : M<S1,Stopped,unit> = U
let toS3 : M<S2,S3,unit> = U
let toS4 : int -> M<S2,S4,unit> = U
let stopS3 : M<S3,Stopped,unit> = U
let back : M<S4,Start,int> = U
let stopS4 : M<S4,Stopped,unit> = U

type Builder =
    | Do

    member b.Bind(x: Async<'T>, f: 'T -> M<'S2,'S3,'T>) : M<'S2,'S3,'T> = U
    member b.Bind(x: M<'S1,'S2,'T1>, f: 'T1 -> M<'S2,'S3,'T2>) : M<'S1,'S3,'T2> = U
    member b.Return(x: 'T) : M<'S,'S,'T> = U
    member b.ReturnFrom(x: M<'S1,'S2,'T>) = x

type Client =
    | Client of M<Start,Stopped,unit>

let doSomething : Async<unit> = U

let client =
    Do {
        do! op2
        do! toS4 1
        let! n = back
        do! doSomething
        do! op1
        return! stopS1
    }
    |> Client