> There's something fundamental I'm missing.
It is not necessarily true, but useful, to think that:
- A type is a set of values.
- A kind as a set of types.
- The kind * is the set of all types.
- The kind * -> * is the set of every function with domain * and codomain *.
- The type T -> U is the set of every function with domain T and codomain U, if each of T and U is a type (a set of values).
For example:
- The type Bool is the set {False, True}.
- The type Maybe Bool is the set {Nothing, Just False, Just True}.
- Maybe is a function such that Maybe(T) = { Nothing } union { Just t | t in T }.
- Maybe is not a type; Maybe Bool is a type.
- a -> a is the set { \ x -> x }.
Currying and application can happen at both the value level and the type level:
- The kind of Either is * -> * -> *.
- The kind of Either a is * -> *, if the kind of a is *.
- The kind of Either a b is *, if the kind of a is * and the kind of b is *.
- The type of Just is a -> Maybe a.
- The type of Just x is Maybe a, if the type of x is a.
> Why is it giving two separate treatments?
It is to show the various ways one can implement/represent/realize/concretize/encode/model a mathematical construction in Haskell.
You can (do type-level programming in Haskell, use all features of C++, eat spaghetti with a straw, etc.), but the real question has always been: should you?
> If anyone knows of a really thorough and definitive and understandable treatment of Haskell types, I'd appreciate it.
If you mean Haskell 98, then the Haskell 98 Report [1] (especially Chapter 4) seems "thorough and definitive", but I don't know whether you will find it "understandable".
If you mean the latest Haskell as implemented by GHC, I don't know.