---
# System prepended metadata

title: Type Inference Rules

---

### Type Checking

<!--- data values--->
$\Huge 
\frac{}{G\ \vdash\ \text{true}\ :\ bool} 
\quad
\frac{}{G\ \vdash\ \text{false}\ :\ bool} 
\quad
\frac{}{G\ \vdash\ n\ :\ int}$

<!--- plus --->
$\Huge \frac{G\ \vdash\ e_1\ :\ int\ \quad G\ \vdash\ e_2\ :\ int}{G\ \vdash\ e_1\ +\ e_2\ :\ int\ }$

<!--- and --->
$\Huge \frac{G\ \vdash\ e_1\ :\ bool\ \quad G\ \vdash\ e_2\ :\ bool\ }{G\ \vdash\ e_1\ \&\& \ e_2\ :\ bool\ }$

<!-- if --> 
$\Huge \frac{G\ \vdash\ e_1\ :\ bool\ \quad G\ \vdash\ e_2\ :\ t\  \quad G\ \vdash\ e_3\ :\ t\ }{G\ \vdash\ \text{if}\ e_1\ \text{then}\ e_2\ \text{else}\ e_3\ :\ t\ }$

<!-- fun -->
$\huge \frac{G,x:t_1\ \vdash\ e\ :\ t_2 }{G\ \vdash\ \text{fun}\ (x\ :\ t_1)\ \rightarrow\ e\ :\ t_1\ \rightarrow t_2\ }$

<!-- lookup -->
$\huge \frac{}{G\ \vdash\ x\ :\ G(x)\ }$

<!-- let -->
$\huge \frac{G\ \vdash\ e_1\ : t_1\ 
      \quad
      G,x:t_1\ \vdash\ e_2\ : t_2\ }
      {G\ \vdash\ \text{let}\ x\ =\ e_1\ \text{in}\ e_2\ :\ t_2\ }$

Example 1a: Use type checking to prove that this is well-typed: 

`let a = true in a && false`
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
Example 1b: Use type checking to prove that this is well-typed: 

`fun (z:int) -> z + 1`
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\

### Type Inference

<!--- data values--->
$\Huge 
\frac{}{G\ \vdash\ \text{true}\ :\ bool\ \dashv\ \{\}} 
\quad
\frac{}{G\ \vdash\ \text{false}\ :\ bool\ \dashv\ \{\}} 
\quad
\frac{}{G\ \vdash\ n\ :\ int\ \dashv\ \{\}}$

<!--- plus --->
$\Huge \frac{G\ \vdash\ e_1\ :\ t_1\ \dashv\ C_1\quad G\ \vdash\ e_2\ :\ t_2\ \dashv\ C_2}{G\ \vdash e_1\ +\ e_2\ :\ int\ \dashv\ \{t_1:t_2,\ t_1: int\}\ \cup\ C_1\ \cup\ C_2}$

<!--- and --->
$\Huge \frac{G\ \vdash\ e_1\ :\ t_1\ \dashv\ C_1\quad G\ \vdash\ e_2\ :\ t_2\ \dashv\ C_2}{G\ \vdash e_1\ \&\& \ e_2\ :\ bool\ \dashv\ \{t_1:t_2,\ t_1: bool\}\ \cup\ C_1\ \cup\ C_2}$

<!-- if --> 
$\Huge \frac{G\ \vdash\ e_1\ :\ t_1\ \dashv\ C_1 \quad G\ \vdash\ e_2\ :\ t_2\ \dashv\ C_2 \quad G\ \vdash\ e_3\ :\ t_3\ \dashv\ C_3}{G\ \vdash\ \text{if}\ e_1\ \text{then}\ e_2\ \text{else}\ e_3\ :\ t_2\ \dashv\ \{t_1:bool,\ t_2:t_3\}\ \cup\ C1\ \cup\ C_2\ \cup\ C_3}$

<!-- fun -->
$\huge \frac{\text{make}(t_x) \quad G,x:t_x\ \vdash\ e\ :\ t\ \dashv\ C_1}{G\ \vdash\ \text{fun}\ x\ \rightarrow\ e\ :\ t_x\ \rightarrow t\ \dashv\ C_1}$ 
(make creates some new, not yet used 'a/'b/'c-style type)

<!-- lookup -->
$\huge \frac{}{G\ \vdash\ x\ :\ G(x)\ \dashv\ \{\}}$

<!-- let -->
$\huge \frac{G\ \vdash\ e_1\ : t_1\ \dashv\ C_1
      \quad
      G,x:t_1\ \vdash\ e_2\ : t_2\ \dashv\ C_2}
      {G\ \vdash\ \text{let}\ x\ =\ e_1\ \text{in}\ e_2\ :\ t_2\ \dashv\ C_1\ \cup\ C_2}$
      
Example 2a: Use type inference to prove that this is well-typed: 

`let a = true in a && false`
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
Example 2b: Use type inference to prove that this is well-typed: 

`fun z -> z + 1`
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
___________
      
Example(s) with just let bindings and &&:
      
![1744151825235-3a1a656a-5e84-4184-aefc-d6fb48ec5bf7_1](https://hackmd.io/_uploads/BJdrSQ701g.jpg)


Example(s) with functions and +:

![1744151825235-3a1a656a-5e84-4184-aefc-d6fb48ec5bf7_2](https://hackmd.io/_uploads/S1uSHQmA1e.jpg)
