Polymoprhic Typing Rule

---

We will say a monomorphic type $\tau$ is an $\mathbf{\text{instance}}$ of a polymorphic type $\sigma$ if there exists a monomorphic type ${\tau }^{\prime }$, (a possibly empty) list of type variables ${\alpha }_1,\cdots ,{\alpha }_n$, and a corresponding list of monomorphic types ${\tau }_1,\cdots ,{\tau }_n$ such that $\sigma =\mathrm{\forall }{\alpha }_1,\cdots ,{\alpha }_n$. ${\tau }^{\prime }$ and $\tau ={\tau }^{\prime }[{\tau }_1/{\alpha }_1,\cdots ,{\tau }_n/{\alpha }_n]$, the type gotten by replacing each occurence of ${\alpha }_i$ in ${\tau }^{\prime }$ by ${\tau }_i$. When using the rule below that require one type to be an instance of another, you should give the instantiation: $[{\tau }_1/{\alpha }_1,\cdots ,{\tau }_n/{\alpha }_n]$.

In simpler terms, think of a polymorphic type like a template and a monomorphic type like a filled-out form of that template. The process described is like saying, “To prove that this filled-out form is based on a specific template, show me how you substituted the placeholders in the template with actual information to get this form.

Signatures

Polymorphic constant signatures:

$\text{sig(true) = bool}$	$\text{sig(true) = bool}$
$\text{sig}(n)=\text{int }n\text{ an integer constant}$	$\text{sig}(f)=\text{float }f\text{ a floating point (real) constant}$
$\text{sig}(s)=\text{string }s\text{ a string constant}$	$\text{sig}([])=\mathrm{\forall }\alpha .\alpha \text{list}$

Polymorphic Unary Primitive Operators:

$\text{sig(fst)}=\mathrm{\forall }\alpha \beta .(\alpha \ast \beta )\to \alpha$	$\text{sig(snd)}=\mathrm{\forall }\alpha \beta .(\alpha \ast \beta )\to \beta$
$\text{sig(hd)}=\mathrm{\forall }\alpha .\alpha \text{list}\to \alpha$	$\text{sig(tl)}=\mathrm{\forall }\alpha .\alpha \text{list}\to \alpha \text{ list}$
$\text{sig}(\sim )=\text{int }\to \text{ int}$	$\text{sig(print\_string)}=\text{string }\to \text{ unit}$
$\text{sig(not)}=\text{bool }\to \text{ bool}$

Polymorphic Binary Primitive Operators:

$\text{sig}(\oplus )=\text{int}\to \text{ int}\to \text{ int for }\oplus \in \{+,-,\ast ,\text{mod},/\}$	$\text{sig}{(}^{\wedge })=\text{string }\to \text{ stirng}\to \text{ string}$
$\text{sig}(\oplus )=\text{float}\to \text{ float}\to \text{ float for }\oplus \in \{+.,-.,\ast .,/.,\ast \ast \}$	$\text{sig}((\mathrm{\_},\mathrm{\_}))=\mathrm{\forall }\alpha \beta .\alpha \to \beta \to \alpha \ast \beta$
$\text{sig}(\wr )=\text{bool}\to \text{ bool}\to \text{ bool for }\wr \in \{||,\mathrm{\&}\mathrm{\&}\}$	$\text{sig}(::)=\mathrm{\forall }\alpha .\alpha \to \alpha \text{ list}\to \alpha \text{ list}$
$\text{sig}(\approx )=\mathrm{\forall }\alpha .\alpha \to \alpha \to \text{bool for }\approx \in \{<,>,=,<=,>=,<>\}$

Rules

Constants:

$\frac{}{\mathrm{\Gamma }⊢c:\tau }$ $\text{CONST}\text{where }c\text{ is a constant listed above, and }\tau \text{ is an instance of sig}(c)$

Variables:

$\frac{}{\mathrm{\Gamma }⊢x:\tau }$ $\text{VAR}$ $\text{ where }x\text{ is a variable and }\tau \text{ is an instance of }\mathrm{\Gamma }(x)$

Unary Primitive Operators:

$\frac{\mathrm{\Gamma }⊢e:{\tau }_1}{\mathrm{\Gamma }⊢\oplus e:{\tau }_2}$ $\text{MONOP}$ ${\tau }_1\to {\tau }_2\text{ an instance of sig}(\oplus )$

Binary Prmitive Operators:

$\frac{\mathrm{\Gamma }⊢e_1:{\tau }_1\mathrm{\Gamma }⊢e_2:{\tau }_2}{\mathrm{\Gamma }⊢e_1\odot e_2:{\tau }_3}$ $\text{BINOP}$ ${\tau }_1\to {\tau }_2\to {\tau }_3\text{ an instance of sig}(\odot )$

If then else rule:

$\frac{\mathrm{\Gamma }⊢e_c:\text{bool}\mathrm{\Gamma }⊢e_t:\tau \mathrm{\Gamma }⊢e_e:\tau }{\mathrm{\Gamma }⊢\text{if}{e}_c\text{then}{e}_t\text{else}{e}_e:\tau }$ $\text{IF}$

Application rule:

$\frac{\mathrm{\Gamma }⊢e_1:{\tau }_1\to {\tau }_2\mathrm{\Gamma }⊢e_2:{\tau }_1}{\mathrm{\Gamma }⊢e_1{e}_2:{\tau }_2}$ $\text{APP}$