Session types in Haskell

Presentation.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE EmptyCase #-}

{-# OPTIONS_GHC "-fwarn-incomplete-patterns" #-}

module Presentation where

import Data.Kind (Type)

--
-- +-----+                  +-----------+
-- | Idl | >-- Req -------> | Requested |
-- |  C  | <-----------+    |     S     |
-- +-----+             |    +-----------+
--    v                |          v
--    |                |          |
--    |             ResFin      ResOne
--    |                |          |
--    |                |          v
--   Fin               |    +-----------+
--    |                +--< | Responded | >-- ResMore --\
--    |                     |     S     | <-------------/
--    v                     +-----------+
-- +------+
-- | Fins |
-- +------+
--

data State where
  Idle      :: State
  Requested :: State
  Responded :: State
  Finished  :: State

data Transition (d :: Type) (s :: State) (t :: State) where
  Req     :: Transition Int 'Idle      'Requested
  ResOne  :: Transition Int 'Requested 'Responded
  ResMore :: Transition Int 'Responded 'Responded
  ResFin  :: Transition ()  'Responded 'Idle
  Fin     :: Transition ()  'Idle      'Finished

-- Client :: s -> Type
data Client (s :: State) where
  ClientIdle :: Client 'Idle

-- Server :: s -> Type
data Server (s :: State) where
  ServerRequested :: Server 'Requested
  ServerResponded :: Server 'Responded


-- Same as  (a, b)
data And a b where
  And :: a -> b -> And a b

symmetric_and :: And a b -> And b a
symmetric_and (And a b) = And b a

-- Not (And Int Bool)
--
--   And 42 True
--
-- Not (And Int Bool) :: And Int Bool -> (forall x . x)
type Not t = forall x . t -> x


type Exclusive (local :: state -> Type) (remote :: state -> Type) =
  forall st . Not (And (local st) (remote st))

exclusive :: Exclusive Client Server
exclusive (And c s) = case c of
  ClientIdle -> case s of {}


-- A message is a transition with a value of its datum type
data Message tr from to where
  Message :: tr datum from to -> datum -> Message tr from to


newtype Process r local remote tr st = Process
  { getProcess :: ProcessStep r local remote tr st (Process r local remote tr) }

data ProcessStep r local remote transition state next where

  Send :: local state
       -> Exists (Message transition) state next
       -> ProcessStep r local remote transition state next

  Recv :: remote state
       -> Forall (Message transition) state next
       -> ProcessStep r local remote transition state next

  Done :: Not (local  state)
       -> Not (remote state)
       -> r
       -> ProcessStep r local remote transition state next


connect
  :: Exclusive local remote
  -> Process x local remote transition state
  -> Process y remote local transition state
  -> (x, y)
connect excl (Process local) (Process remote) = connectStep excl local remote


connectStep
  :: Exclusive local remote
  -> ProcessStep x local remote transition state (Process x local remote transition)
  -> ProcessStep y remote local transition state (Process y remote local transition)
  -> (x, y)

connectStep excl (Send _ (Exists msg next)) (Recv _ (Forall k)) =
  connect excl next (k msg)

connectStep excl (Recv _ (Forall k)) (Send _ (Exists msg next)) =
  connect excl (k msg) next

connectStep excl (Done _ _ x) (Done _ _ y) = (x, y)


connectStep excl (Send localAgency _) (Send remoteAgency _) =
  excl (And localAgency remoteAgency)
connectStep excl (Recv remoteAgency _) (Recv localAgency _) =
  excl (And localAgency remoteAgency)

connectStep excl (Send localAgency _) (Done _ notLocalAgency _) =
  notLocalAgency localAgency
connectStep excl (Recv remoteAgency _) (Done notRemoteAgency _ _) =
  notRemoteAgency remoteAgency
connectStep excl (Done _ notRemoteAgency _) (Send remoteAgency _) =
  notRemoteAgency remoteAgency
connectStep excl (Done notLocalAgency _ _) (Recv localAgency _) =
  notLocalAgency localAgency


data Forall transition state next where
  Forall :: (forall state' . (transition state state' -> next state'))
         -> Forall transition state next

data Exists transition state next where
  Exists :: transition state state'
         -> next state'
         -> Exists transition state next