/
kinding.tex
43 lines (30 loc) · 1.81 KB
/
kinding.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
\colorbox{thistle}{For programming language, three levels: \textit{\textbf{terms}}, \textit{\textbf{types}}, and \textit{\textbf{kinds}}, have proved sufficient}.
\subsection{Terms}
Sometimes, the word \textit{term} and \textit{expression} are used interchangeably.
Recap term-level \textit{abstraction} and \textit{application} in the $\lambda$-calculus:
\begin{bnfgrammar}
t ::=
x : \textcolor{grey}{Variable}
| $\lambda$x.t : \textcolor{grey}{Abstraction}
| t, t : \textcolor{grey}{Application}
\end{bnfgrammar}
The symbol \texttt{t} in the left-hand side of the rules is called a \textit{metavariable}. It is a place-holder for some particular term.
\subsection{Types}
\subsection{Kinds}
\begin{question}{To treat type-level functions, collectively called \textit{type operators} more formally, it is required to:}
\begin{enumerate}
\setlength\itemsep{-.3em}
\item Add a collection of rules of \textit{kinding} which specify how type expressions can be combined to yield new type expressions.
\item Whenever a type T appears in a term ($\lambda x:\text{T}.t$), check whether T is well formed.
\item Add a collection of rules for the definitonal equivalence relations between types.
\end{enumerate}
\end{question}
$\Gamma \vdash \text{T}::\text{K}$ is read as \say{type T has kind K in context $\Gamma$}.
% basic mechanisms of \textcolor{red}{abstraction} and \textcolor{red}{application} at the level of types.
% Precisely define when two type expressions should be regarded as equivalent.
\textit{kinding} is a well-formedness relation.
% \begin{grammar}[$\lambda$-calculus syntax][t][gr:grammar1]
% \firstcase{\mathit{t}}{\mathit{x}}{Variable}
% \otherform{\lambda x. \mathit{t}}{Abstraction}
% \otherform{(\mathit{t}, \mathit{t})}{Application}
% \end{grammar}