Written by Li Zhuohua
on 

Notes on Type Theory

Here are some notes about type theory, mainly from the book Type Theory and Formal Proof: An Introduction.

\(\lambda\to\) (terms depending on terms) #

Definitions #

  1. Variables: \(V={x,y,z,\ldots}\)
  2. Type variables: \(\mathbb{V}={\alpha, \beta, \gamma, \ldots}\)
  3. Types: \(\mathbb{T}=\mathbb{V}\mid \mathbb{T}\to \mathbb{T}\)
  4. Pre-typed \(\lambda\)-terms: \(\Lambda_{\mathbb{T}}=V\mid (\Lambda_{\mathbb{T}}\Lambda_{\mathbb{T}})\mid (\lambda V:\mathbb{T}.\Lambda_{\mathbb{T}})\)
  5. Statement, declaration, context, judgement
    1. Statement: \(M:\sigma\), where \(M\in\Lambda_\mathbb{T}, \sigma\in\mathbb{T}\)
    2. Declaration: a statement with \(M\in V\)
    3. Context: \(\Gamma\), a list of declarations with different \(M\)
    4. Judgement: \(\Gamma \vdash M:\sigma\)
  6. \(\beta\)-Reduction (\(\to_{\beta}\)): \((\lambda x:\sigma.\; M)N \to_{\beta} M[x:=N]\)
  7. Derivation rules:

Notes #

  1. Basically the same with untyped lambda calculus, except that we add types.
  2. The type for each variable is explicitly given in advance, aka Church typing.
  3. The type, if existing, is unique.
  4. Church-Rosser Theorem holds.
  5. \(\lambda\to\) is strongly normalizing, meaning that a well-typed term always reduced to a value. This also means \(\lambda\to\) is not Turing complete.

\(\lambda2\) (\(\lambda\to\) + terms depending on types) (polymorphisim, generic programming) #

Definitions #

  1. Variables: \(V={x,y,z,\ldots}\)
  2. Type variables: \(\mathbb{V}={\alpha, \beta, \gamma, \ldots}\)
  3. The type of all types: \(*\), e.g. \(\alpha:*\)
  4. Type-binder (\(\Pi\)-binder): The type of functions that convert an arbitrary type to a term of type, e.g. \(\lambda\alpha:*.\; \lambda x:\alpha.\; x:\Pi\alpha:*.\; \alpha\to\alpha\)
  5. Types: \(\mathbb{T}2=\mathbb{V}\mid(\mathbb{T}2\to\mathbb{T}2)\mid(\Pi\mathbb{V}:*.\; \mathbb{T}2)\)
  6. \(\lambda2\)-terms: \(\Lambda_{\mathbb{T}2}=V\mid (\Lambda_{\mathbb{T}2}\Lambda_{\mathbb{T}2})\mid (\Lambda_{\mathbb{T}2}\mathbb{T}2)\mid(\lambda V:\mathbb{T}2.\Lambda_{\mathbb{T}2})\mid(\lambda \mathbb{V}:*.\; \Lambda_{\mathbb{T}2})\)
  7. Statement, declaration, context, judgement
    1. Statement: either \(M:\sigma\) where \(M\in\Lambda_{\mathbb{T}2}, \sigma\in\mathbb{T}2\), or \(\sigma:*\), where \(\sigma\in\mathbb{T}2\)
    2. Declaration: a statement with \(M\in V\) or \(M\in\mathbb{V}\)
    3. Context: \(\Gamma\), a list of declarations with the restriction that all variables must be declared before they can be used
    4. Judgement: \(\Gamma \vdash M:\sigma\), or \(\Gamma \vdash \sigma:*\)
  8. \(\beta\)-Reduction (\(\to_{\beta}\)):
    1. (First order): \((\lambda x:\sigma.\; M)N\to_{\beta}M[x:=N]\)
    2. (Second order): \((\lambda \alpha:*.\; M)T\to_{\beta}M[\alpha:=T]\)
  9. Derivation rules:

Notes #

  1. Comparing with \(\lambda\to\), \(\lambda2\) adds the type of all types (\(*\)), and \(\Pi\)-types
  2. \(*\) is used to introduce second-order \(\lambda\)-abstraction, e.g. \(\lambda \alpha:*.\; \lambda x:\alpha.\; x\)
  3. \(\Pi\)-type is used to represent the types of the second-order terms, e.g. \(\lambda \alpha:*.\; \lambda x:\alpha.\; x\; :\; \Pi\alpha: *.\; \alpha\to\alpha\)
  4. Two new derivation rules ((\(appl_2\)), (\(abst_2\))) capture second order abstraction and application rules
  5. Uniqueness of Types, Church-Rosser Theorem and Strong Normalization Theorem still hold

\(\lambda\underline{\omega}\) (\(\lambda\to\) + types depending on types) (type constructor) #

