4
$\begingroup$

In the paper "introduction to type theory" by Herman Geuvers, it states the following definition for the type theory of propositional logic (I've added "convention 2" just for reference):

enter image description here

Given that this is an introduction, I'd assume that he would explain the meaning of a statement like $\mathrm {Typ}:=\mathrm {TVar}|(\mathrm {Typ}\to \mathrm {Typ})$, or what a "type variable" is.

My question is twofold:

  • What do these two things mean?

  • What background knowledge is this introduction assuming, that I would need to study before reading this "introductory" text?

$\endgroup$
7
$\begingroup$

Intuitively, a type variable is like a variable in an expression, except that it stands in for a type rather than standing in for a number/bitstring/etc.

Formally, we choose a countably infinite set $\mathsf{TVar}$, and then define a type variable to be a member of $\mathsf{TVar}$.

The notation $\mathsf{Typ}:=\mathsf{TVar}|(\mathsf{Typ}\to \mathsf{Typ})$ is an instance of Backus normal form. It is an inductive definition of $\mathsf{Typ}$. It says that if $\alpha$ is a type variable (i.e., if $\alpha \in \mathsf{TVar}$), then $\alpha$ is an element of $\mathsf{Typ}$; and if $\alpha,\beta$ are type variables (i.e., $\alpha,\beta \in \mathsf{TVar}$), then the term $\alpha \to \beta$ is an element of $\mathsf{Typ}$. $\mathsf{Typ}$ is the set of terms that can be constructed in this way. We call a term a type if it is an element of $\mathsf{Typ}$.

$\endgroup$
  • $\begingroup$ So $|$ basically means: "the term left to me and the term right to me are of the type that is being defined"? About my second question: What (topic) should I study so that I would have known this before reading this "introduction" on type theory, given that it apparently assumes this as background knowledge? $\endgroup$ – user56834 Apr 30 '18 at 18:20
  • 2
    $\begingroup$ It means "or". Like in context-free grammars. $\endgroup$ – Yuval Filmus Apr 30 '18 at 21:47
6
$\begingroup$

More formally, if you are familiar with algebraic data types (sometimes referred to as "generalized enumeration types") as in Haskell, O'Caml, Agda, Swift, Rust, and (thankfully) increasingly more programming languages, it's basically declaring $\mathsf{Typ}$ as:

data Typ tv = TVar tv | TArrow (Typ tv) (Typ tv)

This is using Haskell's algebraic data type syntax. Here I've decided to make tv a parameter because we don't care what the "type variables" actually are as long as we can distinguish them from each other and we can get a "new" one whenever we need to (hence the usual statement that it is a countably infinite set). To be clear, while algebraic data type mechanisms usually incorporate a "tag" to discriminate the options from each other, TVar and TArrow above, the notation used in the paper does not do a disjoint union. This means that we further require elements of $\mathsf{TVar}$ not to be of the form $t\to t'$ for $t,t'\in\mathsf{Typ}$. So $\mathsf{TVar}$ could be a set of natural numbers, a set of strings, a set of rational numbers, a set of finite subsets of natural numbers, or many, many other things.

At any rate, the core idea is the notion of an inductively defined set. Here's just a random book chapter I found googling "inductively defined set": https://www.cl.cam.ac.uk/teaching/1213/DiscMathII/Ch5.pdf As D.W. states, the specific notation used is inspired by Backus-Naur Form (almost always referred to simply as BNF) which is a notation for context-free grammars. Such grammars give rise to inductively defined sets of derivations.

$\endgroup$
5
$\begingroup$

You can read $Typ$ as the least set containing $TVar$, and such that for all $a, b \in Typ$ we have $(a \to b) \in Typ$.

$\endgroup$

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.