Clarification of Terms around Haskell Type system

Type system in haskell seem to be very Important and I wanted to clarify some terms revolving around haskell type system.

Some type classes
- Functor
- Applicative
- Monad
After using :info I found that Functor is a type class, Applicative is a type class with => (deriving?) Functor and Monad deriving Applicative type class.

I've read that Maybe is a Monad, does that mean Maybe is also Applicative and Functor?
-> operator

When i define a type
```
data Maybe = Just a | Nothing
```
and check :t Just I get Just :: a -> Maybe a. How to read this -> operator?

It confuses me with the function where a -> b means it evaluates a to b (sort of returns a maybe) – I tend to think lhs to rhs association but it turns when defining types?
The term type is used in ambiguous ways, Type, Type Class, Type Constructor, Concrete Type etc... I would like to know what they mean to be exact

Solution

Indeed the word “type” is used in somewhat ambiguous ways.

The perhaps most practical way to look at it is that a type is just a set of values. For example, Bool is the finite set containing the values True and False.
Mathematically, there are subtle differences between the concepts of set and type, but they aren't really important for a programmer to worry about. But you should in general consider the sets to be infinite, for example Integer contains arbitrarily big numbers.

The most obvious way to define a type is with a data declaration, which in the simplest case just lists all the values:

data Colour = Red | Green | Blue

There we have a type which, as a set, contains three values.

Concrete type is basically what we say to make it clear that we mean the above: a particular type that corresponds to a set of values. Bool is a concrete type, that can easily be understood as a data definition, but also String, Maybe Integer and Double -> IO String are concrete types, though they don't correspond to any single data declaration.

What a concrete type can't have is type variables^†, nor can it be an incompletely applied type constructor. For example, Maybe is not a concrete type.

So what is a type constructor? It's the type-level analogue to value constructors. What we mean mathematically by “constructor” in Haskell is an injective function, i.e. a function f where if you're given f(x) you can clearly identify what was x. Furthermore, any different constructors are assumed to have disjoint ranges, which means you can also identify f.^‡

Just is an example of a value constructor, but it complicates the discussion that it also has a type parameter. Let's consider a simplified version:

data MaybeInt = JustI Int | NothingI

Now we have

JustI :: Int -> MaybeInt

That's how JustI is a function. Like any function of the same signature, it can be applied to argument values of the right type, like, you can write JustI 5.
What it means for this function to be injective is that I can define a variable, say,

quoxy :: MaybeInt
quoxy = JustI 9328

and then I can pattern match with the JustI constructor:

> case quoxy of { JustI n -> print n }
9328

This would not be possible with a general function of the same signature:

foo :: Int -> MaybeInt
foo i = JustI $ negate i


> case quoxy of { foo n -> print n }
<interactive>:5:17: error: Parse error in pattern: foo

Note that constructors can be nullary, in which case the injective property is meaningless because there is no contained data / arguments of the injective function. Nothing and True are examples of nullary constructors.

Type constructors are the same idea as value constructors: type-level functions that can be pattern-matched. Any type-name defined with data is a type constructor, for example Bool, Colour and Maybe are all type constructors. Bool and Colour are nullary, but Maybe is a unary type constructor: it takes a type argument and only the result is then a concrete type.

So unlike value-level functions, type-level functions are kind of by default type constructors. There are also type-level functions that aren't constructors, but they require -XTypeFamilies.

A type class may be understood as a set of types, in the same vein as a type can be seen as a set of values. This is not quite accurate, it's closer to true to say a class is a set of type constructors but again it's not as useful to ponder the mathematical details – better to look at examples.

There are two main differences between type-as-set-of-values and class-as-set-of-types:

How you define the “elements”: when writing a data declaration, you need to immediately describe what values are allowed. By contrast, a class is defined “empty”, and then the instances are defined later on, possibly in a different module.
How the elements are used. A data type basically enumerates all the values so they can be identified again. Classes meanwhile aren't generally concerned with identifying types, rather they specify properties that the element-types fulfill. These properties come in the form of methods of a class. For example, the instances of the Num class are types that have the property that you can add elements together.

You could say, Haskell is statically typed on the value level (fixed sets of values in each type), but duck-typed on the type level (classes just require that somebody somewhere implements the necessary methods).

A simplified version of the Num example:

class Num a where
  (+) :: a -> a -> a

instance Num Int where
  0 + x = x
  x + y = ...

If the + operator weren't already defined in the prelude, you would now be able to use it with Int numbers. Then later on, perhaps in a different module, you could also make it usable with new, custom number types:

data MyNumberType = BinDigits [Bool]

instance Num MyNumberType where
  BinDigits [] + BinDigits l = BinDigits l
  BinDigits (False:ds) + BinDigits (False:es)
    = BinDigits (False : ...)

Unlike Num, the Functor...Monad type classes are not classes of types, but of 1-ary type constructors. I.e. every functor is a type constructor taking one argument to make it a concrete type. For instance, recall that Maybe is a 1-ary type constructor.

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

instance Functor Maybe where
  fmap f (Just a) = Just (f a)
  fmap _ Nothing = Nothing

As you have concluded yourself, Applicative is a subclass of Functor. D being a subclass of C means basically that D is a subset of the set of type constructors in C. Therefore, yes, if Maybe is an instance of Monad it also is an instance of Functor.

^†_{That's not quite true: if you consider the _universal quantor_ explicitly as part of the type, then a concrete type can contain variables. This is a bit of an advanced subject though.}

^‡_{This is not guaranteed to be true if the -XPatternSynonyms extension is used.}