Alright, let's go one by one.
Values are the concrete pieces of data that programs evaluate and juggle. Nothing fancy, some examples might be
"fizz buzz foo bar"
A nice description for a type is "a classifier for a value". A type is a little bit of information about what that value will be at runtime, but indicated at compile time.
For example if you tell me that
e : bool at compile time, and I'll know that
e is either
false during runtime, nothing else! Because types classify values nicely like this, we can use this information to determine some basic properties of your program.
For example, if I ever see you adding
e : int and
e' : String, then I know something is a bit off! In fact I can flag this and throw an error at compile time, saying "Hey, that doesn't make any sense at all!".
A more powerful type system allows for more interesting types which classify more interesting values. For example, let's consider some function
f = fun x -> x
It's pretty clear that
f : Something -> Something, but what should that
Something be? In a boring type system, we'd have to specify something arbitrary, like
Something = int. In a more flexible type system, we could say
f : forall a. a -> a
That is to say "for any
f maps an
a to an
a". This let's us use
f more generally and write more interesting programs.
Moreover, the compiler is going to check actually satisfying the classifier we've given it, if
f = fun x -> true then we have a bug and the compiler will say so!
So as a tldr; a type is a compile time constraint on the values an expression can be at runtime.
Some types are related. For example a list of integers is very similar to a list of strings. This is almost like how
sort for integers is almost like
sort for strings. We can imagine a sort of factory that builds these almost-the-same types by generalizing over their differences and building them upon demand. That's what a type constructor is. It's kind of like a function from types to types, but a little more limited.
The classic example is a generic list. A type constructor for is just the generic definition
data List a = Cons a (List a) | Nil
List is a function which maps a type
a to a list of values of that type! In Java-land I think these are perhaps called "generic classes"
A type parameter is just the type passed to a type constructor (or function). Just like in the value level we'd say
foo(a) has a parameter
a just like how
List a has a type parameter
Kinds are a bit tricky. The basic idea is that certain types are similar. For example, we have all the primitive types in java
float... which all behave as if they have the same "type". Except, when we're speaking of the classifiers for types themselves, we call the classifiers kinds. So
int : Prim,
String : Box,
List : Boxed -> Boxed.
This system gives nice concrete rules about what sort of types we can use where, just like how types govern values. It'd clearly be nonsense to say
In Java since
List needs to be applied to a concrete type to be used like that! If we look at their kinds
List : Boxed -> Boxed and since
Boxed -> Boxed /= Boxed, the above is a kind error!
Most of the time we don't really think about kinds and just treat them as "common sense", but with fancier type systems it's something important to think about.
A little illustration of what I've been saying so far
value : type : kind : ...
true : bool : Prim : ...
new F() : Foo : Boxed : ...
Better Reading Than Wikipedia
If you're interested in this sort of thing, I'd highly recommend investing a good textbook. Type theory and PLT in general is pretty vast and without a coherent base of knowledge you (or at least I) can wander around without getting anywhere for months.
Two of my favorite books are
- Types and Programming Language - Ben Pierce
- Practical Foundations of Programming Languages - Bob Harper
Both are excellent books that introduce what I've just talked about and much more in beautiful, well explained detail.