What is the common supertype of all Kind instances in type theory

Question

I am trying to create an ontology, for example, which can be defined using OWL or thematic maps, which includes support for polymorphic types such as List [T], where T is a parameter of type Interval Kind In (Nothing, Any) and List is a function of the form * → *. Ultimately, I want to describe the ontology of the type system in a semantic language with sufficient detail and rigor so that it can be the basis for program code with software written in the same semantic language.

To this end, I am trying to figure out the hierarchical structure of views, where Type, Interval Kind, and Function Kind are instances of Kind. Is there a formal name for the common "supernatural" of all kinds? The best term I can think of is Kind Instance. Is this even a meaningful concept of type theory? Even if it’s not, I need a concept to say things such as (in the terminology "Thematic Maps") "association with the restriction of function-argument-type has the role of" allowed type ", whose player must be of type" Kind Instance " "".

Other than that, I just started teaching type theory for this project, and I have a lot more room to learn before I can finish this. I read several scala related articles on type theory, including Generics of the Higher Kind (http://adriaanm.github.com/files/higher.pdf), and started working on my way through Scala's safe level abstraction (http: //adriaanm.github.com/files/scalina-final.pdf) and Constructor-type Polymorphism for Scala [pdf] . I am less familiar with Haskell than Scala, but I came across some relevant documents, such as System F with type equality [pdf] , which I will need a much deeper understanding of Haskell to understand. If someone could suggest the progression of reading materials to study a system like Haskell, starting at the beginner level and leading all the way to advanced principles such as generalized algebraic data types, that would also be very helpful.

Finally, if you are aware of any existing attempts to describe the type system in a semantic ontological language such as OWL or Theme Maps, or if you have any suggestions on how to do this, I would also like to hear that.

Answer 1

There is no better introduction to type theory than Benjamin Pearce "Types and Programming Languages." I don’t think there are standard names for the levels above, but “sorting” is one of the common options. Another common choice is to go straight to the dependent types and smooth the hierarchy, so there is only one level. One typing rule to add to this situation (when working with everyday programming languages, the logical content of which is usually not so important) is the rule "Type: Type", so, for example, 3: Int: Type: Type: Type: ...