Does <- implicitly coerce types in a Haskell do block?

6
votes

My question relates to the answer to another question: https://stackoverflow.com/a/11766789/3212958

In his answer, ertes writes the following type signature

select :: [a] -> [(a, [a])]

However, when select is actually used, ertes writes the following inside of a do block

(y, ys) <- select xs

Please help me shed some light on how the tuple (y, ys) matches the return type of select, namely [(a, [a])]. Is Haskell coercing the types at some point? (Does Haskell ever coerce types?) Is <- extracting a tuple of type (a, [a]) from the list monad that select returns?

Thanks, Max

--- EDIT: ---

@Lee reminds newbs to desugar before trying to reason about types. After making >>= explicit, it's more clear what's going on. After desugaring, the function in question looks like:

select xs >>= \(y, ys) -> fmap (y:) (perms (n - 1) ys)

And for lists, xs >>= f = concat (map f xs). So a better reading of (y, ys) in this context is as the signature of the function to map over the list.

2
haskelltypesmonads
select returns a list. If you write a <- select xs then a is every element of select xs. If you later write func a, the result of that is the result of applying func to every element of select xs. This is just how the list monad is defined. a <- select xs; func a is the same as select xs >>= func. Bind for lists is defined as : m >>= f = concat (map f m), so you are writing map func (select xs). There is no type coercion in haskell. - user2407038
@user2407038 some slight technicality here; a is not 'every element', a represents one (arbitrary but specific) element of the list. - Justin L.

2 Answers

13
votes

In do notation,

do x1 <- action1
   action2

is translated into action1 >>= \x1 -> action2

This means that if action1 has type m a for some monad m, then x1 has type a. It's not really coercing types, but rather 'unpacking' the value from the monadic action action1 and binding it to x1.

4
votes

(y, ys) is of type (b, c)

The return type of select is of type [(a, [a])]

In <- the types are actually d and Monad m => m d. So we can write the following type equalities:

(b, c) ~ d
[(a, [a])] ~ Monad m => m d

Solving is easy. First substitute d from first equation into second equation:

[(a, [a])] ~ Monad m => m (b, c)

Now to see what's going on I will use a prefix form of [] type constructor (it's not valid haskell but you should get the idea):

[] (a, [a]) ~ Monad m => m ( b, c)

So 

m ~ []
(a, [a]) ~ (b, c)

At this point the compiler checks that instance Monad [a] exists. The rest is easy:

a ~ b
[a] ~ c