[philh]

Or Haskell has types like `Void`, `Maybe`, and `Monad`. If you think of them as "sets of possible values", these all have no possible values. But they're very different types.

You could probably define terms such that of these, only `Void` is a "type" - for example, it's the only one that you can use directly as function inputs or outputs. (i.e. you can write a function `Void -> Int` but not a function `Maybe -> Int`.) I think that would be nonstandard, but maybe reasonable to do. But then when you explain what a "type" is you've only explained a subset of what "type theorists" talk about, which includes the others.

[lkitching]

Maybe and Monad are not types - Maybe is a type constructor and Monad is a type class.

[philh]

As I said, I think that's a reasonable but nonstandard way to define the word "type" but it doesn't make much difference - type theory concerns itself with them, whatever they're called.

But to support my "nonstandard" claim:

* https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compil... mentions "Types (possibly of higher kind); e.g. [Int], Maybe"

* https://limperg.de/ghc-extensions/#polykinds talks about "types of different kinds", using Int and Monad as examples.

* https://en.wikipedia.org/wiki/Kind_%28type_theory%29 says "the type [] (list) is a type constructor". It uses the terms "data type" and "proper type" for what I think you simply want to call "type".

It's also possible usage is just inconsistent on the subject. (Evidence for this: that second link calls constraints "type-like things", when they're just types according to me.) But my sense is that usually, people engaging seriously with type theory or advanced Haskell would call Maybe and Monad types.

(You're of course right that Maybe is a type constructor and Monad is a typeclass, but that doesn't mean they aren't also types.)

[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-...