According to the basic Wikipedia entry about kinds "a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator". So I understand that to mean the type of a kind is a kind and it's kinds all the way down (which makes sense - otherwise we would need an infinite number of names, one for each meta-type(i)).
From the same reference:
"(* => *) => * is the kind of a higher-order type operator from unary type constructors to proper types. These are very seldom encountered, even in programming language theory, but see Pierce (2002), chapter 32 for an application."
would seem to indicate it has limited but non-zero usefulness.
Not a great answer, but hopefully it will stop the "not a real question" close votes until someone who, say, implemented a Haskell compiler and really knows what he's talking about comes along...
First, the GHC error,
GHC is attempting to unify a few constraints with x
, first, we use it as a function so
x :: a -> b
Next we use it as a value to that function
x :: a
And finally we unify it with the original argument expression so
x :: (a -> b) -> c -> d
Now x x
becomes an attempt to unify t2 -> t1 -> t0
, however, We can't unify this since it would require unifying t2
, the first argument of x
, with x
. Hence our error message.
Next, why not general recursive types. Well the first point worth noting is the difference between equi and iso recursive types,
- equi-recursive are what you'd expect
mu X . Type
is exactly equivalent to expanding or folding it arbitrarily.
- iso-recursive types provide a pair of operators,
fold
and unfold
which fold and unfold the recursive definitions of types.
Now equi-recursive types sound ideal, but are absurdly hard to get right in complex types systems. It can actually make type checking undecidable. I'm not familiar with every detail of OCaml's type system but fully equirecursive types in Haskell can cause the typechecker to loop arbitrarily trying to unify types, by default, Haskell makes sure that type checking terminates. Further more, in Haskell, type synonyms are dumb, the most useful recursive types would be defined like type T = T -> ()
, however are inlined almost immediately in Haskell, but you can't inline a recursive type, it's infinite! Therefore, recursive types in Haskell would demand a huge overhaul to how synonyms are handled, probably not worth the effort to put even as a language extension.
Iso-recursive types are a bit of a pain to use, you more or less have to explicitly tell the type checker how to fold and unfold your types, making your programs more complex to read and write.
However, this is very similar to what your doing with your Mu
type. Roll
is fold, and unroll
is unfold. So actually, we do have iso-recursive types baked in. However, equi-recursive types are just too complex so systems like OCaml and Haskell force you to pass recurrences through type level fixpoints.
Now if this interests you, I'd recommend Types and Programming Languages. My copy is sitting open in my lap as I'm writing this to make sure I've got the right terminology :)
Best Answer
Alright, let's go one by one.
Values
Values are the concrete pieces of data that programs evaluate and juggle. Nothing fancy, some examples might be
1
true
"fizz buzz foo bar"
Types
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 thate
is eithertrue
orfalse
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
ande'
whene : int
ande' : 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
It's pretty clear that
f : Something -> Something
, but what should thatSomething
be? In a boring type system, we'd have to specify something arbitrary, likeSomething = int
. In a more flexible type system, we could sayThat is to say "for any
a
,f
maps ana
to ana
". This let's us usef
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.
Type Constructor
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 likesort
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
Now
List
is a function which maps a typea
to a list of values of that type! In Java-land I think these are perhaps called "generic classes"Type Parameters
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 parametera
just like howList a
has a type parametera
.Kinds
Kinds are a bit tricky. The basic idea is that certain types are similar. For example, we have all the primitive types in java
int
,char
,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. Soint : 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
or
In Java since
List
needs to be applied to a concrete type to be used like that! If we look at their kindsList : Boxed -> Boxed
and sinceBoxed -> 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
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
Both are excellent books that introduce what I've just talked about and much more in beautiful, well explained detail.