2
$\begingroup$

I've tried to learn type theory a few times, but the notation $x : X$ always trips me up. Does it mean:

  1. $x$ represents a fixed but arbitrary inhabitant of the type $X$?
  2. The variable $x$ is just "associated" to the type $X$, but not necessarily fixed. In particular, we can now write $\forall xPx$ as shorthand for $(\forall x : X)(Px),$ similarly we can write $\lambda x f x$ as shorthand for $(\lambda x : X)(f x)$ etc.
  3. Something else?

Thanks.

$\endgroup$
3
  • 2
    $\begingroup$ The "meaning" of $x : X$ is that $x$ is of type $X$, no more, no less. You can think of it as being like $x \in X$ if you like but this is misleading. More importantly, types are not like sets: whereas you can ask, "what are the members of this set?", you cannot ask, "what are the inhabitants of this type?" $\endgroup$
    – Zhen Lin
    Aug 29, 2013 at 13:01
  • $\begingroup$ @ZhenLin, when you say that we cannot ask, "what are the inhabitants of this type?" what precisely do you mean? Are you basically saying that that although $x : X \vdash [\mbox{whatever}]$ makes sense, nonetheless $\neg(x : X) \vdash [\mbox{whatever}]$ is meaningless? Thus $x : X$ is devoid of a truthvalue. $\endgroup$ Oct 1, 2013 at 8:02
  • $\begingroup$ In the first place, $\lnot (x : X)$ is not a well-formed formula. But I would not go so far as to say that $x : X$ has no truth value. (My own view is that $x : X$ is well-formed in a given context if and only if $x$ is a term of type $X$ in that context, so it is true if well-formed.) $\endgroup$
    – Zhen Lin
    Oct 1, 2013 at 8:18

2 Answers 2

5
$\begingroup$

When you formalize type theory it is probably easiest to work with expressions $C \vdash J$, where $C$ is a context, and $J$ is a judgement. A context is of the form $x_1 : A_1, \ldots, x_n : A_n$ where $x_i$ are free variables and $A_i$ are types. A judgement is either $t : A$ or $t \equiv s : A$ where $A$ is a type and $t$ and $s$ are terms. The terms $s$ and $t$ can contain free variables, but we only consider $C \vdash J$ when every free variable occurring in $J$ already appears in $C$.

When we see $x : A$ as part of a context it is an assumption, so we think of it as saying "for every $x$ of type $A$." However, exactly the same expression $x:A$ can also appear as the judgement $J$ (since each free variable is in particular a term). In this case we read it as saying "$x$ is an object of type $A$."

To give an easy example, we can prove in type theory $x:A, y:B \vdash (x, y) : A \times B$. This says that, given an object $x$ of type $A$ and an object $y$ of type $B$, the term $(x, y)$ is of type $A \times B$. We can also think of this as a function, that takes two inputs (one from $A$ and one from $B$) and produces an element of $A \times B$.

$\endgroup$
7
  • $\begingroup$ Thanks, this is helping a lot. So..... can we write things like $x : \mathbb{N} \vdash \forall x(x+1 \neq 0)$? $\endgroup$ Aug 29, 2013 at 13:07
  • 1
    $\begingroup$ The variable $x$ on the RHS is bound by $\forall$, so you should write either $\vdash \forall x : \mathbb{N} . x + 1 \ne 0$ or $x : \mathbb{N} \vdash x + 1 \ne 0$. $\endgroup$
    – Zhen Lin
    Aug 29, 2013 at 13:34
  • $\begingroup$ Like Zhen Lin said, $x$ should not be bound on the right hand side. Another issue is that $x + 1 \neq 0$ is not a valid judgement, because every judgement is either of the form $t : A$ or $t \equiv s : A$. To express what you want, you need to use identity types. $\endgroup$
    – aws
    Aug 29, 2013 at 13:46
  • 3
    $\begingroup$ A valid expression would be $x : \mathbb{N} \vdash t : I_\mathbb{N}(x + 1, 0) \rightarrow \bot$, where $I_\mathbb{N}(x + 1, 0)$ is the type of "proofs that $x+1$ and $0$ are equal", $\bot$ is the empty type and $t$ is a term that you need to find. $\endgroup$
    – aws
    Aug 29, 2013 at 13:48
  • 1
    $\begingroup$ Note also that $\Pi_{x:\mathbb{N}}A$ is a type not dependent on $x$ and finding a proof of $\Pi_{x:\mathbb{N}}A$ in the empty context is equivalent to finding a proof of $A$ in the context $x:A$. $\endgroup$
    – aws
    Aug 29, 2013 at 15:51
0
$\begingroup$

x such that the set X; ":" operator denotes "such that". It is basically its type.

$$a : b$$ and the description following the colon is actually the definition (b) of a.

$\endgroup$
2
  • $\begingroup$ Wait, in type theory? $\endgroup$ Aug 29, 2013 at 12:21
  • 1
    $\begingroup$ In type theory and programming language theory, the colon sign after a term is used to indicate its type, sometimes as a replacement to the symbol. $\endgroup$
    – Don Larynx
    Aug 29, 2013 at 12:23

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.