---
title: "typing"
source: https://www.jemoka.com/posts/kbhtyping/
---

what is a type? a type is a set of values.
consider List[Int]; importantly, List is not a type; its a &ldquo;type constructor&rdquo; which takes a type as input (Int) and gives you as type as output List[int].
-&gt; is another &ldquo;type constructor&rdquo;; 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 -&gt; Int
types are rules of inference &ldquo;If Hypothesis is true, then Conclusion is true&rdquo; &ldquo;If E1 and E2 have certain types, then E3 has a certain type&rdquo;
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} &amp;A \vdash e_1: t \to t&rsquo;\\ &amp;A \vdash e_2 : t \end{align}}{A \vdash e_1e_2: t&rsquo;} \end{equation}
if my function \(f\) takes \(t\) to \(t&rsquo;\), then applying it to a \(t\) will give you a \(t&rsquo;\)
abstraction \begin{equation} \frac{A, x:t \vdash e: t&rsquo;}{A \vdash \lambda x:t . e : t \to t&rsquo;} \end{equation}
if we can prove that with a thing \(x\) of type \(t\) we can force \(e\) to be type \(t&rsquo;\), then the lambda wrapped around it would have the signature \(t \to t&rsquo;\).
let \begin{equation} \frac{\begin{align} &amp;A \vdash \lambda x.e : t, A \\ &amp;f: t \vdash e&rsquo; : t' \end{align}}{A \vdash let\ f=\lambda x.e \text{ in } e&rsquo; : t&rsquo;} \end{equation}
environment Environments gives types for free variables&mdash;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 &ldquo;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&rsquo;t allow primitive recursion, there maybe type duplication because you can&rsquo;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&rsquo;, A \vdash e : t}{A \vdash f e: t&rsquo;} \end{equation}
now, we modify this with a new type variables
\begin{equation} \frac{t=t&rsquo; \to \beta, A \vdash e_1: t, A \vdash e_2 : t&rsquo;}{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 = ⍺ =&gt; S, t = ⍺, ⍺ = t [Symmetry] S, ⍺ = t1, ⍺ = t2 =&gt; S, ⍺ = t1, ⍺ = t2, t1 = t2 [Transitivity] S, t1 → t2 = t3 → t4 =&gt; 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&rsquo; = C(\emptyset, S, A)\) is defined canonicalization
