What is the difference between Either a and Either Int? What is Either a ? A polymorphic type constructor? What is its purpose?

Question

Introduction:

I understand the difference between Maybe a and Maybe Int, I also understand the difference between Either a b and Either Int Int. I also understand that Either Int is the same kind of animal as Maybe, they both take a type as an argument and produce a new type i.e. they are both type constructors that take a single type as parameter (either concrete like Int or not concrete like a) and produce either a concrete type or polymorphic type.

Now what I don't understand is what kind of construct is Either a ? It is not like Maybe because it can never produce a concrete (read not polymorphic) type if we feed a concrete type (like Int) to it. So in this case is it correct to call Either a a polymorphic type constructor and call Maybe a concrete type constructor ? ( This is just how I call them, what are their official name in the Haskell nomenclature?)

Furthermore, I don't know what is the official categorization within the Haskell type system of type constructors like Either a because it cannot be in the same kind of category as Maybe because - as mentioned in the previous paragraph - no matter to what type we apply Either a the resulting type never will be a concrete type, i.e. it will always be a polymorhic type, for example, Either a Int.

The reason why I am asking this is because Either a is a Functor. Which starts to get confusing. Nothing like anything I've seen before. I don't know how should I conceptually interpret the fact that Either a ( a polymorphic type constructor ) is an instance of Functor? Similarly, (->) r (which is also the same kind of animal as Either a) is a Functor too.

Questions:

What are Either a and (->) r ?

What are they called officially?

How do they conceptually fit into the type system of Haskell ?

Where are these polymorphic type constructors described / discussed in more detail?

What whould I read about so I get a better understanding of them?

Should I read about kinds? Are kinds the secret way towards understanding such polymorphic type constructors as Either a and (->) r?

Is Either a Int the same kind of animal as [a] ?

Is the only purpose of Either a Int to declare polymorphic input and output types for functions, just like in the case of [a] in fmap :: (a -> b) -> [a] -> [b]?

Most important question:

How should I interpret the following code in the light of the above described thoughts?

instance Functor (Either a) where 
  fmap f (Right x) = Right (f x) 
  fmap f (Left x) = Left x

class Functor f where 
  fmap :: (a -> b) -> f a -> f b

So the resulting fmap function (whose type is fmap :: (a -> b) -> Either c a -> Either c b) will be polymorphic in c ?

Is this the only effect of making Either a an instance of Functor? So that the resulting fmap function will be polymorphic in c ?

As compared to, for example, making Either Int an instance of Functor?

Then the resulting fmap would work only on Either Int a types but would not work generally/polymorphically on all Either a b types?

If I understand correctly is this the only point and purpose of having polymorphic type constructors like Either a ? So that fmap works on all Either a b types?

I am confused and I am not sure if I am interpreting Either a correctly. Could someone please comfirm that 1) either my interpretation is correct 2) if not then please enlighten me.

Thanks for reading.

Answer 1

There's not really any such thing as Either a. Like polymorphic functions, polymorphic instances should be read system-F style with universal quantification:

forall a . instance Functor (Either a) where ...

The functor instance itself is a dictionary, i.e. type-level function

functor = Λf -> { Λa b -> (a->b) -> f a->f b }

So the either instance would be something like

eitherFunctor = Λa -> functor (Either a)

Alternatively you can think about it as if the compiler replaced instance Functor (Either a) with tons of discrete instances

instance Functor (Either ()) where ...
instance Functor (Either Int) where ...
...
instance Functor (Either (Either Int String)) where ...
...

Though it would obviously not be possible to do that, literally.

Answer 2

Maybe is not a type. Maybe Int is a type. But Maybe, on its own, is something you can make a type out of. It is a type constructor function.

Either is not a type, it is a type constructor. You know how you can curry Haskell functions? Well, you can curry type constructor functions too. So Either is a 2-argument type constructor function, but Either Int is a 1-argument type constructor. And Either Int Bool is an actual type.

The Functor type-class is a higher-kinded type-class. Something like Show applies to a type; Functor applies to a type constructor. For example, you do not write

instance Functor (Maybe Int) where ...

Instead, you write

instance Functor (Maybe) where ...

The definition of Functor is

class Functor f where
  fmap :: (x -> y) -> f x -> f y

Here f is not a type, but a 1-argument type constructor function. You give it an argument (such as x or y) to construct a real, usable type.

Values have "types". Things in a type signature have "kinds". A "type" has kind *. A "1-argument type constructor" has kind "* -> *". It basically says how many arguments you have to supply to get an actual type.

In summary, you could write an instance for Functor (Either Int). But then only Int would be allowed; by making it a type variable, you make it more polymorphic.

Notice that if you wanted it so that the second argument to Either was fixed rather than the first one... you can't do that. In a sense, higher-kinded type-classes are a bit of a kludge. It they're simple to understand and they work for the easy cases. Functional Dependencies and Associated Types are two (incompatible) attempts to solve this problem better.

Answer 3

I don't know answers to some of your questions - like, what some things are called officially, or where to read about them, because they look self-evident to me after studying type systems. (This should not be taken as a advice that the only way to get undestanding is to go study dependent type systems.)

Either Int can be declared a Functor, too, but we can express a more general statement, that it doesn't actually matter whether the first argument to Either is Int - therefore, we declare that Either a is a Functor.

In other type systems there is no need to distinguish kinds, instead Either can be treated as a type, too; but in Haskell they are treated separately from types to simplify the type system. Kinds are a way to describe that types have arity and avoid complications with dependent types by only distinguishing arity. So, Either and (->) have arity 2, or kind *->*->*.

Either a Int is the same kind of animal as [a] in the sense that their kind is *.

fmap :: (a->b) -> Either c a -> Either c b is polymorphic in c, indeed. The importance of this declaration is that it preserves the c. Of course, the only way this can happen for any type c is when Left x remains untouched.