typing — Jemoka Knowledge Base

what is a type? a type is a set of values. consider List[Int]; importantly, List is not a type; its a “type constructor” which takes a type as input (Int) and gives you as type as output List[int]. -> is another “type constructor”; its a type constructor written in infix notation. It takes two arguments, it constructs a type for set of functions which takes an integer as input and maps it to another integer Int -> Int types are rules of inference “If Hypothesis is true, then Conclusion is true” “If E1 and E2 have certain types, then E3 has a certain type” For instance: if e_1 has type Int and e_2 has type Int, then e_1 + e_2 has type Int. inference rule notation \begin{equation} \frac{\vdash H_{1} \dots \vdash H_{n}}{\vdash C} \end{equation} where each H_{j}, C have the shape \vdash e: T, that some e has type some T summation \begin{equation} \frac{\vdash e_1 : Int, \vdash e_2: Int}{\vdash e_1+e_2 : Int} \end{equation} combining rules suppose you need to first show that 1 and 2 are integers

\begin{equation} \frac{\frac{\vdash 1: \text{1 is an integer}}{\vdash 1 : Int}, \frac{\vdash 2: \text{1 is an integer}}{\vdash 2 : Int}}{\vdash 1+2 : Int} \end{equation}

type rules variables \begin{equation} \frac{}{A, x: t \vdash x: t} \end{equation} if you assume x:t, then x:t integers \begin{equation} \frac{}{A \vdash i: int} \end{equation} we call i any int function applications \begin{equation} \frac{\begin{align} &A \vdash e_1: t \to t’\ &A \vdash e_2 : t \end{align}}{A \vdash e_1e_2: t’} \end{equation} if my function f takes t to t’, then applying it to a t will give you a t’ abstraction \begin{equation} \frac{A, x:t \vdash e: t’}{A \vdash \lambda x:t . e : t \to t’} \end{equation} if we can prove that with a thing x of type t we can force e to be type t’, then the lambda wrapped around it would have the signature t \to t’. let \begin{equation} \frac{\begin{align} &A \vdash \lambda x.e : t, A \ &f: t \vdash e’ : t' \end{align}}{A \vdash let\ f=\lambda x.e \text{ in } e’ : t’} \end{equation} environment Environments gives types for free variables—an environment is a function from variables to types. Let A be a function from free variables to type. For instance, A \vdash e:T, meaning “under the assumption that variables have types by A, its provable that the expression e has type T. We have then tack on this on

\begin{equation} \frac{A \vdash e_1 : Int, A \vdash e_2: Int}{A\vdash e_1+e_2 : Int} \end{equation}

variables \begin{equation} \frac{A(x) = T}{A \vdash x:T} \end{equation} religion For a type system that doesn’t allow primitive recursion, there maybe type duplication because you can’t assign a thing into multiple types. type inference see type inference for every new application, we wrote

\begin{equation} \frac{A \vdash f: t \to t’, A \vdash e : t}{A \vdash f e: t’} \end{equation}

now, we modify this with a new type variables

\begin{equation} \frac{t=t’ \to \beta, A \vdash e_1: t, A \vdash e_2 : t’}{A \vdash e_1e_2: \beta} \end{equation}

and now, to actually type things, we just want to solve for \beta. we then solve the constraints: S, t = ⍺ => S, t = ⍺, ⍺ = t [Symmetry] S, ⍺ = t1, ⍺ = t2 => S, ⍺ = t1, ⍺ = t2, t1 = t2 [Transitivity] S, t1 → t2 = t3 → t4 => S, t1 → t2 = t3 → t4, t1 = t3, t2 = t4 [Structure] infiite solutions Consider:

\begin{equation} x = int \to x \end{equation}

constraint solving for each equation A=B \in S, check that A’ = C(\emptyset, S, A) is defined canonicalization