Inconsistent do notation in functions

Question

Why is this function allowed:

-- function 1
myfunc :: String
myfunc = do
  x <- (return True)
  show x

and this is not:

-- function 2
myfunc :: String
myfunc = do
  x <- getLine
  show x

The compile error:

Couldn't match type `[]' with `IO'
Expected type: IO Char
Actual type: String

I get why function 2 shouldn't work, but why then thus function 1 work?

and why does this then work:

-- function 3
myfunc = do
  x <- getLine
  return (show x)

I get that it returns IO String then, but why is function 1 also not forced to do this?

Head

What is the error message? – Delsiedelsman

I added the compilation error @RobertHarvey – Head

Because show x is a String, which is the same as [Char], so the types all match up when the do block is in the List Monad. Whereas that option isn't available in the second one, since the use of getLine forces the Monad to be IO. – Elongation

Not in this case. x <- (return True) wouldn't compile since then you essentially are saying this: (return True) >>= (\x -> _) thus a lamba without a body which is not allowed. – Head

@RobinZigmond I still don't really understand. What I thought was happening is that the return True is of type IO String or IO [char] if you will. Is that not the case then? – Head

return True has type (Monad m) => m Bool. GHC will, if possible, infer which Monad m makes sense in context. When the return type is String then only m ~ [] can ever work. – Elongation

PS your title is strange as the question has nothing to do with referential transparency. – Elongation

@RobinZigmond the title is this way primarily because I think that function 1 is not referentially transparent. It of course is, but I don't see how. Since I can get a String type out of a function that uses a do-block – Head

@RobinZigmond if it is Monad m where m ~ []. Shouldn't the return type of function 1 be different then? – Head

see stackoverflow.com/tags/do-notation/info and the answer linked from there. – Saintpierre

also this, search for "axiomatically". – Saintpierre

Answer 1

In function1 the do block in myfunc is working in the list monad, because String is really just [Char]. In there, return True just creates [True]. When you do x <- return True that "extracts" True out of [True] and binds it to x. The next line show x converts True into a String "True". which being the return value the compiler value expects to see, ends up working fine.

Meanwhile in function2, the do block in myfunc is also working on the list monad (for the same reason, String being really [Char]) but calls on getLine which is only available in the IO monad. So unsurprisingly, this fails.

-- EDIT 1

OP has added a function3

-- function 3
myfunc :: String
myfunc = do
  x <- getLine
  return (show x)

No this should not work for the same reason function2 fails.

-- EDIT 2

OP has updated function3 to fix a copy paste error.

-- function 3
myfunc = do
  x <- getLine
  return (show x)

This is mentioned in the comments, but for clarity sake, this works because, when the type information is unspecified, GHC makes it best inference and after seeing getLine, it figures it’s IO String which does provide getLine.

Note - I wrote this answer with as casual a tone as I could manage without being wrong with the intention of making it approachable to a beginner level.

Discernment

Then why would it work if I changed it to return (show x) ? – Head

@GertjanBrouwer Unless I'm missing something, that shouldn't work from what you have given us- as getLine should not be available otherwise. Do recheck your code structure again. – Discernment

I should have left out the type indeed, it is a copy paste error. The type in that case becomes an IO String. – Head

@GertjanBrouwer Ah I see. Yes if you leave out the type, GHC infers the type for you. It saw getLine and inferred that you were working on IO String. – Discernment

I think I figured it out now. I was thinking function 1 would not be referentially transparent. But this is of course only applicable to IO types. I was thinking x <- (return True) would be of that type. But apparently it somehow is not, still not sure why tho – Head

It doesn't "extract" True so much. What it really does is basically produce [[True]] and flatten that to get [True]. – Kobi

@GertjanBrouwer This might not be related to referential transparency. Perhaps you're confusion is more about how return True works in a function that has nothing to do with IO? If so that is because, String being a synonym for [Char] is really just a list; so now you're working inside a list monad. Within this list monads's do block, a return True just creates a list with True in it. – Discernment

But return is of type Monad a => b -> a b. So why is then function 1 not of type a String? – Head

@GertjanBrouwer because b is Bool. a is [] in this case (because of the last line of the do block is a String = [Char] = [] Char, forcing the monad to be []). So return True has type [Bool]. – Candycecandystriped

@GertjanBrouwer In the first line of function1, return True is definitely not String. However remember, we are still within the List monad here (String really being [Char]). So the b -> ab part in return's type would look like something like this in the List monad - b -> [b]. So here, return does True -> [True]. So you could pretty much rewrite that line as x <- [True] which eventually results in x bound to True. Obviously True is not a String, but your next line did show True which creates the string "True". Hope that explanation cleared it up for ya! – Discernment

So the compiler is essentially looking from the end of the function? It sees that show x is used so it infers that Monad [] should be the previous type? – Head

Since you explicitly set function1's return type as String, the compiler doesn't need to infer at all and will expect to see a String as the return value at the end of the do block here. – Discernment

I see, but I can omit the type signature and it still gets the right type. How does that process work in this case? Since the type True has nothing to do with List. I assume it looks at the last part first? – Head

Yes, if you omit the type signature, GHC will infer one based on the function definition. It is generally advised to not assume that GHC will end up inferring what you want, so when possible be explicit with the type signature. About your 2nd question, yes "the last part" being the the return value is one way of looking at it. – Discernment

Yeh some compiler trickery then. This post explained it well: #27933294 – Head

type inference is not "guessing" though. – Saintpierre

@WillNess you are correct. I was doing my best to not mention words like inference etc. that might distract a potentially confused beginner. – Discernment

we could say "derive" or "determine". – Saintpierre

Answer 2

do blocks work in the context of an arbitrary Monad. The Monad, in this case, is []. The Monad instance for lists is based on list comprehensions:

instance Monad [] where
  return x = [x]
  xs >>= f = [y | x <- xs, y <- f x]

You can desugar the do notation thus:

myfunc :: String
myfunc = do
  x <- (return True)
  show x

-- ==>

myfunc = [y | x <- return True, y <- show x]

-- ==>

myfunc = [y | x <- [True], y <- show x]

In a list comprehension, x <- [True] is really just the same as let x = True, because you're only drawing one element from the list. So

myfunc = [y | y <- show True]

Of course, "the list of all y such that y is in show True" is just show True.

Kobi

Yes this is exactly what I was looking for. The only thing confusing about this is the use of Monad []. Since I say return True I would assume it would be Monad Bool(don't know if it exists) instead of Monad []. Does the compiler do some trickery or is there is simple explanation for that too? – Head

@GertjanBrouwer, no trickery. Just look more carefully at the type of return. Monad is what's sometimes called a "constructor class", because its argument is a type constructor rather than a base type. – Kobi

Yeh I think it is clear now. Return did Monad m => a -> m a so then the Monad type [] is used which is then returned. I was completly confused, but turns out [] is just a Monad and string is just [char] so it all works out! Thanks a lot – Head