effect-monad-0.8.1.0: Embeds effect systems and program logics into Haskell using graded monads and parameterised monads

Safe HaskellSafe
LanguageHaskell98

Control.Effect.Parameterised.SafeFiles

Documentation

openFile :: FilePath -> IOMode -> SafeFiles (St h opens) (St (h + 1) (h ': opens)) (SafeHandle h) Source #

hGetChar :: Member h opens => SafeHandle h -> SafeFiles (St n opens) (St n opens) Char Source #

hPutChar :: Member h opens => SafeHandle h -> Char -> SafeFiles (St n opens) (St n opens) () Source #

hClose :: Member h opens => SafeHandle h -> SafeFiles (St n opens) (St n (Delete h opens)) () Source #

hIsEOF :: Member h opens => SafeHandle h -> SafeFiles (St n opens) (St n opens) Bool Source #

runSafeFiles :: SafeFiles (St 0 '[]) (St n '[]) () -> IO () Source #

data SafeFiles pre post a Source #

Instances

PMonad * SafeFiles Source # 

Methods

return :: a -> pm inv inv a Source #

(>>=) :: pm pre interm t -> (t -> pm interm post t') -> pm pre post t' Source #

data SafeHandle (n :: Nat) Source #

data St (n :: Nat) (opens :: [Nat]) Source #

class PMonad (pm :: k -> k -> * -> *) where Source #

Minimal complete definition

return, (>>=)

Methods

return :: a -> pm inv inv a Source #

(>>=) :: pm pre interm t -> (t -> pm interm post t') -> pm pre post t' Source #

Instances

PMonad * SafeFiles Source # 

Methods

return :: a -> pm inv inv a Source #

(>>=) :: pm pre interm t -> (t -> pm interm post t') -> pm pre post t' Source #

PMonad * State Source # 

Methods

return :: a -> pm inv inv a Source #

(>>=) :: pm pre interm t -> (t -> pm interm post t') -> pm pre post t' Source #

(>>) :: PMonad pm => pm pre mid t -> pm mid post t' -> pm pre post t' Source #

ifThenElse :: Bool -> a -> a -> a Source #

fail :: String -> m inv inv a Source #