# Type theoy
---
Type


Type safety
Degree to which a language enforces functions to obey the type required by arguments
- Strongly typed
- Weakly typed

Class of mathematical objects
Term
\[ \mathrm{term} : \mathsf[type]\]
mathematical object endowned with a specific type
Judgements
Declaration of type of some object (right of turnstile symbol) given some prior conditions (left of turnstile symbol)
\[\vdash\]

Algebraic data type (ADT)
Atomic type
Basic irreducible types

Function type
type describing a map between two types
Lambda term
Function type defined by a Lambda expression

Function application
alpha reduction
beta reduction
eta reduction

type of types \[ \mathsf{type} \]
type whose terms are all the possible types
empty type \[ 0 \]
type with no terms

unit type \[ 1 \]
type with two terms, canonically \[\mathrm{\*}\]

Boolean type \[ 2 \]
type with two terms, canonically \[\mathrm{true},\mathrm{false}\]

Natural numbers \[ \mathbb{N} \]
type representing natural numbers, often defined by repeated use of an increment function. Note the perspective of treating natual numbers as bying of type \[\mathbb{N}\] rather than belonging to \[\mathbb{N}\]

Product type
ordered pair of terms where the first term is of one type and the second term is of the second type
Sum type
Polymorphic type (generic type)
Type that requires knowledge of another type (such as arays of floats)

subtype
type that substitute any instance of its supertype 

Variance; type of relationship between subtypes
- covariant; A subtype of B means I<A> subtype of I<B>
- contravariant; A subtype of B means I<B> subtype of I<A>
- bivariant; A subtype of B means I<A> is the type I<B>
- invariant; none of above