Should Haskell be rebranded away from "Pure Functional Programming"

[atravers]

@tomjaguarpaw

Could you describe in more detail how to apply this to

recipe :: FilePath -> IO String
recipe path = do
   b <- someCondition path
   if b then someFunction path else pure ""

main :: IO ()
main = recipe someFilePath

For example, what does evaluating main entail?

What a surprise: it’s a question about I/O in Haskell - I’m assuming none of these helped. Let’s try something different and see how Agda performs I/O:

4 Compiling Agda programs

This section deals with the topic of getting Agda programs to interact with the real world. Type checking Agda programs requires evaluating arbitrary terms, ans as long as all terms are pure and normalizing this is not a problem, but what happens when we introduce side effects? Clearly, we don’t want side effects to happen at compile time. Another question is what primitives the language should provide for constructing side effecing programs. In Agda, these problems are solved by allowing arbitrary Haskell functions to be imported as axioms. At compile time, these imported functions have no reduction behaviour, only at run time is the Haskell function executed.

Dependently Typed Programming in Agda, Ulf Norell and James Chapman (emphasis added).

Haskell 2010 almost permits a similar "outsourcing" of I/O:

-- the I/O ADT...
data IO a
foreign import "primUnitIO" unitIO :: a -> IO a
foreign import "primBindIO" bindIO :: IO a -> (a -> IO b) -> IO b

instance Monad IO where
    return  = unitIO 
    (>>=)   = bindIO 

Main.main can be dealt with in similar fashion, so:

module Main(main) where

main :: IO ()
        ⋮

would be translated into:

module Main() where
foreign export "hs_Main_main" main :: IO ()

main :: IO ()
        ⋮

So after all that, what does evaluating main entail?

{- Haskell I/O outsourced: nothing to see here... -}

…just as Agda outsources I/O - and not a real faux world in sight! It just requires some FFI extensions. It would also help to make abundantly clear that the monadic interface is actually relatively boring e.g:

 -- "alternate" I/O ADT!
data IO a
type Await a = IO a -> a
foreign import "primAsyncIO" asyncIO :: ((forall a . Await a) -> b) -> IO b

instance Monad IO where
    return x = asyncIO $ \ await -> x
    m >>= k  = asyncIO $ \ await -> let !x = await m in
                                    let !y = await (k x) in
                                    y