Commit 19db38a8 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

added subtyping

parent 7300f7a4
......@@ -224,7 +224,7 @@ then
that is the union of all the possible
input types, while the precise return type of such a
function depends on the type of the argument the function is applied to:
either an integer, or a string, or both (i.e., the argument has union type
either an integer, or a string, or both (i.e., the union type
\(\Int\vee\String\)). So we have \( t_1 \circ \Int = \Int \),
\( t_1 \circ \String = \String \), and
\( t_1 \circ (\Int\vee\String) = \Int \vee \String \) (see Section~\ref{sec:typeops} for the formal definition of $\circ$).
......
......@@ -42,7 +42,8 @@ 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. A detailed description of the algorithm to decide it can be found in~\cite{Cas15}.
by~\citet{Frisch2008} to which the reader may refer for the formal
definition (see~\cite{types18post} for a simpler alternative definition). A detailed description of the algorithm to decide it can be found in~\cite{Cas15}.
For this presentation it suffices to consider that
types are interpreted as sets of \emph{values} ({i.e., either
constants, $\lambda$-abstractions, or pairs of values: see
......
......@@ -189,6 +189,24 @@ Finally, I took advantage of this opportunity to describe some undocumented adva
}
@InProceedings{types18post,
author = {Tommaso Petrucciani and Giuseppe Castagna and Davide Ancona and Elena Zucca},
title = {Semantic subtyping for non-strict languages},
DMI-CATEGORY = {intc},
FILE = {types18post.pdf},
series ={Leibniz International Proceedings in Informatics (LIPIcs)},
volume ={130},
pages = {4:1--4:24},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11408},
URN = {urn:nbn:de:0030-drops-114083},
doi = {10.4230/LIPIcs.TYPES.2018.4},
publisher ={Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
year = 2019,
}
@inproceedings{siek2006gradual,
title={Gradual typing for functional languages},
author={Siek, Jeremy G and Taha, Walid},
......
......@@ -297,6 +297,11 @@ The authors thank Paul-André Melliès for his help on type ranking.
%% Appendix
\appendix
\section{Definition of the Subtyping Relation}
\label{sec:subtyping}
\input{subtyping}
\section{Proof of Type Soundness}
\label{sec:proofs}
\input{proofs}
......
......@@ -6,14 +6,14 @@
% Packages
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\let\Bbbk\relax
\usepackage{amsmath}
%\usepackage{amsmath}
\usepackage{mathtools}
\usepackage{amssymb}
\usepackage{amsthm}
%\usepackage{amssymb}
%\usepackage{amsthm}
\usepackage{alltt}
\usepackage{bm}
\usepackage{nicefrac}
\usepackage{stmaryrd}
%\usepackage{stmaryrd}
\usepackage{mathpartir}
\usepackage{color}
\usepackage{listings}
......@@ -62,6 +62,17 @@
\newcommand{\tcase}[4]{\ensuremath{(#1{\in}#2)\,\texttt{\textup{?}}\,#3\,\texttt{\textup{:}}\,#4}}
\newcommand{\morecompact}{\baselineskip=9.5pt}
\newcommand {\Pd} {\mathcal{P}}
\newcommand {\Pf} {\mathcal{P}_{\!\textup{fin}}}
\newcommand {\Domain} {\mathcal{D}}
\newcommand {\Constants} {\mathcal{C}}
\newcommand {\TypeInter}[1] {\llbracket #1 \rrbracket}
\def\dbar{{\mkern3mu\mathchar'26\mkern-7mu\raisebox{-.7pt}{$\mathchar'26$}\mkern-11mu d}}
\newcommand {\domega} {\dbar} %possibilities: \dbar \dh \dj \delta
\newcommand {\Set}[1] {\{#1\}}
\newcommand {\ConstantsInBasicType} {\mathbb{B}}
\newcommand{\tauUp}{\tau^\Uparrow}
\newcommand{\sigmaUp}{\sigma^\Uparrow}
\newcommand{\types}{\textbf{\textup{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