concrete-type-rant.rst

Why You Should Stop Saying "Concrete Type"!

TL;DR: There is no concrete (hah!) definition of "concrete type", different people are meaning different things by those words and assuming everyone else means the same thing.

A Quick Type Primer

There are two separate axes along which we can distinguish types:

1. The kind of the type
2. Whether the type is monomorphic or polymorphic

The kind of a type is, essentially, the "type" of a type. It indicates if and how many argument types it takes and the kinds of those argument types. Values always have types of kind *. Some examples:

Int :: *
Maybe :: * -> *
Either :: * -> * -> *
StateT :: * -> (* -> *) -> *

The term polymorphic consists of two parts:

1. poly, coming from the Ancient Greek πολύς (polús), meaning "many" or "much".
2. morph, coming from the Ancient Greek μορφή (morphḗ), meaning "shape" or "form".

We use polymorph(ic) to refer to types that contain type variables, which can be filled in with multiple possible types, making it "many formed". Monomorphic, (mono, coming from the Ancient Greek μόνος (mónos), meaning "alone", "only", or "single") is the antonym of polymorphic. In other words, it refers to types that have a single shape, i.e., no type variables. Some examples:

Int = monomorphic
Maybe = monomorphic
Maybe a = polymorphic
Maybe Int = monomorphic
Either a String = polymorphic

Why All This Is Ambiguous

In my time in #haskell I've seen people using the term "concrete type" to mean all of the following:

1. Type of kind *
2. Any monomorphic type
3. Any monomorphic type of kind *

In fact, I've not seen anything close to consensus on which these three is the "right" definition. This means that about half of the discussions involving the term "concrete type" eventually devolves into confusing messes, because no one can agree on what "concrete type" means.

The Simple Solution

Fortunately, there is a solution to this entire terminological mess:

Stop using the fucking term "concrete type" as if it means anything!

After reading this text you should have all the terminology you need to accurately and unambiguously describe what kind of types you mean:

Kind \ Morphity [1]	Monomorphic	Polymorphic	Any Morphity
Kind *	Monomorphic type of kind *	Polymorphic type of kind *	Any type of kind *
Some Kind k	Monomorphic type of kind k	Polymorphic type of kind k	Any type of kind k
Any Kind	Monomorphic type of any kind	Polymorphic type of any kind	Any type of any kind

[1]	I've decided to ad hoc invent the term "morphity" to describe the property of being mono-/polymorph.