What is the common supertype of all instances of Kind in Type Theory

Question

I'm trying to design an ontology such as could be defined with OWL or Topic Maps that includes support for polymorphic types such as List[T] where T is a type parameter of the Interval Kind In(Nothing, Any) and List is the Function Kind * -> *. Ultimately, I want to describe a type system ontology in semantic language with sufficient detail and rigour that it could be the basis for type-safe software code written in the same semantic language.

With this goal in mind, I'm trying to figure out a hierarchical structure of Kinds where Type, Interval Kind and Function Kind are all instances of Kind. Is there a formal name for the common 'superkind' of all Kinds? The best term I can come up with is 'Kind Instance'. Is this even a meaningful concept in type theory? Even if it isn't, I need such a concept to say things such as (in Topic Maps terminology) "a function-argument-type-constraint association has a Role 'allowed-type' whose player must be of type 'Kind Instance'".

Beyond this, I've only just begun teaching myself type theory for this project and I have a lot more to learn before I'll be able to complete it. I have read a few scala-related papers on type-theory including Generics of a Higher Kind (http://adriaanm.github.com/files/higher.pdf) and started working my way through Safe Type-level Abstraction in Scala (http://adriaanm.github.com/files/scalina-final.pdf) and Type Constructor Polymorphism for Scala[pdf]. I have less familiarity with Haskell than Scala but I have encountered some relevant-looking papers such as System F with Type Equality Coercions[pdf] that I'll need a much more advanced grasp of Haskell to understand. If anyone can suggest a progression of reading material for learning Haskell's type system starting from the beginner level and leading all the way to advanced principles like Generalized Algebraic Data Types, that would also be much appreciated.

Finally, if you know of any existing attempts to describe a type system in a semantic ontology language like OWL or Topic Maps, or if you have any suggestions about how to do this, I'd love to hear that too.

Answer 1

There is no better introduction to type theory than Benjamin Pierce's "Types and Programming Languages". I don't think there are standardized names for the levels above kind, but "sort" is one common choice. Another common choice is to jump straight to dependent types and flatten the hierarchy, so that there is only one level after all. One common typing rule to add in this situation (when dealing with day-to-day programming languages whose logical content isn't usually so important) is the "Type : Type" rule, so that, for example, 3 : Int : Type : Type : Type : ...