Commit 5c8f13e8 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

started organizing extension

parent 655397e2
\subsection{Adding structured types}
The previous analysis already covers a large pan of realistic cases. For instance, the analysis already works for list data structures since products and recursive type are enough is enough to encode them as right associative nested pairs, as it is done in the language CDuce~\cite{BCF03} (e.g., $X = \textsf{Nil}\vee(\Int\times X)$ is the type of the lists of integers). And even more since the presence of union types makes it possible to type heterogeneous lists whose content is described by regular expressions on types as proposed by~\citet{hosoyapierce}.
First thing we add a new type constructor for products.
We add to types the following production
\textbf{Types} & t & ::= & \pair t t
to those of Definition~\ref{def:types} and we relax contractivity by that every infinite branch contains an infinite number of occurrences of the arrow or product type constructors.
We also modify subtyping ...
The largest product type is $\pair\Any\Any$ and it denotes the set of all pairs of well-typed values
We also add two operators for the new product type constructor, the right and left projection respectively denoted by $\bpi_{\boldsymbol 1}$ and $\bpi_{\boldsymbol 2}$ and defined as follows.
Let $t$ be a product type (i.e., $t\leq\pair\Any\Any$) then:
\bpl t & = & \min \{ u \alt t\leq \pair u\Any\}\\
\bpr t & = & \min \{ u \alt t\leq \pair \Any u\}
We add to expressions the terms for pairs and projections:
\textbf{Expressions} & e & ::= & \pi_1 e\alt \pi_2 e \alt (e,e)
We enrich paths to distinguish uniquely the expression they are applied to (this simplifies the following definitions). So besides $0$ and $1$ we will have steps towards $l$eft, $r$ight, $f$irst, and $s$econd.
Let $e$ be an expression and $\varpi\in\{0,1,l,r,f,s\}^*$ a \emph{path}; we denote $\occ e\varpi$ the occurrence of $e$ reached by the path $\varpi$, that is
e&\epsilon & e\\
e_0e_1& i.\varpi & \occ{e_i}\varpi\qquad i=0,1\\
(e_0,e_1)& l.\varpi & \occ{e_0}\varpi\\
(e_0,e_1)& r.\varpi & \occ{e_1}\varpi\\
\pi_1 e& f.\varpi & \occ{e}\varpi\\
\pi_2 e& s.\varpi & \occ{e}\varpi\\
undefined otherwise
Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0,1\}^*$ and $p\in\{+,-\}$, we extend $\typep p \varpi {\Gamma,e,t}$ as follows
\typep{p}{\varpi.l}{\Gamma,e,t} & = & \bpl{\Gp p {\Gamma,e,t} (\varpi)}\\
\typep{p}{\varpi.r}{\Gamma,e,t} & = & \bpr{\Gp p {\Gamma,e,t} (\varpi)}\\
\typep{p}{\varpi.f}{\Gamma,e,t} & = & \pair{\Gp p {\Gamma,e,t} (\varpi)}\Any\\
\typep{p}{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\Gp p {\Gamma,e,t} (\varpi)}\\ \\
\Gp p {\Gamma,e,t}(\varpi) &=& \typep p \varpi{\Gamma,e,t} \wedge \tyof {\occ e\varpi}\Gamma
and extend the previous definitions $\Gp p {\Gamma,e,t}(\varpi)$ and
$\Gamma^p_{\Gamma,e,t}$ to the new paths. The reason why in the
definition of $\typep{p}{\varpi.l}{\Gamma,e,t}$ and
$\typep{p}{\varpi.l}{\Gamma,e,t}$ we intersected $\typep p
\varpi{\Gamma,e,t}$ with $\pair\Any\Any$ is to ensure that the
operators $\bpl{}$ and $\bpr{}$ are defined. It handles the (admitedly
stupid) cases in which an \texttt{if} tests whether a pair has a type
which contains values other than pairs, such as for instance
$$\ite {(x,y)}{((\pair\Int\Int)\vee(\Int\to\Bool))}{...}{...},$$
thus deducing the type $\Int$ for the occurrences of $x$ and $y$ in the \texttt{then} branch.
All it remains to do is to add the typing rules for the new expressions:
{\Gamma \vdash e:t\and t\leq\pair\Any\Any}
{\Gamma \vdash \pi_i e:\bpi_{\mathbf{i}}(t)}
{\pi_i e\not\in\dom\Gamma}
{\Gamma \vdash e_1:t_1 \and \Gamma \vdash e_2:t_2}
{\Gamma \vdash (e_1,e_2):\pair{t_1}{t_2}}
As an example one can consider TODO
Finally, for what concerns the algorithmic part, the operators $\bpi_{\boldsymbol 1}$ and $\bpi_{\boldsymbol 2}$ are standard in the semantic subtyping framework and they can be computed as described by~\citet{} (see also~\citep[\S4.4.1]{Cas15} for a detailed description, in particular formulae (4.20) and (4.21))
\subsubsection{Lists} The work above on pairs is enough for having also the lists. It suffices to encode them as right associative nested pairs, as it is done in the language CDuce. The interesting part is that thanks to the presence of union and recursive types one can type heterogeneous lists whose content is described by regular expressions on types as proposed by~\citet{hosoyapierce}.
Since the main application of occurrence typing is to type dynamic languages, then what is really missing are record types.
Compare with path expressions of ~\citet{THF10}
\beppe{Compare with path expressions of ~\citet{THF10} }
First of all, we define:
......@@ -587,7 +587,7 @@ We need similar operators for projections since the type $t$ of $e$ in $\pi_i e$
All the operators above but $\worra{}{}$ are already present in the
theory of semantic subtyping: the reader can find how to compute them
and how to extend their definition to type schemes in~\cite[Section
6.11]{Frisch2008}. Below we just show the formula that computes
6.11]{Frisch2008} (see also~\citep[\S4.4]{Cas15} for a detailed description). Below we just show the formula that computes
$\worra t s$ for a $t$ subtype of $\Empty\to\Any$. For that, we use a
result of semantic subtyping that states that every type $t$ is
equivalent to a type in disjunctive normal form and that if
......@@ -49,6 +49,18 @@ author = "Wright, Andrew K. and Felleisen, Matthias",
keywords = {scheme, type systems},
AUTHOR = {V. Benzaken and G. Castagna and A. Frisch},
TITLE = {{CD}uce: an {XML}-Centric General-Purpose Language},
BOOKTITLE = {ICFP~'03, 8th ACM International Conference on Functional Programming},
PAGES ={51--63},
ADDRESS = {Uppsala, Sweden},
DMI-CATEGORY = {intc},
YEAR = {2003},
author = {Frisch, Alain and Castagna, Giuseppe and Benzaken, V{\'e}ronique},
title = {Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation 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