{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

-- Using parameterized (generalized) `monad' to statically enforce
-- lock safety in advanced cases.
--
-- Lock safety means: no held lock may be acquired, no free
-- lock may be freed, all locks must be freed by the end
-- of the computation.
--
-- The simple case of the problem, for one lock, is implemented in
-- http://okmij.org/ftp/Computation/monads.html#param-monad
-- http://okmij.org/ftp/Haskell/DoParamM.hs
--
-- This file deals with the case of multiple locks. For simplicity and
-- clarity, we consider only two locks. Generalization to more than
-- two is straightforward, but requires the type-level programming
-- similar to that of the HList library.
--
-- The first example in this file illustrates acquiring several locks
-- at once. The locks can be released by one unlock command, or
-- one at a time. Any order of lock acquisition and release is supported
-- as long as lock safety holds.
--
-- The second example illustrates conditional acquisition and release
-- of locks, based on a run-time condition. Although we cannot know
-- at compile time the value of the condition, we statically ensure
-- lock safety nevertheless.


module Locks where

import qualified Prelude
import Prelude hiding (return, (>>=), (>>))

-- A parameterized `monad'
class Monadish m where
    return :: a -> m p p a
    fail   :: String -> m p p a
    (>>=)  :: m p q a -> (a -> m q r b) -> m p r b

m1 >> m2 = m1 >>= (const m2)

-- All regular monads are parameterized `monads'
newtype RegularM m p q a = RegularM{unRM :: m a}

instance Prelude.Monad m => Monadish (RegularM m) where
    return = RegularM . Prelude.return
    fail   = RegularM . Prelude.fail
    m >>= f = RegularM ((Prelude.>>=) (unRM m) (unRM . f))


-- ------------------------------------------------------------------------
-- First example: multiple locks and locking several locks at once.
-- For clarity, we limit ourselves here to two locks. The technique
-- is general however, and can support an arbitrary number of locks:
-- the state of the generalized monad becomes then an HList (nested
-- tuple, essentially) of the types of the held locks. We would use
-- the HList library for operations such as membership testing, deletion,
-- insertion, etc. on these HLists.

-- Begin the library code. The classes Insert and
-- Delete are *not* exported

data N1 = N1 deriving Show		-- Avoid Peano numerals for simplicity
data N2 = N2 deriving Show

-- A trivial type equality predicate, most naive but simple.
-- HList has a predicate that takes only a few lines and works for all
-- types, present and declared in the future. That predicate takes 
-- pages to explain, even to Simon Peyton-Jones.
class TEQ a b r | a b -> r

data HTrue
data HFalse

instance TEQ N1 N1 HTrue
instance TEQ N2 N2 HTrue
instance TEQ N1 N2 HFalse
instance TEQ N2 N1 HFalse

-- Locks, indexed by some type (usually, a numeral)
-- We lift the equality of the index types to locks
newtype Lock a = Lock a deriving Show
instance TEQ a b r => TEQ (Lock a) (Lock b) r


-- Here we define a tuple HL2 to emulate an HList of at most two elements
-- and the basic operations on that list. The implementation is the most naive.
-- But it also the most straightforward and so abstracts from the
-- complexity of the HList library

data HL0     = HL0      deriving Show
data HL1 a   = HL1 a    deriving Show
data HL2 a b = HL2 a b  deriving Show

-- The following are _type_ functions. They operate on types

-- insert an element a into l1 yielding l2. The list should not already contain
-- the element a
class Insert a l1 l2 | a l1 -> l2

instance Insert (Lock a) HL0 (HL1 (Lock a))
instance TEQ (Lock a) b HFalse => Insert (Lock a) (HL1 b) (HL2 (Lock a) b)

-- delete an existing element a from l1 yielding l2. 

class Delete a l1 l2 | a l1 -> l2

instance Delete (Lock a) (HL1 (Lock a)) HL0
instance (TEQ (Lock a) b eqab, TEQ (Lock a) c eqac, 
	  Delete' eqab eqac (Lock a) b c l2)
    => Delete (Lock a) (HL2 b c) l2
class Delete' eqab eqac a b c l2 | eqab eqac a b c -> l2
instance Delete' HTrue HFalse (Lock a) (Lock a) c (HL1 c)
instance Delete' HFalse HTrue (Lock a) b (Lock a) (HL1 b)

newtype LIO p q a = LIO{unLIO::IO a}

-- The parameterized `monad' that carries the locking state in its _phantom_
-- parameters i (the state before the action) and o (the state after the
-- action)
instance Monadish LIO where
  return  = LIO . Prelude.return
  m >>= f = LIO ((Prelude.>>=) (unLIO m) (unLIO . f))

-- Lift a few i/o operations to LIO
lput :: String -> LIO p p ()
lput = LIO . putStrLn
lget :: LIO p p String
lget = LIO getLine

-- In the real program, the following will execute actions to acquire
-- or release a lock. Here, we just print out our intentions.
lock :: (Show l, Insert l i o) => l -> LIO i o ()
lock l = LIO (putStrLn $ "Lock " ++ show l)

unlock :: (Show l, Delete l i o) => l -> LIO i o ()
unlock l = LIO (putStrLn $ "UnLock " ++ show l)

-- We should start in unlocked state, and finish in the same state
runLIO :: LIO HL0 HL0 a -> IO a
runLIO = unLIO

nolocks :: LIO HL0 HL0 ()
nolocks = LIO (Prelude.return ())

-- The user code

lock1 = Lock N1				-- useful abbreviations
lock2 = Lock N2

tlock1 = lget >>=  (\l -> 
	 return (read l) >>= (\x ->
	 lput (show (x+1))))

tlock1r = runLIO tlock1
-- If we enter 1, we get the printed result 2

{-
  *VarStateM> :t tlock1
  tlock1 :: LIO p p ()
 Inferred type has the same input and output states and is polymorphic:
 tlock1 does not affect the state of the lock.
-}


tlock2 = lget >>= (\l -> 
	 lock lock1 >> (
	 return (read l) >>= (\x ->
	 lput (show (x+1)))))

{-
  *Locks> :t tlock2
  tlock2 :: LIO HL0 (HL1 (Lock N1)) ()

 The inferred type says that the tlock2 holds the lock1 when terminates.
 One may wonder why the input type is HL0 rather than being polymorphic.
 The answer is the monomorphism restriction. See tlock21 below on how
 to keep the type polymorphic.
-}


-- tlock2r = runLIO tlock2
{- If uncommented, it gives the type error 
    Couldn't match expected type `HL0'
           against inferred type `HL1 (Lock N1)'
 That is, impossible to run code that has not freed Lock1
-}

tlock21 () = lget >>= (\l -> 
	 lock lock1 >> (
	 return (read l) >>= (\x ->
	 lput (show (x+1)))))
{-
 *Locks> :t tlock21
 tlock21 :: (Insert (Lock N1) p q) => () -> LIO p q ()

 Now, the input type state is polymorphic
-}

-- the following is OK
tlock22 () = lock lock2 >> tlock21 ()
tlock23r = runLIO (tlock22 () >> unlock lock1 >> unlock lock2)


-- tlock3 = tlock2 >> unlock lock2
{- the above, if uncommented, gives a type error:

    No instance for (Delete (Lock N2) (HL1 (Lock N1)) r)
      arising from a use of `unlock'
                   at Locks.hs:185:19-30

That is, it is impossible to delete Lock2 from the list that contains 
only Lock1: we acquired Lock1 but then tried to release Lock2
-}

tlock3' = tlock2 >> unlock lock1
tlock3r' = runLIO tlock3'

{-
*Locks> tlock3r'
-- user input: 123
Lock Lock N1
124
UnLock Lock N1
-}

-- An attempt to execute the following
-- tlock4 = tlock2 >> tlock2
{-
 gives a type error:
    Couldn't match expected type `HL0'
           against inferred type `HL1 (Lock N1)'
    When using functional dependencies to combine
      Insert (Lock a) HL0 (HL1 (Lock a)),
        arising from the instance declaration at Locks.hs:103:0
      Insert (Lock N1) HL0 HL0,
        arising from a use of `lock'
                     at Locks.hs:166:2-11

I admit the error message could be clearer about the problem of
trying to acquire the already held lock. There is something we can do
to make the error message clearer, but it complicates the code.
-}

-- The following is OK
tlock4' = tlock2 >> lock lock2
{-
 *Locks> :t tlock4'
 tlock4' :: LIO HL0 (HL2 (Lock N2) (Lock N1)) ()
-}

-- and so is the following
tlock4'' = tlock2 >> unlock lock1 >> tlock2


-- Similarly, the following gives a type error because of an attempt
-- to release a lock twice
-- tlock4''' = tlock2 >> unlock lock1 >> unlock lock1
{-
    No instance for (Delete (Lock N1) HL0 r)
      arising from a use of `unlock'
    ...
    In the second argument of `(>>)', namely `unlock lock1'
    In the expression: tlock2 >> unlock lock1 >> unlock lock1

-}

-- We can add two locks at once
-- We extend our implementation as follows, to permit insertion and
-- deletion of a list of locks

instance Insert HL0 l l
instance Insert a l1 l2 => Insert (HL1 a) l1 l2
instance (Insert a l1 li, Insert b li l2) => Insert (HL2 a b) l1 l2

instance Delete HL0 l l
instance Delete a l1 l2 => Delete (HL1 a) l1 l2
instance (Delete a l1 li, Delete b li l2) => Delete (HL2 a b) l1 l2

-- That was it. End of the changes to the implementation

-- User code: tests

tlock12 = lget >>= (\l -> 
	  lock (HL2 lock1 lock2) >> (
	  return (read l) >>= (\x ->
	  lput (show (x+1)))))

{-
 *Locks> :t tlock12
 tlock12 :: LIO HL0 (HL2 (Lock N2) (Lock N1)) ()

The inferred type says two locks are held at the end of tlock12
-}


-- tlock12r = runLIO tlock12
{- The above, if uncommented, gives a type error:

    Couldn't match expected type `HL0'
           against inferred type `HL2 (Lock N2) (Lock N1)'

 Two locks are not released.
-}

-- tlock12r1 = runLIO (tlock12 >> unlock lock1)
{-
 Still a type error
    Couldn't match expected type `HL0'
           against inferred type `HL1 (Lock N2)'

lock2 is still being held
-}

-- This is OK: we acquire two locks at once but release them separately
tlock12r2 = runLIO (tlock12 >> unlock lock2 >> unlock lock1)

{-
*Locks> tlock12r2
-- user input: 123
Lock HL2 (Lock N1) (Lock N2)
124
UnLock Lock N2
UnLock Lock N1
-}


-- These are OK too: the order of release does not matter
tlock12r3 = runLIO (tlock12 >> unlock (HL2 lock2 lock1))
tlock12r4 = runLIO (tlock12 >> unlock (HL2 lock1 lock2))

-- ------------------------------------------------------------------------
-- Second example: Locking either lock1 or lock2 based on a run-time value
-- We still _statically_ assure lock safety.
-- See the `user code' below, in particular, rtcl3.

-- We extend our implementation again. We use fresh types (eigenvariables)
-- to represent unknown dynamic values.

-- A `typed boolean' 
-- s is the type (eignevariable) that represents the dynamic boolean
newtype TBool s = TBool Bool
newtype TBoolNeg s = TBoolNeg Bool	-- represents the opposite boolean

-- generating a unique s to correspond to the boolean value
brand_bool :: Bool -> (forall s. TBool s -> TBoolNeg s -> w) -> w
brand_bool b f = f (TBool b) (TBoolNeg b)

-- Negating the type boolean, preserving the type s
class Neg a b | a -> b, b -> a where
    neg :: a s -> b s

instance Neg TBool TBoolNeg where
    neg (TBool b) = TBoolNeg b

instance Neg TBoolNeg TBool where
    neg (TBoolNeg b) = TBool b


-- We use a special data type: a conditional lock. For simplicity,
-- we use only one conditional lock. Multiple conditional locks can
-- be handled using the techniques of our Regions paper

-- s is the typed boolean that selects either the lock a or the lock b
-- We can't say which lock is selected as the value of the typed boolean
-- is not statically known
data CL s a b = CL s a b

-- Operations to acquire and release a lock conditionally.
-- Our type state contains not only the name of the lock but also
-- the `name' of the condition. The lock acquired under a condition
-- must be released under the same condition. That statically assures
-- the lock safety.

class CLock s l i o | s l i -> o where
    clock   :: s -> l -> LIO i o ()
    cunlock :: s -> l -> LIO o i ()

instance Show a =>
    CLock (TBool s) (Lock a) HL0 (CL (TBool s) (Lock a) ())
    where clock (TBool b) l = 
	      if b then LIO (putStrLn $ "Lock " ++ show l)
		   else LIO (Prelude.return ())
          cunlock (TBool b) l = 
	      if b then LIO (putStrLn $ "Unlock " ++ show l)
		   else LIO (Prelude.return ())

instance Show a =>
    CLock (TBoolNeg s) (Lock a) HL0 (CL (TBool s) () (Lock a))
    where clock (TBoolNeg b) l = 
	      if b then LIO (Prelude.return ())
		   else LIO (putStrLn $ "Lock " ++ show l)
          cunlock (TBoolNeg b) l = 
	      if b then LIO (Prelude.return ())
		   else LIO (putStrLn $ "Unlock " ++ show l)

instance (Show a, NormCL (CL (TBool s) (Lock a) b) r) =>
    CLock (TBool s) (Lock a) (CL (TBool s) () b) r
    where clock (TBool b) l = 
	      if b then LIO (putStrLn $ "Lock " ++ show l)
		   else LIO (Prelude.return ())
          cunlock (TBool b) l = 
	      if b then LIO (putStrLn $ "Unlock " ++ show l)
		   else LIO (Prelude.return ())

instance (Show a, NormCL (CL (TBool s) b (Lock a)) r) =>
    CLock (TBoolNeg s) (Lock a) (CL (TBool s) b ()) r
    where clock (TBoolNeg b) l = 
	      if b then LIO (Prelude.return ())
		   else LIO (putStrLn $ "Lock " ++ show l)
          cunlock (TBoolNeg b) l = 
	      if b then LIO (Prelude.return ())
		   else LIO (putStrLn $ "Unlock " ++ show l)

-- The same lock acquired under a condition and its negation does
-- not actually depend on the condition: P v ~P == T
class NormCL a b | a -> b
instance (TEQ a b eqab, NormCL' eqab (CL s a b) r) => NormCL (CL s a b) r

class NormCL' eq a b | eq a -> b
instance NormCL' HTrue (CL s a a) (HL1 a)
instance NormCL' HFalse (CL s a b) (CL s a b)

instance TEQ (Lock a) () HFalse
instance TEQ () (Lock a) HFalse

-- User code: tests

-- Here we see the drawback of the quantified variable s
-- We have to specify what the input type state is (using nolocks, for example)
-- Instead of quantification, we could have added a new component to the
-- typestate, a type counter to generate fresh types to name the conditional
-- That makes the code more complex however.
tcl1 = 
    nolocks >> 
    lget >>= (\l -> 
    brand_bool ((read l) > (0::Int)) (\b bnot ->
    clock b lock1 >>
    clock bnot lock1 >>
    lput l))

{-
 *Locks> :t tcl1
 tcl1 :: LIO HL0 (HL1 (Lock N1)) ()
 
The inferred type says that Lock1 is being held unconditionally: indeed,
the same lock is being acquired with under the condition and its negation
-}

-- The following is OK: we can use an unconditional operation to release
-- the lock
tcl1r = runLIO (tcl1 >> unlock lock1)


tcl2 = 
    nolocks >>
    lget >>= (\l -> 
    brand_bool ((read l) > (0::Int)) (\b bnot ->
    clock b lock1 >>
    clock bnot lock2 >>
    lput l))

{-
 *Locks> :t tcl2
 tcl2 :: LIO HL0 (CL (TBool s) (Lock N1) (Lock N2)) ()

 Either lock1 is held, or lock2 -- depending on the dynamic condition
-}

-- tcl21 = tcl2 >> unlock lock1
{- The above, if uncommented, gives a type error:

    No instance for (Delete
                       (Lock N1) (CL (TBool s) (Lock N1) (Lock N2)) r)
      arising from a use of `unlock'
                   at Locks.hs:472:16-27

 Indeed, one cannot unconditionally release a conditionally held lock
-}


{-
rtcl2 = runLIO (
    lget >>= (\l -> 
    brand_bool ((read l) > (0::Int)) (\b bnot ->
    clock b lock1 >>
    clock bnot lock2 >>
    lput l >>
    cunlock b lock1)))
-}

{- The above, if uncommented, gives a type error:
    Couldn't match expected type `()' against inferred type `Lock N2'
      Expected type: CL (TBool s) (Lock N1) ()
      Inferred type: CL (TBool s) (Lock N1) (Lock N2)

The error message essentially says that Lock2 is still being held, 
conditionally. One cannot statically prove lock safety. Indeed, there
exists a program run that violates the safety.
-}


{-
rtcl2 = runLIO (
    lget >>= (\l -> 
    brand_bool ((read l) > (0::Int)) (\b bnot ->
    clock b lock1 >>
    clock bnot lock2 >>
    lput l >>
    cunlock b lock1 >>
    cunlock b lock2)))
-}

{- The above, if uncommented, gives a type error:
    Could not deduce (CLock
                        (TBool s)
                        (Lock N1)
                        (CL (TBool s) (Lock N2) ())
                        (CL (TBool s) (Lock N1) (Lock N2)))
      from the context ()
      arising from a use of `cunlock'
                   at Locks.hs:512:4-18

We try to remove both locks. However, lock2 was acquired under the negation
of the condition and is being released under the original condition.
-}

-- But the following is OK
rtcl3 = runLIO (
    lget >>= (\l -> 
    brand_bool ((read l) > (0::Int)) (\b bnot ->
    clock b lock1 >>
    clock bnot lock2 >>
    lput l >>
    cunlock b lock1 >>
    cunlock bnot lock2)))

-- The following shows that depending on the input value, either lock1
-- is acquired and released, or lock2. The lock safety holds in either
-- case.
{-
*Locks> rtcl3
-- user input: 1
Lock Lock N1
1
Unlock Lock N1
*Locks> rtcl3
-- user input: 0
Lock Lock N2
0
Unlock Lock N2
-}