Re: [Haskell-cafe] Design of protocol implementation?

Yeah, session types are worth looking at for specifying the protocol in the type system. A good paper to look at for implementing session types in Haskell is "Haskell Session Types with (Almost) No Class" which gives a nice overview of the idea and presents a design that looks reasonably nice to use. On Thu, Mar 5, 2015 at 6:23 AM, wrote:

El Mar 5, 2015, a las 5:58, Christopher Done escribió:

...

Right, what you have there is the simplest implementation and it seems pretty common to me, for RPC-style services.

The only adjustments I like to make is to ensure input and return are matched up.

Another way I've taken to is e.g. in Fay:

data Returns a = Returns data Command = Procedure Int Char (Returns (Text,Maybe [Int]))

call :: (Returns a -> Command) -> IO a call = …

produce :: Returns a -> IO a -> IO a produce _ m = m

handle :: Command -> IO () handle (Procedure i c r) = produce r (procedure i c)

Another way I've taken was in e.g. ghc-server was to use a GADT:

data Command a where LoadTarget :: Text -> Command (Producer Msg (SuccessFlag,Integer)) Eval :: Text -> Command (Duplex Text Text EvalResult) Ping :: Integer -> Command (Returns Integer) TypeOf :: Text -> Command (Returns Text) LocationAt :: FilePath -> Text -> Int -> Int -> Int -> Int -> Command (Returns SrcSpan) TypeAt :: FilePath -> Text -> Int -> Int -> Int -> Int -> Command (Returns Text) UsesAt :: FilePath -> Text -> Int -> Int -> Int -> Int -> Command (Returns Text) KindOf :: Text -> Command (Returns Text) InfoOf :: Text -> Command (Returns [Text]) Set :: Text -> Command (Returns ()) PackageConf :: FilePath -> Command (Returns ()) SetCurrentDir :: FilePath -> Command (Returns ())

My type looks like a pipe or a conduit, but was more involved because it was a duplex:

type Duplex i o r = DuplexT IO i o r type Producer o r = Duplex () o r type Returns r = Duplex () () r type Unit = Duplex () () ()

But in essence the commands could return a result and/or accept incoming input and produce output. E.g. evaluating a line of Haskell lets you send/receive stdin/stdout and eventually return a success/fail result.

I wrote a few lines of TH to do the dispatching code.

I've also seen an approach using type-level literals to put strings in the types to use dispatching, but I can't remember who wrote it.

You can also use e.g. closed type families to express a finite state machine that this-must-happen-before-that-state etc. if you really want to ensure every state change is valid.

It's hard to find links to any of these things I've seen, not sure what the keywords are.

The search term for this is "session types" -- iirc there's a nice example in spj's paper "fun with type families"

Tom

...

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

---

Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe