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?

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`. — Robin Zigmond, Oct 09 '20 at 14:08
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. — Gertjan Brouwer, Oct 09 '20 at 14:09
@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? — Gertjan Brouwer, Oct 09 '20 at 14:13
`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. — Robin Zigmond, Oct 09 '20 at 14:20
PS your title is strange as the question has nothing to do with referential transparency. — Robin Zigmond, Oct 09 '20 at 14:20
@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 — Gertjan Brouwer, Oct 09 '20 at 14:22
@RobinZigmond if it is Monad m where m ~ []. Shouldn't the return type of function 1 be different then? — Gertjan Brouwer, Oct 09 '20 at 14:23
see https://stackoverflow.com/tags/do-notation/info and the answer linked from there. — Will Ness, Oct 22 '20 at 20:03
also [this](https://stackoverflow.com/a/44728131/849891), search for "axiomatically". — Will Ness, Oct 23 '20 at 12:12

Sri Kadimisetty · Accepted Answer · 2020-12-26T07:15:40.453

12

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.

edited Dec 26 '20 at 07:15

answered Oct 09 '20 at 14:17

Sri Kadimisetty

1,804
4
23
25

Then why would it work if I changed it to `return (show x)` ? – Gertjan Brouwer Oct 09 '20 at 14:19
@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. – Sri Kadimisetty Oct 09 '20 at 14:25
I should have left out the type indeed, it is a copy paste error. The type in that case becomes an IO String. – Gertjan Brouwer Oct 09 '20 at 14:28
@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`. – Sri Kadimisetty Oct 09 '20 at 14:32
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 – Gertjan Brouwer Oct 09 '20 at 14:34
It doesn't "extract" `True` so much. What it really does is basically produce `[[True]]` and flatten that to get `[True]`. – dfeuer Oct 09 '20 at 14:39
@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. – Sri Kadimisetty Oct 09 '20 at 14:42
But return is of type Monad a => b -> a b. So why is then function 1 not of type a String? – Gertjan Brouwer Oct 09 '20 at 14:54
@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]`. – luqui Oct 09 '20 at 15:07
1

@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! – Sri Kadimisetty Oct 09 '20 at 15:09
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? – Gertjan Brouwer Oct 09 '20 at 15:10
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. – Sri Kadimisetty Oct 09 '20 at 15:12
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? – Gertjan Brouwer Oct 09 '20 at 15:14
1

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. – Sri Kadimisetty Oct 09 '20 at 15:17
Yeh some compiler trickery then. This post explained it well: https://stackoverflow.com/questions/27932794/what-is-the-type-of-return-5-in-haskell-when-no-context-is-given – Gertjan Brouwer Oct 09 '20 at 15:19
1

type inference is not "guessing" though. – Will Ness Oct 23 '20 at 12:02
@WillNess you are correct. I was doing my best to not mention words like inference etc. that might distract a potentially confused beginner. – Sri Kadimisetty Oct 25 '20 at 04:47
1

we could say "derive" or "determine". – Will Ness Oct 25 '20 at 14:37

score 9 · Answer 2 · answered Oct 09 '20 at 14:59

9

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.

answered Oct 09 '20 at 14:59

dfeuer

48,079
5
63
167

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? – Gertjan Brouwer Oct 09 '20 at 15:09
1

@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. – dfeuer Oct 09 '20 at 15:34
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 – Gertjan Brouwer Oct 09 '20 at 17:09

Inconsistent do notation in functions

2 Answers2