3
$\begingroup$

I'm attending a course on Type Theory. The textbook is 'Types and Programming Languages' by Prof. Benjamin C. Pierce.

In Chapter 29, Prof. Pierce introduces 'type operator', which can generate another type with an input type. For example, 'Pair' can be a type operator which accepts any two types $X$ and $Y$ to form a type $Pair\; X\; Y$.

However, the 'type operator' itself is a type - a special type which is different from 'proper type' such as $Nat$ and $Nat \rightarrow Nat$. It seems that all 'proper types' have terms of it. For example, $Nat \rightarrow Nat$ has at least $(\lambda x : Nat. x)$. But type operator like $Pair$ does not have any term of it.

Prof. Pierce doesn't explain why $Pair$ has no term. Why 'non-proper' types can be called a 'type' when it does not correspond to any collection of programming language terms?

$\endgroup$
3
$\begingroup$

Counter-question: why should every type be inhabited by a term? You could not have the Curry-Howard correspondence between typing systems and logic if every type was inhabited.

Concrete answer: I don't have Pierce's book handy, but I think you are talking about the system $\lambda\underline{\omega}$ in Barendregt's $\lambda$-cube, a classification of typing systems along three orthogonal axes. (Please correct me if I'm wrong.)

Barendregt's $\lambda$-cube.

$\lambda\underline{\omega}$ is the simplest extension of the simply typed $\lambda$-calculus allowing type-level computation. Note that $\lambda\underline{\omega}$ doesn't have parametric polymorphism or type dependency. One way of thinking about $\lambda\underline{\omega}$ is that type-level computation is carried out by having another $\lambda$-calculus, but this time at the type level. You can think of type-level computation as being run at 'compile time'. Why use a typed language to run type-level computation? Why not use the untyped $\lambda$-calculus at the type level? Because the things that could go wrong at the term level with untyped terms (e.g. ill-formed programs like $3 + hello$) could now go wrong at the type level (e.g. $\mathbb{B}\; Pair$). So $\lambda\underline{\omega}$ needs a way of preventing ill-formed type-level computation.

But how? Well, let's use the simply typed $\lambda$-calculus again, but now at the type-level, to carry out, and constrain type-level computation? In order to avoid terminological confusion, we speak of kinds of for this second simply typed $\lambda$-calculus. In summary:

  • Terms are classified by types.

  • Types are classified by kinds.

(As an aside, you can iterate this and have kind-level computation in the same way and so on, but that's not done in $\lambda\underline{\omega}$.)

So far, I've said that kinds classify types. That's another way of saying that well-formed programs for type-level computation inhabit kinds. In $\lambda\underline{\omega}$ kinds are given by the grammar

$$ \newcommand{\TY}{\mathsf{Ty}} \kappa\quad ::= \quad \TY\ \ |\ \ \kappa \rightarrow \kappa $$

Here $\kappa \rightarrow \kappa'$ is the kind of type-level functions such as $\lambda t^{\kappa}. \mathbb{N} \rightarrow \kappa$. But what is $\TY$? Answer: the base kind. The kind that is inhabited by all types that can potentially be inhabited by terms, e.g. types like $\mathbb{B}$ or $\mathbb{N} \rightarrow \mathbb{B}$. It is the only kind that is inhabited by types. This gives a neat classification of type-level programs into types usable to be inhabited by terms, and type-level programs that are only used as components in the computation of such types.

Operators like $Pair$ are not kinded by $\TY$ and so cannot be inhabited by terms. Instead $Pair$ has the kind $\TY$ $\rightarrow$ $\TY$ $\rightarrow$ $\TY$, which, by its very shape, cannot be inhabited by types, it can only be used as a program in a type-level computation. Now $\mathbb{N}$ (integers) and $\mathbb{B}$ (Booleans) both are kinded $\TY$, hence the type level program $Pair \;\mathbb{N} \;\mathbb{B}$ also has kind $\TY$ and can therefore be inhabited by a program.

$\endgroup$
  • $\begingroup$ Thanks for the explanations on Kinds. But I'm afraid 'Kind' classification is not the final reason that Pair is not inhabited. This classification must have been the result for incomprehensible extensions on type system. You've mentioned Curry-Howard correspondence and I guess that should be a better reason to make theoretical researchers create things like Pair. Am I right? $\endgroup$ – xywang Jun 12 '15 at 1:02
  • $\begingroup$ @xywang I'm not sure I understand your question. You can invent all sorts of crazy typing systems, but that's not how $\lambda\underline{\omega}$ works. What do you think should be the inhabitants of $Pair$? $\endgroup$ – Martin Berger Jun 12 '15 at 5:39
  • $\begingroup$ Sorry for my poor English...My previous comment was on two things: 1) being in different kinds seems to be the result of with/no inhabitants, but not the reason. 2) The counter-question is more interesting: what proposition can be matched to a type with no terms? Any false propositions? $\endgroup$ – xywang Jun 12 '15 at 6:14
  • $\begingroup$ @xywang Regarding (1) I'd say being "in different kinds" is the cause why $Pair$ has no term inhabitants. That's the choice the designers of $\lambda\underline{\omega}$ made. As to (2), under the Curry-Howard interpretation of type theory, Falsity (if it is represented as a type) has no inhabitants. But not the other way round. Consider the type / proposition $(A \vee B) \rightarrow (A \wedge B)$. It is not equivalent to Falsity, but what program could have this type? $\endgroup$ – Martin Berger Jun 12 '15 at 6:50
