Skip to content

Instantly share code, notes, and snippets.

@wongjiahau
Last active May 29, 2022 03:46
Show Gist options
  • Save wongjiahau/6b92782617117643a1099cec50fd4eff to your computer and use it in GitHub Desktop.
Save wongjiahau/6b92782617117643a1099cec50fd4eff to your computer and use it in GitHub Desktop.
The latex code for Hindley Milner Type System.
\documentclass{article}
\begin{document}
\begin{table}[h!]
\begin{center}
\begin{tabular}{cl}
\\
\(\frac
{x \ : \ \sigma \ \in \ \Gamma}
{\Gamma \ \vdash \ x \ : \ \sigma} \)
& [\texttt{Var}] \\
\\
\\
\(\frac
{\Gamma \ \vdash \ {e}_{0} \ : \ \tau \rightarrow {\tau}' \;\;\;\; \Gamma \ \vdash \ {e}_{1} \ : \ \tau}
{\Gamma \vdash {e}_{0} \; {e}_{1} \ : \ {\tau}'} \)
& [\texttt{App}] \\
\\
\\
\(\frac
{\Gamma , \ x \ : \ \tau \ \vdash \ e \ : \ {\tau}'}
{\Gamma \ \vdash \ \lambda x \ . \ e \ : \ \tau \rightarrow{\tau}'}\)
& [\texttt{Abs}] \\
\\
\\
\(\frac
{\Gamma \ \vdash \ {e}_{0} \ : \ \sigma \;\;\;\;
\Gamma, \ x \ : \ \sigma \ \vdash \ {e}_{1} \ : \ \tau}
{\Gamma \ \vdash \ \texttt{let} \ x \ = \ {e}_{0} \ \texttt{in} \ {e}_{1} \ : \ \tau}\)
& [\texttt{Let}] \\
\\
\\
\(\frac
{
\newline
\Gamma \ \vdash \ e \ : \ {\sigma}' \;\;\;\;
{\sigma}' \ \sqsubseteq \ \sigma
}
{
\Gamma \ \vdash \ e \ : \ \sigma
}\)
& [\texttt{Inst}] \\
\\
\\
\(
\frac
{
\Gamma \ \vdash \ e \ : \ \sigma \;\;\;\;
\alpha \ \notin \text{free}(\Gamma)
}
{
\Gamma \ \vdash \ e \ : \ \forall \ \alpha \ . \ \sigma
}
\)
& [\texttt{Gen}] \\
\\
\end{tabular}
\end{center}
\end{table}
\end{document}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment