I'm thinking about a type system that has some special kind of some certain types that are subtypes of the universe kind type.

Imagine the typing relation, where $A$ and $B$ are both types, $\textbf{Type}$ is the universe kind, like * in Haskell or Type in Idris or Set in Agda; while <: denotes subtyping:

$$ A:a \\ B:b \\ A <: B \\ a <: \textbf{Type} \\ b <: \textbf{Type} $$

Then what should the relation between $a$ and $b$? Could one of them be the subtype (or subkind?) of the other? Although it is fine to make $a$ and $b$ distinct, but ideally we want more consistent subtyping (subkinding) relations to present.

In other words, if I allow either $a <: b$ or $b <: a$, will the type system become inconsistent?

  • $\begingroup$ Since $a$ and $b$ are supposed to be kinds, you should be asking whether they are subkinds (not subtypes). Also, your question is pretty vague. The answer is "yes they could but not necessarily". What are you actually trying to find out? Whether there must be a relation between $a$ and $b$? Of course not, the question underspecifies what we are dealing with. $\endgroup$ – Andrej Bauer Jul 31 '19 at 11:55
  • $\begingroup$ Making a type system based on how its implemented in a PL sounds like a recipe for making it inconsistent. Perhaps you might want to look first at some of the type theories that inspire type systems in specific PLs, to see if any have the feature you want. That would usually avoid the chance for making something unsound. $\endgroup$ – Algeboy Jul 31 '19 at 16:09
  • $\begingroup$ Note Scala 3 has moved to a type system where types form a lattice, maybe that is related to your intentions. It certainly adds clarity to many programming situations, and while the type theory DOT in Scala 3 isn't as academically studied as others, it has had some validation in Coq. $\endgroup$ – Algeboy Jul 31 '19 at 16:12
  • $\begingroup$ @AndrejBauer question updated -- clarified what I was asking and wording. $\endgroup$ – ice1000 Jul 31 '19 at 22:24
  • $\begingroup$ @Algeboy: the so-called inconsistencies in programming languages almost exclusively arise from general recursion, or at least enough recursion available to inhabit every type. They have little to do with type systems of programming languges (except in fancy cases when the types themselves possess a form of recursion). So, looking at PL is quite ok here, and in any case we don't know whether OP is doing PL or something else with the types. $\endgroup$ – Andrej Bauer Aug 1 '19 at 6:45

There will be no inconsistency. Those arise from shady postulates which state that some subkind is an element of itself, or that "too large" a kind/type is an element of a "too small" one (the most famous example is $\mathrm{Type} : \mathrm{Type}$), but that is not what we are dealing with here.

To give an example of what you're looking for, take $\mathrm{Type}$ to be the class of all sets. For the subtype and subkind relations we simply use subset and subclass inclusion. Take $a$ to be the class of all finite sets, and $b$ the class of all countable sets. Let $A = \{23, 42\}$ and $B = \mathbb{N}$. Then we have $A : a$, $B : b$, $A \subseteq B$, $a \subseteq b$, and both $a$ and $b$ are subkinds of $\mathrm{Type}$. And it would not be difficult to arrange $A \subseteq B$ and $b \subseteq a$, if we so wished.

Or you could take $\mathrm{Type} = a = b$ and $A = B$, but that's not a very informative answer, even though it has its virtues.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.