[louthy]

`Maybe a` is a type:

For a start it's a discriminated union (a sum type), its set of values is:

    a + 1

`a` is the values in the `Just` case, and 1 is the `Nothing` case. It's obvious why they're called sum-types when you view it like this.

`Maybe a` is a type-lambda abstraction (still a type)

`Maybe Int` is a type-application, passing Int to the `Maybe a` type-lambda as an argument, to get a `Maybe Int` in return (still a type).

[lkitching]

> `Maybe a` is a type-lambda abstraction (still a type)

I don't know what you mean by this - lambdas are values not types. You could argue the type of the Maybe type constructor is Type -> Type but there is no Type type in Haskell so Maybe is not a 'type' in the Haskell type system in the way e.g. String is. The separation of types and values is AFAIK the defining characteristic of non-dependent type systems, which Haskell is (for now).

[philh]

> I don't know what you mean by this - lambdas are values not types.

I think they meant "`Maybe` is a type-lambda abstraction", meaning roughly "a type-level function", which seems true to me. I don't think they meant to say that `Maybe` is a type in the same way String is. (I'd agree it's not, though I'd still call it a type.)

> there is no Type type in Haskell

Incidentally there is[1], and it even has kind `Type` just like `String` does. So you can ask "what is the kind of `Maybe Type`" (it's `Type`) where you can't ask "what is the kind of `Maybe Maybe`" (`Maybe` has kind `Type -> Type` so this is a kind error).

[1]: https://hackage.haskell.org/package/base-4.15.0.0/docs/Data-...