Definitions #

  1. Variables and type variables are unified: \(V={x,y,z,\ldots,\alpha, \beta, \gamma, \ldots}\)
  2. The type of all types: \(*\), e.g. \(\alpha:*\)
  3. The type of type constructors: \(*\to*\), e.g. \(\lambda\alpha:*.\; \alpha\to\alpha: :: *\to*\)
  4. Kinds: \(\mathbb{K}=*\mid(\mathbb{K}\to\mathbb{K})\)
  5. The type of all kinds: \(\Box\), e.g. \(*:\Box\), and \(*\to*:\Box\)
  6. Sort: either \(*\) or \(\Box\), denoted by \(s\)
  7. Terms and types are unified as expressions: \(\mathcal{E}=V\mid\Box\mid * \mid(\mathcal{E}\mathcal{E})\mid(\lambda V:\mathcal{E}.\; \mathcal{E})\mid(\mathcal{E}\to \mathcal{E})\)
  8. Statement, declaration, context, judgement
    1. Statement: \(A:B\), where \(A, B\in \mathcal{E}\)
    2. Declaration: no longer has such terminology, because context is defined in a different way
    3. Context: \(\Gamma\), it is well-formed if it can be constructed by derivation rules, i.e., there are \(A\) and \(B\) such that \(\Gamma \vdash A:B\)
    4. Judgement: \(\Gamma \vdash A:B\)
  9. \(\beta\)-Reduction: Natural thus omitted
  10. Derivation rules:

Notes #

  1. Comparing with \(\lambda\to\), \(\lambda\underline{\omega}\) adds type constructors, a function that takes a type and outputs a new type. E.g. \(\lambda \alpha:*.\; \alpha\to\alpha\), which maps the type \(\alpha\) to the new type \(\alpha\to\alpha\)
  2. The type of type constructors is \(*\to*\). A type can be also regarded as a type constructor because it is “a function that takes nothing and outputs a type”.
  3. Since now we have a “super-type” \(*\to*\), we define kinds as above
  4. The type of all kinds is defined as \(\Box\)
  5. Unlike the previous two systems, types are not given beforehand as a fixed set. The permissibility of a type occurring in a judgement depends on whether we can formally derive it
  6. Uniqueness of Types, Church-Rosser Theorem and Strong Normalization Theorem still hold

\(\lambda P\) (\(\lambda\to\) + types depending on terms) (dependent types) #

Definitions #

  1. \(V\), \(*\), kinds, sorts are the same as those in \(\lambda\underline{\omega}\)
  2. Expressions: \(\mathcal{E}=V\mid\Box\mid * \mid(\mathcal{E}\mathcal{E})\mid(\lambda V:\mathcal{E}.\; \mathcal{E})\mid(\Pi V:\mathcal{E}.\; \mathcal{E})\)
  3. Statement, declaration, context, judgement are the same those in \(\lambda\underline{\omega}\)
  4. Derivation rules (Note that (sort), (var), (weak), (conv) are the same as those in \(\lambda\underline{\omega}\))

Notes #

  1. Comparing with \(\lambda\underline{\omega}\), \(\lambda P\) introduces \(\Pi\)-types (in rule (form)), because \(x\) can appear in \(B\) as free variables.
  2. Since \(\lambda P\) does not have types depending on types, in \(\Pi x:A.\; B\), \(x\) must be a term so \(A\) can only have type \(*\)
  3. \(\lambda P\) is able to code minimal predicate logic, which has implication and universal quantification operations:

  1. The coding of minimal predicate logic by means of the derivation rules of \(\lambda P\):

    Minimal predicate logic The type theory of \(\lambda P\)
    (S\) is a set| (S:*\)|
    (A\) is a proposition| (A:*\)|
    (a\in S\)| (a:S\)|
    (p\) proves \(A\)| (p:A\)|
    (P\) is a predicate on \(S\)| (P:S\to *\)|
    (A\Rightarrow B\)| (A\to B\) (\(=\Pi x:A.\; B\))|
    (\forall_{x\in S}(P(x))\)| (\Pi x:S.\; Px\)|
    \(\Rightarrow-elim\))| \(appl\))|
    \(\Rightarrow-intro\))| \(abst\))|
    \(\forall-elim\))| \(appl\))|
    \(\forall-intro\))| \(abst\))|

  2. Term finding is decidable in \(\lambda\to\) and \(\lambda\underline{\omega}\), but undecidable in \(\lambda P\). This is understandable because \(\lambda P\) is equivalent to minimal predicate logic, thus according to the Church-Turing Undecidability Theorem (Entscheidungsproblem), there is no general method to prove or disprove an arbitrary theorem.

\(\lambda C\) (\(\lambda2 + \lambda\underline{\omega} + \lambda P\)) (types/terms depending on types/terms) #

Definitions #

  1. The only difference between \(\lambda P\) and \(\lambda C\) is the rule (form):

Notes #

  1. By choosing the combinations of \(s_1\) and \(s_2\), we get 8 systems, and they form the \(\lambda\)-cube:

lambda-cube

  1. Uniqueness of Types holds up to conversion, i.e., if \(\Gamma \vdash A:B_1\) and \(\Gamma \vdash A:B_2\), then \(B_1=_\beta B_2\)
  2. Church-Rosser Therorem and Strong Normalization Theorem hold
  3. Term finding is decidable in \(\lambda\to\) and \(\lambda\underline{\omega}\), but undecidable in all other systems

No notes link to this note