When we discuss the type of functions, we describe them like Int ->
Float. I can say I have a function that takes a real number and
always returns a positive or zero real number, Real ->
PositiveOrZeroReal [1].
In my mind, I can think of many things. I can consider a function
that takes some type A, and returns optionally the type List[String]
or the value 42, depending on a throw of a die. (Perhaps I cannot
phrase it well into standard CS theory, but I can think of it). When
I try to express this concept precisely using CS theory, I fall
short. Of course, it is not often useful to discuss functions from
types to types-or-numbers, and so perhaps this does not exist in
theory or practice.
If we discussed the function f(x) = x^2, you might say that this
function has type Real -> Complex. That would be technically correct,
but not as precise as Real -> Real, or Real -> PositiveOrZeroReal,
right?
However, it does seem often useful to discuss functions from types to
types, with some caveats. I consider a type constructor like List[T]
to be such a function.
When I look at a type constructor like List, I see that its kind is
traditionally defined as * => *. I wonder, why is that the case? Why
is its kind not A => List[A]? That seems to me to be more precise,
more useful. My first thought perhaps is that the * => * notation
implies this automatically; that is, the type in the first * is
incor****ated into the type represented by the second *. But this
cannot be true, for I can conceive of many functions with strange
kinds. Consider the function to satisfy A => Int (that is, a constant
kind always returning Int). This is * => * as well but it seems very
different from List.
The Kind notation "K ::= K | * => K" basically only describes the
arity of the kind. How is that useful? That seems to me like only
describing the arity of a function. There are many functions like (* -
> *) but (List[Int]-> Int) is perhaps very different from (Int ->
List[Int]). With function notation, we can see the difference between
catamorphisms and anamorphisms, but with kind notation we barely
discern anything ... ?
Is there no algebra to discuss type constructors / higher order
functions describing kinds like A => List[A]? This seems to make
intuitive sense to me. Perhaps List is an interface, with
SinglyLinkedList, LinkedList, RecursiveList, and other
implementations. Then the kind A => List[A] represents the kind of
all of these type constructors! Is this not a useful notion?
I could not accept that A => List[A] is not a useful notion! I think
that this kind has a "solution" for the term List just like other
descriptive equations with quantifiers (that is to say, it is really
Forall A. A => List[A], right? ) in type systems have meaningful
solutions.
For example, List[T] = Nil | T * List[T] is a similar quantifier; that
is, Forall T. List[T] = Nil | T * List[T]. The solution to this is
something meaningful, and is necessary for every recursive structure,
right?
If one describes kinds more precisely, one might hope to generalize
about the kind A => C[A]. I think that this kind has a very
characterizable set of inhabitants (container data structures)! Most
type systems cannot express such constructors as I understand it.
Why? Is there a trap to including such a concept in a static type
system that I don't see?
What should I study to learn more about this?
Thanks for your time. Happy holidays & New Year, everyone!
[1] Humor me :) My syntax is loose in this post. It's sort of a
Scala-ML hybrid.
--
Justin Crites
|
