Prototype of type-enforced linear behaviour for Cloud Haskell

cloudsession.hs

{- 

Proof of concept for adding linearity constraints on the communication-patterns
of Cloud Haskell.

Uses the 'effect-monad' package for embedding effect systems in Haskell types:

  cabal install effect-monad

-}

{-# LANGUAGE RebindableSyntax, TypeOperators, DataKinds, KindSignatures, PolyKinds, TypeFamilies, ConstraintKinds, NoMonomorphismRestriction, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, DeriveDataTypeable, StandaloneDeriving #-}

module Main where

import Control.Concurrent ( threadDelay )
import Data.Binary
import Data.Proxy
import Data.Typeable
import Control.Distributed.Process hiding (send,recv,liftIO,newChan,spawnLocal)
import qualified Control.Distributed.Process as CP
import qualified Prelude as P
import Prelude hiding (Monad(..))
import Control.Distributed.Process.Node
import Network.Transport.TCP
import Control.Effect.Monad
import Control.Effect 
import GHC.TypeLits
import GHC.Prim
import Control.Effect.Helpers.List hiding (LookUpA,lookupA)

data Ping = Ping deriving Typeable

-- server: receives a channel 'd' on 'c', and then sends a Ping on 'd'.
server :: Typeable d => RecvChan c (SendChan d Ping) -> Session '[R c, S d] ()
server c = do d <- recv c
              send d Ping
              -- [non-linear usage]
              -- UNCOMMENT THIS: makes a type error.              
              -- send d Ping

-- client: creates a new channel 'd', and sends one endpoint to th server, 
--            then receives a ping on the other endpoint.
client :: SendChan c (SendChan D Ping) -> Session '[S c, R D] ()
client c = do (sendD, recvD) <- newChan (Chan :: (Chan D))
              send c sendD
              Ping <- recv recvD
              liftIO $ putStrLn "Got a ping"

-- Compose server and client
go = do (sPing, rPing) <- newChan (Chan :: (Chan C))
        par (server rPing) (client sPing)
        liftIO $ threadDelay 10000

-- TCP setup 
main :: IO ()
main = (P.>>=) (createTransport "127.0.0.1" "8090" defaultTCPParameters)
        (\transport -> 
    case transport of 
      Right transport -> (P.>>=) (newLocalNode transport initRemoteTable) (\node -> runProcess node (getProcess go))
      Left x -> error $ show x)

{- 'Session' effect monad -}

data Session (s :: [*]) a = Session {getProcess :: Process a}

instance Effect Session where
    type Plus Session s t = s :++ t
    type Unit Session     = '[]
    type Inv Session s t  = Split s t

    return a = Session (P.return a)
    (Session x) >>= k = Session ((P.>>=) x (getProcess . k))

liftIO :: IO a -> Session '[] a
liftIO = Session . CP.liftIO

{- Type-level send and receive information and duality -}

data R c = R
data S c = S

type family Dual (s :: [*]) :: [*] where
    Dual '[] = '[]
    Dual ((R c) ': xs) = (S c) ': (Dual xs)
    Dual ((S c) ': xs) = (R c) ': (Dual xs)

{- Channels -}

-- Can use Symbols (with 7.10 where Symbols are instances of Typeable)
data ChanName = X | Y | Z | C | D deriving Typeable

deriving instance Typeable X
deriving instance Typeable Y
deriving instance Typeable Z
deriving instance Typeable C
deriving instance Typeable D

data Chan (n :: ChanName) = Chan
data SendChan (c :: ChanName) t = SChan (SendPort t) deriving Typeable
data RecvChan (c :: ChanName) t = RChan (ReceivePort t) deriving Typeable

{- Communication/concurrency primitives -}

send :: (Binary a, Typeable a) => SendChan c a -> a -> Session '[S c] ()
send (SChan c) t = Session (sendChan c t)

recv :: (Binary a, Typeable a) => RecvChan c a -> Session '[R c] a
recv (RChan c) = Session (receiveChan c)

newChan :: (Binary a, Typeable a) => Chan c -> Session '[] (SendChan c a, RecvChan c a)
newChan Chan = Session ((P.>>=) CP.newChan (\(s, r) -> P.return (SChan s, RChan r)))

par :: (Split s t, Dual s ~ t) => Session s () -> Session t () -> Session (s :++ t) ProcessId
par x y = do spawnLocal x
             spawnLocal y

spawnLocal :: Session s () -> Session s ProcessId
spawnLocal (Session p) = Session $ CP.spawnLocal p

{- Serialisability of data types -}

instance Binary Ping where
    put Ping = putWord8 0
    get = (P.>>) getWord8 (P.return Ping)

instance (Typeable t, Binary t) => Binary (SendChan c t) where
    put (SChan s) = put s
    get = (P.>>=) get (\x -> P.return (SChan x))