[Haskell-cafe] Design of protocol implementation?

[Tikhon Jelvis]

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, <amindfv at gmail.com> wrote:

>
>
> El Mar 5, 2015, a las 5:58, Christopher Done <chrisdone at gmail.com>
> 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 at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150305/9ed04ed1/attachment.html>