Home > Net >  Haskell: a return before is cancelled out by a monad after. How?
Haskell: a return before is cancelled out by a monad after. How?

Time:09-25

How do I understand the statement return 1 getLine? It passes type-checking, and seems identical to 1. How are getLine and return "cancelling" each other out? It doesn't make sense to me at all.

Prelude> :t return 1
return 1 :: (Monad m, Num a) => m a

Prelude> :t return 1 getLine            -- why is it not a type error?
return 1 getLine :: Num t => t          

Prelude> return 1 getLine               
1                                       -- whatever happened to getLine?

Also, how come the end product is "pure" even though it involves a getLine?

CodePudding user response:

If you write return 1 getLine, that means that return 1 should be a function that takes getLine as parameter.

We are lucky, because there is an instance for Monad with a function ((->) r) [src]. Indeed:

-- | @since 2.01
instance Applicative ((->) r) where
    pure = const
    (<*>) f g x = f x (g x)
    liftA2 q f g x = q (f x) (g x)

-- | @since 2.01
instance Monad ((->) r) where
    f >>= k = \ r -> k (f r) r

(->) r is a more canonical form for r -> …. It is thus a function with r as parameter type, and if applied to a type parameter a for example, then ((->) r) a is equivalent to r -> a.

For this instance of Monad, return has the same implementation as pure which is const. This thus means that:

return 1 getLine

is equivalent to:

   const 1 getLine
→ (\_ -> 1) getLine
→ 1

CodePudding user response:

By first noticing that return 1 getLine is (return 1) getLine.

This means that return 1 is a function, since it accepts an additional argument, and functions are monadic values too (that's why it's not a type error).

Thus we must unify

return :: Monad m => a -> m a
return 1 :: (Num a , Monad m) => m a
return 1 ::  Num a           => r -> a

so that m a ~ r -> a and thus m ~ (->) r. For functions, return = const and so we have

return 1 getline 
= const 1 getline 
= const 1 undefined
= 1

because const is defined as

const :: a -> b -> a
const    x    y =  x

(and that's how getLine gets ignored).


In general, the functions Monad instance is defined so that

do { a <- f ; b <- foo a ; return (bar a b) } x

is the same as

let { a = f x ; b = foo a x } in bar a b  -- const (bar a b) x

And that's the reason for return being defined as const.

This means that return and getLine do not "cancel each other out". That's the doing of return only, by virtue of being applied to a second argument, whatever that is, even one which is undefined.

So getLine belonging to the IO "monad", as you write in the question, is irrelevant. Everything is a value in Haskell, and getLine is just another value as well. And it is a pure value at that; it just describes an "impure" I/O action, but by itself it is just another value, simply used as an argument here. Only when getLine appears in main in an appropriate position (or in other code that appears in main, recursively) is it "run", i.e. the computation it describes is actually performed. Here this is not the case.

The monad in play here is the functions monad, to which this return belongs.


As to the purity question, monads are not pure or impure themselves. A type which implements a Monad can be either pure or impure. Functions happen to be pure.

What Monads do is separate the pure from the potentially impure.

But that's actually what Functors do as well. Monads, specifically, allow then for the intermingling chaining of the pure--impure--pure--impure--.... bits, while preserving their separation (again, the "impure" bits can actually be pure themselves as well; the important thing is the separation between the two).

  • Related