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

Answer 3

Type synonyms cannot be partially applied.

A type synonym is just a short hand to help the programmer, not something that actually exists as something the Haskell language can talk about. The only way Haskell can deal with a type synonym is by "looking through" it to see the type on the right hand side. The parameters just give you a sort of "macro language".

So Maybe' a is exactly equivalent to forall b. (b -> (a -> b) -> b). It behaves just as if you'd written forall b. (b -> (a -> b) -> b) instead. But what is Maybe' on its own without an argument then? Haskell can't deal with it as Maybe', it would have to replace it with something else. But what? If it meant anything, it would have to be something like \a ~> (forall b. (b -> (a -> b) -> b), where I'm using \a ~> ... as pseudo-syntax for a type-level lambda; an arbitrary function from a type to another type. The reason I had to make up syntax for that is because Haskell has no syntax for this, and the reason it has no syntax is because it cannot handle fully general type-level functions.

I'm not certain whether supporting arbitrary type-level lambdas (type constructors and type families are effectively very restricted forms of this) would be actually impossible, but it's certainly very difficult. So type synonyms can't be partially applied.

To get something that can made an instance of Monad (which needs something that can be applied to a type to make a type - something of kind * -> *), you need to use data or newtype to create a type constructor. A type synonym can't be used for this purpose.