Par Means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs

Parallel.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

module Parallel where

import Control.Concurrent (forkIO)
import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar)
import qualified Control.Functor.Linear as Linear
import Data.Functor (void)
import Prelude.Linear hiding (IO)
import qualified System.IO.Linear as Linear
import Unsafe.Linear (toLinear)
import Prelude (IO, pure)

infixr 1 ~>
type a ~> b = a %1 -> Linear.IO b
type Not a = a ~> ()
type Par a b = Not (Not a, Not b)

linearIO :: Linear.IO () -> IO ()
linearIO io = Linear.withLinearIO (io Linear.>> Linear.pure (Ur ()))

takeMVar' :: MVar a ~> a
takeMVar' = Linear.fromSystemIO . toLinear takeMVar

putMVar' :: MVar a -> a ~> ()
putMVar' m = Linear.fromSystemIO . toLinear (putMVar m)

newEmptyMVar' :: Linear.IO (MVar a)
newEmptyMVar' = Linear.fromSystemIO newEmptyMVar

forkIO' :: Linear.IO () ~> ()
forkIO' = Linear.fromSystemIO . toLinear (\io -> void (forkIO (linearIO io)))

print' :: (Show a) => a ~> ()
print' = Linear.fromSystemIO . toLinear print

unit :: Linear.IO (Linear.IO a, Not a)
unit = Linear.fromSystemIO do
  m <- newEmptyMVar
  pure (takeMVar' m, putMVar' m)

data Prog io where
  Val :: Linear.IO a %1 -> Prog a
  Ch :: (Prog a %1 -> Prog (Not a) %1 -> Prog r) %1 -> Prog r
  Out :: Prog (Not a) %1 -> Prog b %1 -> Prog (a ~> b)
  Out2 :: Prog (Not a) %1 -> Prog (Not b) %1 -> Prog (a `Par` b) %1 -> Prog ()
  App :: Prog (a ~> b) %1 -> Prog a %1 -> Prog b
  Par :: Prog a %1 -> Prog b %1 -> Prog (a `Par` b)

run :: Prog io ~> io
run (Ch k) = Linear.do
  (ma, seta) <- unit
  run (k (Val ma) (val seta))
run (Val a) = a
run (Out pna pb) = Linear.pure \a -> Linear.do
  na <- run pna
  na a
  run pb
run (Out2 pna pnb pk) = Linear.do
  na <- run pna
  nb <- run pnb
  k <- run pk
  k (na, nb)
run (App pf pa) = Linear.do
  f <- run pf
  a <- run pa
  f a
run (Par pa pb) = Linear.pure \(na, nb) -> Linear.do
  forkIO' (run pa Linear.>>= na)
  run pb Linear.>>= nb

infixl 7 !
(!) :: Prog (a ~> b) %1 -> Prog a %1 -> Prog b
(!) = App

infixl 6 |||
(|||) :: Prog a %1 -> Prog b %1 -> Prog (a `Par` b)
(|||) = Par

sendThen :: Prog (Not a) %1 -> Prog a %1 -> Prog b %1 -> Prog b
sendThen na pa pb = Out na pb ! pa

lam :: (Prog a %1 -> Prog b) %1 -> Prog (a ~> b)
lam f = Ch \a na -> Out na (f a)

val :: a %1 -> Prog a
val a = Val (Linear.pure a)

term :: Prog ()
term = val ()

exMiddle :: Prog (a `Par` Not a)
exMiddle = Ch Par

dn :: Prog (Not (Not a) ~> a)
dn = lam (\nna -> Ch \a na -> sendThen nna na a)

closeL :: Prog (() `Par` a) %1 -> Prog a
closeL p = Ch \a na -> (val \() -> Linear.pure Linear.pure) ! Out2 (val Linear.pure) na p ! a

closeR :: Prog (a `Par` ()) %1 -> Prog a
closeR p = Ch \a na -> (val \() -> Linear.pure Linear.pure) ! Out2 na (val Linear.pure) p ! a

cost :: String ~> Int
cost s = case consume s of () -> Linear.pure 1

clientServer1 :: Prog Int
clientServer1 = closeR $ Ch \x nx -> Ch \y ny ->
  sendThen nx (val "prod") y
  ||| sendThen ny (val cost ! x) term

clientServer2 :: Prog Int
clientServer2 = closeR $ Ch \x nx -> Ch \y ny ->
  sendThen nx (lam \a -> lam \b -> a ! (b ! val "prod")) y
  ||| x ! Out ny term ! val cost

check :: String ~> Not (Not (Not (Not String))) ~> Not (Not (Not (Not String)))
check pw = Linear.pure \r -> Linear.pure (case consume pw of () -> r)

channelTrans :: Prog (() `Par` () `Par` ())
channelTrans = Ch \x nx -> Ch \y ny -> Ch \z nz ->
  z ! val print'
  ||| val check ! x ! Out ny term ! Out nz term
  ||| sendThen nx (val "password") (y ! lam \a -> a ! val "message")

plus :: Int ~> Int ~> Int
plus x = Linear.pure \y -> Linear.pure (x + y)

joinPar :: Prog Int
joinPar = closeR $ closeR $ Ch \x nx -> Ch \y ny ->
  val plus ! x ! y
  ||| sendThen nx (val 1000) term
  ||| sendThen ny (val 2345) term

test :: (Show a) => Prog a ~> ()
test p = run p Linear.>>= print'

test3 :: Linear.IO ()
test3 = Linear.do
  p <- run channelTrans
  p (\x -> x (\() -> print' "printer", \() -> print' "server"), \() -> print' "client")

main :: IO ()
main = do
  linearIO (test clientServer2)
  linearIO test3
  linearIO (test joinPar)