Commit fcb6bc73 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files


parent ea0d4a1a
......@@ -28,7 +28,7 @@ recursive) systems: one is the system to infer the type environments, whose
judgements are of the form $\Gamma\vdash e\triangleright
\{\Gamma_i\}_{i\in I}$; the other is the type inference system we
presented in Section~\ref{sec:static} which we modify/extend to
exploit the inference of $\Gamma\vdash e\triangleright
exploit the results of the inference of $\Gamma\vdash e\triangleright
\{\Gamma_i\}_{i\in I}$.
For what concerns the type inference system we have to modify the rule
......@@ -57,8 +57,7 @@ as \emph{type connectives}.
The subtyping relation for these types, noted $\leq$, is the one defined
by~\citet{Frisch2008} to which the reader may refer for the formal
definition (see~\citet{types18post} for a simpler alternative
definition that we recall in Appendix~\ref{sec:subtyping} for the
definition (we recall it in Appendix~\ref{sec:subtyping} for the
reader's convenience). A detailed description of the algorithm to
decide this relation can be found in~\cite{Cas15}.
For this presentation it suffices to consider that
......@@ -74,11 +74,10 @@ t_i$, $t_1 \land t_2 \vartriangleright
t_i$, $\neg t \vartriangleright t$ is Noetherian.
This gives an induction principle\footnote{In a nutshell, we can do
proofs and give definitions by induction on the structure of unions and negations---and, thus, intersections---but arrows, products, and basic types are the base cases for the induction.} on $\types$ that we
use combined with structural induction on $\Domain$ to give the following definition (due to~\citet{types18post}
and equivalent to but simpler than the definition in~\cite{Frisch2008}),
use combined with structural induction on $\Domain$ to give the following definition,
which validates these equalities.
\begin{definition}[Set-theoretic interpretation of types~\cite{types18post}]\label{def:interpretation-of-types}
\begin{definition}[Set-theoretic interpretation of types~\cite{Frisch2008}]\label{def:interpretation-of-types}
We define a binary predicate $ (d : t) $
(``the element $ d $ belongs to the type $t$''),
where $ d \in \Domain $ and $ t \in \types $,
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