module Control.Effect.Parameterised.SafeFiles
(openFile, hGetChar, hPutChar, hClose, hIsEOF, runSafeFiles
, SafeFiles, SafeHandle, St
, PMonad(..), (>>), ifThenElse, fail) where
import Prelude hiding (Monad(..))
import Control.Effect.Parameterised
import qualified Prelude as P
import qualified System.IO as IO
import GHC.TypeLits
newtype SafeFiles pre post a = SafeFiles { unSafeFiles :: IO a }
instance PMonad SafeFiles where
return = SafeFiles . P.return
(SafeFiles m) >>= k = SafeFiles (m P.>>= (unSafeFiles . k))
newtype SafeHandle (n :: Nat) =
SafeHandle { unsafeHandle :: IO.Handle }
data St (n :: Nat) (opens :: [Nat])
openFile ::
IO.FilePath
-> IO.IOMode
-> SafeFiles (St h opens) (St (h + 1) (h ': opens)) (SafeHandle h)
openFile f mode = SafeFiles $ fmap SafeHandle (IO.openFile f mode)
hClose :: Member h opens =>
SafeHandle h
-> SafeFiles (St n opens) (St n (Delete h opens)) ()
hClose (SafeHandle h) = SafeFiles (IO.hClose h)
type family Delete (n :: Nat) (ns :: [Nat]) where
Delete n '[] = '[]
Delete n (n ': ns) = ns
Delete n (m ': ns) = m ': Delete n ns
class Member (x :: Nat) (xs :: [Nat]) where
instance Member x (x ': xs) where
instance Member x xs => Member x (y ': xs)
hGetChar :: Member h opens =>
SafeHandle h
-> SafeFiles (St n opens) (St n opens) Char
hGetChar (SafeHandle h) = SafeFiles (IO.hGetChar h)
hPutChar :: Member h opens =>
SafeHandle h
-> Char -> SafeFiles (St n opens) (St n opens) ()
hPutChar (SafeHandle h) c = SafeFiles (IO.hPutChar h c)
hIsEOF :: Member h opens =>
SafeHandle h -> SafeFiles (St n opens) (St n opens) Bool
hIsEOF (SafeHandle h) = SafeFiles (IO.hIsEOF h)
runSafeFiles :: SafeFiles (St 0 '[]) (St n '[]) () -> IO ()
runSafeFiles = unSafeFiles