How to make this alternative definition possibly work?

Question

I just suggested the following alternative definition of Maybe :

 type Maybe' a = forall b. (b -> (a -> b) -> b) just :: a -> Maybe' a just a = \df -> fa nothing :: Maybe' a nothing = const bind :: Maybe' a -> (a -> Maybe' b) -> Maybe' b bind ma f = ma nothing (\a -> fa) 

The problem is that I cannot add the following instance declaration

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

Error message:

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

Is there any way to fix it?

Answer 1

You can make it an instance of Monad if you wrap it in newtype . You should also use the PolymorphicComponents extension (a weaker form of RankNTypes ) for universal quantification of b :

 {-# LANGUAGE PolymorphicComponents #-} newtype Maybe' a = Maybe' { unMaybe' :: forall b. (b -> (a -> b) -> b) } just :: a -> Maybe' a just a = Maybe' (\df -> fa) nothing :: Maybe' a nothing = Maybe' const bind :: Maybe' a -> (a -> Maybe' b) -> Maybe' b bind ma f = Maybe' (unMaybe' ma const (\a -> unMaybe' (fa))) instance Monad Maybe' where return = just (>>=) = bind 

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

Haskell uses "core types" to ensure that each type has a normal shape. Normal form of the base function:

 (->) b ((->) ((->) ab) b) 

Type synonyms do not change the normal form of a type, but newtypes do. In particular, newtype in this case reorders the type, so that the normal form now has a , since the last parameter of the type is required, for example, for a Monad instance.

Answer 2

Type synonyms are not types. With newtype you get the type * -> * , but with type synonyms you don't. So your question now comes down to why type synonyms aren't first-class.

The answer is probably due to the fact that synonyms of the first class would create too many ambiguities and make type inference impossible in simple cases.

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

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

Your invention, BTW, is called Church Coding . This is possible for Church coding. See https://gist.github.com/rampion/2176199 for implementing several 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 a programmer, not something that actually exists, as the Haskell language says. The only way that Haskell can deal with a type synonym is to “browse” it to see the type on the right side. The options just give you a kind of macro language.

So Maybe' a is exactly equivalent to forall b. (b -> (a -> b) -> b) forall b. (b -> (a -> b) -> b) . It behaves the same as if you wrote forall b. (b -> (a -> b) -> b) forall b. (b -> (a -> b) -> b) . But what is Maybe' its own without an argument? Haskell can't handle it like Maybe' , he will 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 use \a ~> ... as a pseudo-syntax for level-level lambda; an arbitrary function from type to another type. The reason I had to compose the syntax is because Haskell has no syntax for this, and the reason it has no syntax is that it cannot handle fully general level functions.

I'm not sure if supporting level-level lambdas types (type constructors and type families are actually very limited forms of this) would be virtually impossible, but it is certainly very difficult. Thus, type synonyms cannot be partially applied.

To get something that a Monad instance can do (which requires something that can be applied to the type to make the type something like * -> * ), you need to use data or newtype to create the type constructor. A type synonym cannot be used for this purpose.