How to make this alternative definition of Maybe work?

Question

I hvae just invended the following alternative definition of Maybe:

type Maybe' a = forall b. (b -> (a -> b) -> b)

just :: a -> Maybe' a
just a = \d f -> f a

nothing :: Maybe' a
nothing = const

bind :: Maybe' a -> (a -> Maybe' b) -> Maybe' b
bind ma f = ma nothing (\a -> f a)

The problem is I can't add the following instance declaration

instance Monad (Maybe') where
    return = just
    a >>= f = bind a f

The error message is :

Type synonym Maybe' should have 1 argument, but has been given none

Are there any way to fix?

Answer 1

You can only make it an instance of Monad if you wrap it in a newtype. You also have to use the PolymorphicComponents extension (a weaker form of RankNTypes) to universally quantify the b:

{-# LANGUAGE PolymorphicComponents #-}

newtype Maybe' a = Maybe' { unMaybe' :: forall b. (b -> (a -> b) -> b) }

just :: a -> Maybe' a
just a = Maybe' (\d f -> f a)

nothing :: Maybe' a
nothing = Maybe' const

bind :: Maybe' a -> (a -> Maybe' b) -> Maybe' b
bind ma f = Maybe' (unMaybe' ma const (\a -> unMaybe' (f a)))

instance Monad Maybe' where
    return = just
    (>>=)  = bind

The reason you need a newtype is that Haskell type synonyms do not "stick". When Haskell tries to match the type signature of Maybe' without the newtype against the Monad type class, it does not see the Maybe' at all and instead sees the raw underlying function type.

Haskell uses "principal types" to ensure that every type has a normal form. The normal form of the underlying function is:

(->) b ((->) ((->) a b) b)

Type synonyms do not change the normal form of a type, but newtypes do. Specifically, the newtype in this case is rearranging the type so that the normal form now has the a as the very last type parameter like the Monad instance requires.

Answer 2

Type synonyms are not types. With newtype you get a * -> * type, and with type synonyms you don't. So your question is now reduced to why type synonyms are not first class.

The answer is probably because first class synonyms would create too many ambiguities and make type inference impossible in simple cases.

type First a b = (a, b)
type Second a b = (b, a)
type Both a = (a, a)

If we can define Functor (First a), Functor (Second a) and Functor (Both a) instances, then fmap (+1) (2, 3) would be ambigous.

Your invention, BTW, is called Church encoding. It's possible to Church-encode anything. See https://gist.github.com/rampion/2176199 for implementation of few Church encodings in Haskell (pairs, Maybe and lists).