How can monads determine ordering if their information is lost upon normalization?

Question

If I understood correctly, a monad is just the implementation of a bind >>= and a return operator following certain rules which basically compose 2 functions of different return types together. So, for example, those are equivalent:

putStrLn "What is your name?"
>>= (\_ -> getLine)
>>= (\name -> putStrLn ("Welcome, " ++ name ++ "!"))

(bind (putStrLn "What is your name?")
      (bind
          (\_ -> getLine)
          (\name -> putStrLn ("Welcome, " ++ name ++ "!"))))

But if we strongly normalize this expression, the final result will be just:

(putStrLn ("Welcome, " ++ getline ++ "!"))

The first statement (putStrLn "What is your name?") is completely lost. Also, getLine looks like a function with no arguments, which is nonsense. So how does this work, and what is the actual definition of the >>= and return functions?

Answer 1

Your logical misstep is that you assume certain reduction rules hold which do not. In particular, you appear to be using

f >>= (\x -> g x)  ====  g f

If that held then, yes, monads would be pretty silly: (>>=) would just be flip ($). But it doesn't, in general, hold at all. In fact, the very reason it doesn't hold is what provides monads an opportunity to be interesting.

---

For a little bit of further exploration, here's the one monad where (>>=) == flip ($) (basically) holds.

newtype Identity a = Identity { unIdentity :: a }

To make our equations work out, we'll have to use that Identity a ~ a. This isn't strictly true, obviously, but let's pretend. In particular, Identity . unIdentity and unIdentity . Identity are both identities, no-ops, and we can freely apply Identity or unIdentity however we like to make types match

instance Functor Identity where
  fmap f (Identity a) = Identity (f a)

instance Monad Identity where
  return a = Identity a          -- this is a no-op
  ida >>= f = f (unIdentity ida)

Now, in particular, we want to examine

ida :: Identity a
f   :: a -> b

ida >>= Identity . f          :: Identity b
===
Identity (f (unIdentity ida)) :: Identity b

and if we throw away the Identity/unIdentity noise and thus produce the knowledge that ida = Identity a for some a

Identity (f (unIdentity ida)) :: Identity b
===
Identity (f a)                :: Identity b
===                              ~
f a                           ::          b

---

So, while (>>=) == flip ($) forms a certain basis of intuition about (>>=)... in any circumstance more interesting than the Identity monad (and all other monads are) it doesn't hold exactly.

Answer 2

Seems to be a misunderstanding of how evaluation in IO proceeds in Haskell. If you look at the type signature for (>>=):

λ: :t (>>=)
(>>=) :: Monad m => m a -> (a -> m b) -> m b

It takes a monadic value parameterized by a type a, and a function which accepts a type of the same type and applies it inside the function body yielding a monadic value of type b.

The IO monad itself is a rather degenerate monad since it has special status in Haskell's implementation. A type of IO a stands for a potentially impure computation which, when performed, does some IO before returning a value of type a.

The first statement (putStrLn "What is your name?") is completely lost.

The misunderstanding about this statement is that the value of putStrLn :: String -> IO () does in fact lose it's value in some sense, or more precisely it just yields the unit type () to the bound function after performing the IO action of printing a string to the outside world.

But if we strongly normalize this expression, the final result will be

just: (putStrLn ("Welcome, " ++ getline ++ "!"))

It's best to think of getLine :: IO String as being a computation yielding a value instead of a value itself. In this case as well the function getLine is not itself substituted in but the result of the computation it performs is, which behaves like you expect it to: getting a value from stdin and printing it back out.

Answer 3

[...] what are the actual definitions for the (>>=) and return functions?

From section 6.1.7 (page 75) of the Haskell 2010 report:

The IO type serves as a tag for operations (actions) that interact with the outside world. The IO type is abstract: no constructors are visible to the user. IO is an instance of the Monad and Functor classes.

the crucial point being:

The IO type is abstract: no constructors are visible to the user.

There are no actual (written in idiomatic Haskell) definitions - it's the implementors' choice as to which model to use: state-threading, continuations, direct effects, etc. (This wasn't always the case - I provide more details here :-) We also benefit, as we're able to choose the most convenient model for the investigation being made.

So how does this work [...]?

I will choose the direct-effect model, based on examples from Philip Wadler's How to Declare an Imperative:

(* page 26, modified *)

type 'a io   = oi -> 'a

infix >>=
val >>=      : 'a io * ('a -> 'b io) -> 'b io
fun m >>= k  = fn Oblige => let
                              val x =   m Oblige
                              val y = k x Oblige
                            in
                              y
                            end

val return   : 'a -> 'a io
fun return x = fn Oblige => x

val putc     : char -> unit io
fun putc c   = fn Oblige => putcML c

val getc     : char io
val getc     = fn Oblige => getcML ()

I'm using a new type:

datatype oi  = Oblige

to reserve the unit type and its value () for the usual purpose of vacuous results, for clarity.

(Yes - that's Standard ML: just imagine it's 1997, and you're writing a prototype Haskell implementation ;-)

With the help of some extra definitions:

val gets     : (char list) io
val putsl    : char list -> unit io

that Haskell code sample, modified slightly:

putStrLn "What is your name?"     >>= 
(\_ -> getLine                    >>=
(\name -> putStrLn (greet name)))

greet      :: String -> String
greet name =  "Welcome, " ++ name ++ "!"

translates to:

putsl "What is your name?"
>>= (fn _    => gets
>>= (fn name => putsl (greet name))

where:

val greet      : char list -> char list
fun greet name = List.concat (String.explode "Welcome, "::name::[#"!"])

All going well, the sample should simplify down to:

fun Oblige => let
                val x    = putsl "What is your name?" Oblige
                val name = gets Oblige
                val y    = putsl (greet name) Oblige
              in
                y
              end

Even though x isn't used it's still evaluated in Standard ML, which causes the prompt "What is your name?" to be displayed.

Now for a guess at the next question...Standard ML and Haskell are both functional languages - could all that oi stuff be transferred across to Haskell?

I was wrong? Meh; I'll answer it anyway - sort of; you can read about what I devised over here. If that was just too abominable to contemplate...well, here are those extra Standard ML definitions:

(* from pages 25-26, verbatim *)

val putcML    : char -> unit
fun putcML c  = TextIO.output1(TextIO.stdOut,c);

val getcML    : unit -> char
fun getcML () = valOf(TextIO.input1(TextIO.stdIn));


(* Caution: work of SML novice... *)

val gets     = fn Oblige => let
                              val c = getc Oblige
                            in
                              if c = #"\n" then
                                []
                              else
                                let
                                  val cs = gets Oblige
                                in
                                  (c::cs)
                                end
                            end

fun putsl cs = fn Oblige => let
                              val _ = putsl cs Oblige
                              val _ = putc #"\n" Oblige
                            in
                              ()
                            end

val puts     : char list -> unit io
fun puts cs  = fn Oblige => case cs of
                              []      => ()
                            | (c::cs) => let val _ = putc c Oblige in
                                         puts cs Oblige

Answer 4

It has been so long til I asked that question! The simple answer is that, no, the term I posted does not reduce to putStrLn ("Welcome, " ++ getline ++ "!"). Instead, its normal form will have the shape bind foo (\ _ -> bind bar (\ _ -> ...)), i.e., a chain of lambdas, which holds the ordering information I was worried about.