MVar without deadlock -- initial try

CheckMVar.hs

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeOperators #-}
--
-- MVar without deadlock
--

module CheckMVar (Z(Z),S(S),(:<),Nil,ListPos,Get,Set,Session,sreturn,sbind,runSession,inSession,inS,FullMVar,EmptyMVar,newMVar,newEmptyMVar,takeMVar,putMVar) where

import qualified Control.Concurrent as C

-- | type level zero
data Z = Z
-- | type level succ
data S n = S n

-- | heterogeneous lists
data hd :< tl = hd :< tl
data Nil = Nil

-- | accessor to the hlists
class ListPos n p where
  type Get n p
  type Set n p e
  get :: n -> p -> Get n p
  set :: n -> p -> e -> Set n p e
instance ListPos Z (e :< p) where
  type Get Z (e :< p) = e
  type Set Z (e :< p) e' = e' :< p
  get _ (e :< _) = e
  set _ (_ :< p) e' = e' :< p
instance ListPos n p => ListPos (S n) (e :< p) where
  type Get (S n) (e :< p) = Get n p
  type Set (S n) (e :< p) e' = e :< Set n p e'
  get (S n) (_ :< p) = get n p
  set (S n) (e :< p) e' = e :< set n p e'

-- | parameterized monad
data Session p q a = Session {unSession::p -> IO (q, a)}

runSession :: Session Nil p () -> IO ()
runSession m = unSession m Nil >> return ()

inSession,inS :: IO a -> Session s s a
inSession m = Session (\p -> m >>= \a -> return (p, a))

inS = inSession

sbind :: Session p q a -> (a -> Session q r b) -> Session p r b
sbind m f = Session (\p -> unSession m p >>= \(q, a) -> unSession (f a) q)

sreturn :: a -> Session p p a
sreturn a = Session (\p -> return (p, a))

-- | MVar
newtype FullMVar a = FullMVar {unFullMVar::C.MVar a}
newtype EmptyMVar a = EmptyMVar {unEmptyMVar::C.MVar a}

newEmptyMVar :: Session p (EmptyMVar a :< p) ()
newEmptyMVar = Session (\p -> C.newEmptyMVar >>= \mv -> return (EmptyMVar mv :< p, ()))

newMVar :: a -> Session p (FullMVar a :< p) ()
newMVar a = Session (\p -> C.newMVar a >>= \mv -> return (FullMVar mv :< p, ()))

takeMVar :: (ListPos n p, Get n p ~ FullMVar a) => n -> Session p (Set n p (EmptyMVar a)) a
takeMVar n = 
  Session (\p -> 
    let mv = unFullMVar (get n p)
    in C.takeMVar mv >>= (\a -> return (set n p (EmptyMVar mv), a)))

putMVar :: (ListPos n p, Get n p ~ EmptyMVar a) => n -> a -> Session p (Set n p (FullMVar a)) ()
putMVar n v =
  Session (\p ->
    let mv = unEmptyMVar (get n p)
    in C.putMVar mv v >> return (set n p (FullMVar mv), ()))

-- XXX how do we handle forkIO??? Session typing discipline may help, but it is not applicable directly
-- see http://hackage.haskell.org/package/full-sessions

main.hs

{-# LANGUAGE RebindableSyntax #-}
import CheckMVar

import Prelude hiding (Monad((>>=),(>>),return,fail))
import qualified Prelude as P (Monad((>>=),(>>),return,fail))

-- rebind the do-notation!
(>>=) = sbind
m >> n = sbind m (const n)
return = sreturn
fail = error

-- type level numbers
zero = Z
one = S Z
two = S (S Z)


test1 = do
  -- create a new mvar
  newMVar 10
  -- take from it using de Bruijn index (i.e. innermost mvar is 'zero')
  x <- takeMVar zero
  inS $ print x -- 10

{-
*Main> :t test1
test1 :: Session p (EmptyMVar Integer :< p) ()
-}

-- check that it actually rejects deadlocks
{-
test1' = do
  newEmptyMVar
  takeMVar zero -- type error here since 0-th mvar is empty

    Couldn't match type `EmptyMVar' with `FullMVar'
    In a stmt of a 'do' block: takeMVar Z
    In the expression:
      do { newEmptyMVar;
           takeMVar Z }
    In an equation for test1':
        test1'
          = do { newEmptyMVar;
                 takeMVar Z }
-}


-- use multiple mvars!
test2 = do
  -- create two new mvar
  newMVar 20
  newMVar "abc"
  x <- takeMVar zero
  inS $ print x -- abc
  y <- takeMVar one
  inS $ print y -- 20

{-
*Main> :t test2
test2
  :: Session p (EmptyMVar [Char] :< (EmptyMVar Integer :< p)) ()
-}

main = 
  runSession test1 P.>>
  runSession test2