`Either`

is standard Haskell datatype defined by

data Either a b = Left a | Right b

Let's define Either monad as follows:

instance Monad (Either a) where return = Right x >>= f = case x of Left _ -> x Right r -> f r

This means we fix the type of `Left`

part and consider `Either a`

as monadic constructor of kind `* -> *`

. Binding operator has the following sense: the function transforms data if it's `Right`

and leaves it unchanged if it's `Left`

(it's similar to `Maybe`

monad, `Right`

corresponding to `Just`

and `Left`

corresponding to `Nothing`

).

Now the puzzle itself. 1) Why the above code won't typecheck and 2) how to make it valid with minimal changes?

The answer on the first question was obvious for me, and I thank `#haskell`

ers for giving me solution to the second.

## 7 comments:

let me guess...

Left a -> Left a

?

Correct :)

I kind of thought it was going to be Left a -> Left a, probably because of the way Left _ would behave on Left undefined, however, I'm not sure exactly why this does not typecheck and Left a -> Left a does, anyone care to elaborate?

Bonus, I think it has to do with the unification algorithm.

(>>=) :: m a -> (a -> m b) -> m b

The type checker has already determined that the variable 'x' is of type 'm a', or 'Either l a', and we need to return an 'm b' or 'Either l b'. So we need to recreate the Left so we get a fresh variable to type check against.

A long-winded explanation:

Just infer a type for (>>=):

Either a b1 -> (b1 -> Either a b2) -> Either a b2

So types don't much:

Either a b1 /= Either a b2

So (>>=) may not return its first argument. But you can construct 'Either a b2' from 'a'.

I know you said "minimal changes", but I prefer the pattern match (which also does type check):

instance Monad (Either a) where

return = Right

Left x >>= _ = Left x

Right y >>= f = f y

Yet another take on why it seems like it should work, and yet doesn't: a value |Left a| is of type |Either a b| where |b| is a phantom type. Given this, it would be nice to have the value be typed as |forall b. Either a b| so that we can freely cast the phantoms around[1]. However, in Haskell's type system we can't do this, so we need to deconstruct and reconstruct the Either value in order to change the phantom.

[1] As I've discussed here: http://winterkoninkje.livejournal.com/56979.html One thing that should be borne in mind about that post, is that it is prudent to distinguish these refinement phantom types from true phantom types ---which we don't want to freely cast, since they carry semantic information.

Post a Comment