Sunday, September 7, 2008

Haskell puzzle: Either monad

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 #haskellers for giving me solution to the second.

7 comments:

e.v.e said...

let me guess...

Left a -> Left a

?

Roman Cheplyaka said...

Correct :)

Bonus said...

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?

Bryan said...

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.

beroal said...

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'.

dino said...

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

wren said...

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.