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

started new version of section 2

parent be84e325
......@@ -3,14 +3,14 @@
\begin{definition}[Type syntax]\label{def:types} The set of types are the terms $t$ coinductively produced by the following grammar
\[
\begin{array}{lrcl}
\textbf{Types} & t & ::= & b\alt t\to t\alt t\vee t \alt \neg t \alt \Empty
\textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty
\end{array}
\]
and that satisfy the following conditions
\begin{itemize}
\item (regularity) the term has a finite number of different sub-terms;
\item (contractivity) every infinite branch of a type contains an infinite number of occurrences of the
arrow type constructor.
arrows or product type constructors.
\end{itemize}
\end{definition}
We introduce the following abbreviations for types: $
......
In this section
In this section we present the formalization of the ideas we hinted in the introduction. We start by the definitions of types. Next we define the language and its reduction semantics. The static semantics is the core of our presentation: we first present a declarative types system which deduces for every well-typed expressions several types and then the algorithms that allow us to decide well typedness.
\subsection{Types}
\begin{definition}[Type syntax]\label{def:types} The set of types \types{} are the terms $t$ coinductively produced by the following grammar
\[
\begin{array}{lrcl}
\textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty
\end{array}
\]
and that satisfy the following conditions
\begin{itemize}
\item (regularity) the term has a finite number of different sub-terms;
\item (contractivity) every infinite branch of a type contains an infinite number of occurrences of the
arrow type constructor.
\end{itemize}
\end{definition}
We use the following abbreviations for types: $
t_1 \land t_2 \eqdef \neg (\neg t_1 \vee \neg t_2)$,
$t_ 1 \setminus t_2 \eqdef t_1 \wedge \neg t_2$, $\Any \eqdef \neg \Empty$.
In the definition, $b$ ranges over basic types
(\emph{eg}, \Int, \Bool),
$\Empty$ and $\Any$ respectively denote the empty (that types no value)
and top (that types all values) types. Coinduction accounts for
recursive types and the condition on infinite branches bars out
ill-formed types such as
$t = t \lor t$ (which does not carry any information about the set
denoted by the type) or $t = \neg t$ (which cannot represent any
set).
It also ensures that the binary relation $\vartriangleright
\,\subseteq\!\types^{2}$ defined by $t_1 \lor t_2 \vartriangleright
t_i$, $t_1 \land t_2 \vartriangleright
t_i$, $\neg t \vartriangleright t$ is Noetherian.
This gives an induction principle on $\types$ that we
will use without any further explicit reference to the relation.
We refer to $ b $, $\times$, and $ \to $ as \emph{type constructors}
and to $ \lor $, $ \land $, $ \lnot $, and $ \setminus $
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 more details. Its formal definition is recalled in Appendix~\ref{}.
For this presentation it suffices to consider that
types are interpreted as sets of \emph{values} ({\emph{ie}, either
constants, $\lambda$-abstractions, or pair of values: see
Section~\ref{}) that have that type, and that subtyping is set
containment (\emph{ie}, a type $s$ is a subtype of a type $t$ if and only if $t$
contains all the values of type $s$). In particular, $s\to t$
contains all $\lambda$-abstractions that when applied to a value of
type $s$, if the computation terminates, then they return a result of
type $t$ (\emph{eg}, $\Empty\to\Any$ is the set of all
functions\footnote{\label{allfunctions}Actually, for every type $t$,
all types of the form $\Empty{\to}t$ are equivalent and each of them
denotes the set of all functions.} and $\Any\to\Empty$ is the set
of functions that diverge on every argument). Type connectives
(\emph{ie}, union, intersection, negation) are interpreted as the
corresponding set-theoretic operators (\emph{eg},~$s\vee t$ is the
union of the values of the two types).
\subsection{Syntax}\label{sec:syntax}
The expressions $e$ and values $v$ of our language are the terms inductively generated by the following grammars:
\begin{equation}\label{expressions}
\begin{array}{rclr}
e &::=& c\alt x\alt ee\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt \pi_i e\alt(e,e)\alt\tcase{e}{t}{e}{e}\\
v &::=& c\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt (v,v)
\end{array}
\end{equation}
for $i=1,2$. In~\eqref{expressions}, $c$ ranges over constants
(\emph{eg}, \texttt{true}, \texttt{false}, \texttt{1}, \texttt{2},
...) which are values of basic types (we use $\basic{c}$ to denote the
basic type of the constant $c$); $x$ ranges over variables; $(e,e)$
denote pairs and $\pi_i e$ their projections; $\tcase{e}{t}{e_1}{e_2}$
denotes the type-case expression that evaluates either $e_1$ or $e_2$
according to whether the value returned by $e$ (if any) is of type $t$
or not; $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ is a value of type
$\wedge_{i\in I}s_i\to t_i$ and denotes the function of parameter $x$
and body $e$. An expression has an intersection type if and only if it
has all the types that compose the intersection. Therefore,
intuitively, $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ is a well-typed
value if for all $i{\in} I$ the hypothesis that $x$ is of type $s_i$
implies that the body $e$ has type $t_i$, that is to say, it is well
typed if $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ has type $s_i\to
t_i$ for all $i\in I$. Every value is associated to a type: we said
described the types of constants and abstractions and, inductively,
the type of a pair of values is the product of the types of the
values.
\subsection{Syntax}
\subsection{Dynamic semantics}
uses type schemes?
The dynamic semantics is defined as a classic left-to-right reduction with pairs with a specific rule for type-cases. We have the following notions of reduction:
\[
\begin{array}{rcll}
(\lambda^{\wedge_{i\in I}s_i\to t_i} x.e)v &\reduces& e\subst x v\\
\pi_i(v_1,v_2) &\reduces& v_i & i=1,2\\
\tcase{v}{t}{e_1}{e_2} &\reduces& e_1 &v\in t\\
\tcase{v}{t}{e_1}{e_2} &\reduces& e_2 &v\not\in t\\
\end{array}
\]
The semantics of type-cases uses the relation $v\in t$ that we
informally defined in the previous section. We delay its formal
definition to Section~\ref{sec:type-schemes}. Context reductions are
defined by the following reduction contexts:
\[
\Cx[] ::= [\,]\alt \Cx e\alt v\Cx \alt (\Cx,e)\alt (v,\Cx)\alt \pi_i\Cx\alt \tcase{\Cx}tee
\]
As usual we denote by $\Cx[e]$ the term obtained by replacing $e$ for
the hole in the context $\Cx$ and we have that $e\reduces e'$ implies
$\Cx[e]\reduces\Cx[e']$.
\subsection{Static semantics}
......@@ -22,12 +120,12 @@ uses type schemes?
\item elimination rules (app, proj,if) ->operations on types and how to compute them
\item Compute the environments for occurrence typing. Algorith to compute $\Gamma\vdash\Gamma$
\item Compute the environments for occurrence typing. Algorithm to compute $\Gamma\vdash\Gamma$
\end{enumerate}
Next we can give the algorithmic typing rules
\subsubsection{Type schemes}
\subsubsection{Type schemes}\label{sec:type-schemes}
change the definition of typeof to take into account type-schemes for lambda abstractions
......
......@@ -177,6 +177,8 @@ Text of abstract \ldots.
\label{sec:language}
\input{language}
\section{NEW LANGUAGE}
\input{language2}
\section{Extensions}
\label{sec:extensions}
......
......@@ -45,7 +45,9 @@
{#2}{#3}}
\newcommand {\Rule}[1] {[\textsc{#1}]}
\newcommand{\tcase}[4]{\ensuremath{#1{\in}#2\,\texttt{\textup{?}}\,#3\,\texttt{\textup{:}}\,#4}}
\newcommand{\types}{\textbf{Types}}
\newcommand{\occ}[2]{#1{\downarrow}#2}
\newcommand{\basic}[1]{\text{\fontshape{\itdefault}\fontseries{\bfdefault}\selectfont b}_{#1}}
\newcommand{\tyof}[2]{\textsf{typeof}_{#2}(#1)}
......@@ -71,11 +73,11 @@
}{}
\DeclareSymbolFont{mathb}{U}{mathb}{m}{n}
\DeclareMathSymbol{\sqdot}{\mathbin}{mathb}{"0D}% name to be checked
\newcommand{\Cx}{\mathcal{C}}
\newcommand{\worra}[2]{#1\mathop{\,\sqdot\,} #2}
\newcommand{\apply}[2]{#1\circ#2}
\newcommand {\Empty} {\textsf{Empty}}%\MyMathBb{0}}
\newcommand {\Any} {\textsf{Any}}%\MyMathBb{1}}
\newcommand {\Empty} {\ensuremath{\MyMathBb{0}}}
\newcommand {\Any} {\ensuremath{\MyMathBb{1}}}
\newcommand {\dom}[1]{\textsf{dom}(#1)}
\newcommand {\Keyw} [1] {\text{\textsf{#1}}}
\newcommand {\False} {\Keyw{False}}
......@@ -124,6 +126,7 @@
\newcommand{\cons}[2]{{#1}\textsf{::}{#2}}
\newcommand{\fixpoint}{\textsf{gfp}}
\newcommand{\reduces}{\leadsto}
\newcommand{\xleadsto}[1]{\overset{#1}{\leadsto}}
\newcommand{\idleadsto}[0]{\xleadsto{Id}}
\newcommand{\values}[0]{\mathcal{V}}
......
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