6
$\begingroup$

The best way to understand this is to have a second level of "types above types" which we then call kinds. Kinds can be formed by the following rules:

  1. Type is a kind.
  2. If K and L are kinds then so is K → L.

Kinds have elements:

  1. The elements of Type are types, such as nat, bool, nat → nat, nat × nat, etc.
  2. The elements of K → L are functions which map elements of K to elements of L.

For instance, Pair is an element of Type → Type → Type. It is a "kind-level" function which maps types A and B to type A × B. Another example is List which is an element of Type → Type and it maps a type A to the type List A of lists of As.

A very fancy kind is (Type → Type) → Type which takes a function on types and returns a type. An example of this is "recursive type definition". To see this, consider the most general form of a recursive type definition:

type t = Φ(t)

For instance, we could define lists of numbers like this (using OCaml notation):

type natlist = Nil | Cons of nat * natlist

This is a special case of the general recursive type definition if we take

Φ(a) = Nil | Cons of nat * a

We could actually define an operator rectype and then write

type t = rectype Φ

to define the type t which is equal to Φ(t). Now it takes a moment's thought that rectype is of kind (Type → Type) → Type. (At this point, if you have never seen this before, you should be having a minor epiphany.)

In Haskell Type is written as * so sometimes Haskell tells you that something has type * → *. This means that the thing is a type-level function taking types to types. In Ocaml there are kinds under the hood but they are never shown to the user (well, kind of since they get exposed through module types).

Professor Pierce of course knows all these things much better than I do, but most likely at this point in the course he does not want to burden you with another layer of $\lambda$-calculus on top of $\lambda$-calculus. A quick and dirty solution is to just put all the kinds together in one big messy pile and call them "improper types". The trouble with such things is that the smart students will get confused (and rightfully so).

$\endgroup$
  • $\begingroup$ Can we treat operators like Pair not a type? I know the three levels on term-type-kind requires Pair only lies in the type world. How about create another hierarchy which there are two worlds between terms and kinds? It seems that 'functions on types are type' is similar with 'functions on terms are terms'. Is that the reason we treat type operators as types? $\endgroup$ – xywang Jun 12 '15 at 1:08
  • $\begingroup$ Isn't this what I said? Pair is a function at the kind-level and should not be treated as a type (but rather as a type operator, in other words a function). The reason you are treating type operators as types is probably pedagogical (I am guessing). Why don't you ask prof. Pierce? $\endgroup$ – Andrej Bauer Jun 12 '15 at 6:14
  • $\begingroup$ I'm now clear about your point. I'm not sure whether treat type operator as type or not is a 'do as my wish' question... After reading the other replies it seems that the agreement is we should treat type operator as type and try to explain why there could be inhabited types. $\endgroup$ – xywang Jun 12 '15 at 6:32
  • 2
    $\begingroup$ Type operators are clearly not types, unless you stretch the meaning of "type" beyond anything reasonable. They are functions from types to types. Why you call them improper types in your class I do not know. $\endgroup$ – Andrej Bauer Jun 12 '15 at 6:47
2
$\begingroup$

The fact that a type operator doesn't describe a set of terms or values is precisely the reason that type operators aren't called proper types, but only improper types. Type operators are somewhat like types (because they are used for typing), but they are also somewhat unlike types (because they don't describe terms or values directly).

BTW, all proper types describe a set of values or terms, but that doesn't mean the set has to actually contain any values or terms. A proper type might also describe an empty set!

$\endgroup$
  • $\begingroup$ For now I treat type as something with practical use - semantic specification, formal helper on unstuckness etc. Why the theory researchers create types with no use? $\endgroup$ – xywang Jun 11 '15 at 15:36
  • 1
    $\begingroup$ @xywang Type-theory researchers have many interests, one of them being the use of types as logical specifications. In that use case it is vital that not all types are inhabited. $\endgroup$ – Martin Berger Jun 11 '15 at 15:40
0
$\begingroup$

Whether "Pair" is a type or not is mostly a naming question. "Pair" is not a proper type in the sense that it makes no sense to talk about an object having type "Pair", but "Pair" exists in the language where types are described, and for this reason it can be described as being a type expression.

IOW, the language of types includes expressions like "Int" and "Pair Int Int" which are proper types, and this second expression is an instance of the general form "t1 t2" which is basically an application, but at the type-level. So from this point of view "Pair" is an expression in the language of types, although it is not what is usually considered "a type" (which usually means "a proper type").

$\endgroup$
  • $\begingroup$ I used to think 'type' is defined after 'term' is defined. But now the type system can be free to go beyond 'term'...? $\endgroup$ – xywang Jun 12 '15 at 5:09
  • 1
    $\begingroup$ @xywang Your original thinking works for simple programming languages, but not for more complicated ones. Think of type-level computation as a new programming language, executed at compile time, whose programs return -- at compile time -- a type. This returned type is used in the type-checking process. $\endgroup$ – Martin Berger Jun 12 '15 at 8:33

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.