Commit 0d323ff4 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

few rewordings ...

parent 360e6fb8
......@@ -486,7 +486,7 @@ We introduce the new syntactic category of \emph{types schemes} which are the te
\textbf{Type schemes} & \ts & ::= & t \alt \tsfun {\arrow t t ; \cdots ; \arrow t t} \alt \ts \tstimes \ts \alt \ts \tsor \ts \alt \tsempty
\end{array}
\]
type schemes denote sets of type, as formally stated by the following definition:
Type schemes denote sets of types, as formally stated by the following definition:
\begin{definition}[Interpretation of type schemes]
We define the function $\tsint {\_}$ that maps type schemes into sets of types.
\begin{align*}
......@@ -506,7 +506,7 @@ type schemes denote sets of type, as formally stated by the following definition
\end{definition}
Note that $\tsint \ts$ is closed under subsumption and intersection
(straightforward induction) and that $\tsempty$, which denotes the
empty set of types is different from $\empty$ whose interpretation is
empty set of types is different from $\Empty$ whose interpretation is
the set of all types.
\begin{lemma}
......@@ -524,14 +524,14 @@ the value. By induction on the definition of values: $\tyof c {} =
{v_1}{}\tstimes\tyof {v_1}{}$. Then we have $v\in t\iffdef \tyof
v{}\leq t$.
We also need to perform intersections of type schemes so as to intersect the static type of an expression with the one deduced by occurrence typing. For our algorithmic system (see \Rule{Env$_{\scriptscriptstyle\mathcal{A}}$} in Section~\ref{sec:algorules}) all we need to define is the intersection of a type with a type scheme:
We also need to perform intersections of type schemes so as to intersect the static type of an expression (\emph{ie}, the one deduced by conventional rules) with the one deduced by occurrence typing (\emph{ie}, the one derived by $\vdashp$). For our algorithmic system (see \Rule{Env$_{\scriptscriptstyle\mathcal{A}}$} in Section~\ref{sec:algorules}) all we need to define is the intersection of a type scheme with a type:
\begin{lemma}
Let $\ts$ be a type scheme and $t$ a type. We can compute a type scheme, written $t \tsand \ts$, such that
\(\tsint {t \tsand \ts} = \{s \alt \exists t' \in \tsint \ts.\ t \land t' \leq s \}\)
\end{lemma}
\beppe{Do we need the next definition or it can go in the appendix?
\beppe{Do we need the next definition or it can go in the appendix?\\
Finally, given a type schema it is straightforward to choose in its interpretation a type which serves as the canonical representative of the set:
\begin{definition}[Representative]
We define a function $\tsrep {\_}$ that maps every non-empty type scheme into a type, \textit{representative} of the set of types denoted by the scheme.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment