[Haskell-cafe] Practical Haskell question.

[Arie Peterson]

As others have explained, you can't analyse your do-constructs, because
functions are opaque -- at the value level.

The canonical option would indeed seem to be to use arrows (or applicative
functors), instead of monads.

------

If you want to stick to monads, there is another possibility: carry around
the necessary checks *at the type level*. Below is a sketch of how you
could do this.

Things to note:

- Uses HList <http://homepages.cwi.nl/~ralf/HList/>.

- Deciding which checks to perform happens statically, so it will check
for any actions that are mentioned, even if they are not actually
performed:

  actionX >>= \ b -> if b then actionY else actionZ

will perform checks necessary for actionZ, even if actionX happens to
return True.

- First draft; may contain sharp edges (or outright errors). There are
some possibilities for generalisation: e.g. do it over an arbitrary monad,
instead of IO.

------8<------

module CheckIO where


import Control.Monad.Error
import HList
  (
    (:*:)
  , (.*.)
  , HNil
      (
        HNil
      )
  , HOccurs
  )


data CheckIO labels x
  = CheckIO (IO x)

instance Monad (CheckIO l) where
  return = CheckIO . return
  (CheckIO a) >>= h = CheckIO $ a >>= ((\ (CheckIO x) -> x) . h)
  fail = CheckIO . fail

instance Functor (CheckIO l) where
  fmap f (CheckIO a) = CheckIO (fmap f a)

withCheck :: (HOccurs label labels) => IO x -> label -> CheckIO labels x
withCheck = flip (const CheckIO)


class Check label where
  check :: label -> ErrorT String IO () -- |label| argument is for type
inference only

class Checks c where
  performChecks :: c -> ErrorT String IO () -- |c| argument is for type
inference only

instance Checks HNil where
  performChecks _ = return ()

instance (Check label,Checks rest) => Checks (label :*: rest) where
  performChecks _ = check (undefined :: label) >> performChecks (undefined
:: rest)

runWithChecks :: forall labels x. (Checks labels) => CheckIO labels x ->
labels -> ErrorT String IO x
runWithChecks (CheckIO q) _ = performChecks (undefined :: labels) >> liftIO q

-- End of general CheckIO code; the following example use would actually
go in a different module.

-- Component actions

data Root
  = Root

instance Check Root where
  check _ = do
    liftIO $ putStrLn "Root privileges required. Enter root password:"
    pw <- liftIO getLine
    if pw == "myRootPassword"
      then return ()
      else throwError "No root."

actionA :: (HOccurs Root labels) => CheckIO labels ()
actionA = putStrLn "Enter a string:" `withCheck` Root


data Database
  = Database

instance Check Database where
  check _ = liftIO $ putStrLn "Database is ok."

actionB :: (HOccurs Database labels) => CheckIO labels String
actionB = getLine `withCheck` Database


data Connection
  = Connection

instance Check Connection where
  check _ = do
    liftIO $ putStrLn "Connection up?"
    x <- liftIO getLine
    if x == "yes"
      then return ()
      else throwError "No connection."

actionC :: (HOccurs Connection labels) => String -> CheckIO labels ()
actionC x = putStrLn (reverse x) `withCheck` Connection

-- Composed action

main :: ErrorT String IO ()
main = action `runWithChecks` (Connection .*. Database .*. Root .*. HNil)

action :: (HOccurs Root labels,HOccurs Connection labels,HOccurs Database
labels) => CheckIO labels ()
action = do
  actionA
  x <- actionB
  actionC x

------>8------


Kind regards,

Arie