Commit 26fbc9c0 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

rewording

parent 082e483e
...@@ -68,6 +68,6 @@ positive branch the types of $x_1$, of $x_2$, and of $x_1x_2$ by applying $\sigm ...@@ -68,6 +68,6 @@ positive branch the types of $x_1$, of $x_2$, and of $x_1x_2$ by applying $\sigm
idea is clear (see Appendix~\ref{app:roadmap} for a more detailed explanation), idea is clear (see Appendix~\ref{app:roadmap} for a more detailed explanation),
the technical details are quite involved, especially when considering the technical details are quite involved, especially when considering
functions typed by intersection types and/or when integrating gradual functions typed by intersection types and/or when integrating gradual
typing. This deserves a whole pan of non trivial research that we plan to typing. This needs a whole gamut of non trivial research that we plan to
develop in the near future. develop in the near future.
...@@ -92,7 +92,7 @@ other words, if a function expects an argument of type $\tau$ but can be ...@@ -92,7 +92,7 @@ other words, if a function expects an argument of type $\tau$ but can be
typed under the hypothesis that the argument has type $\tauUp$, then no casts typed under the hypothesis that the argument has type $\tauUp$, then no casts
are needed, since every cast that succeeds will be a subtype of are needed, since every cast that succeeds will be a subtype of
$\tauUp$. Taking advantage of this property, we modify the rule for $\tauUp$. Taking advantage of this property, we modify the rule for
functions as: functions as: \vspace{-2mm}
% %
%\begin{mathpar} %\begin{mathpar}
% \Infer[Abs] % \Infer[Abs]
...@@ -115,7 +115,7 @@ functions as: ...@@ -115,7 +115,7 @@ functions as:
} }
{ {
\Gamma\vdash\lambda x:\sigma'.e:\textstyle\bigwedge_{(\sigma,\tau) \in T}\sigma\to \tau \Gamma\vdash\lambda x:\sigma'.e:\textstyle\bigwedge_{(\sigma,\tau) \in T}\sigma\to \tau
} }\vspace{-2mm}
\] \]
The main idea behind this rule is the same as before: we first collect all the The main idea behind this rule is the same as before: we first collect all the
information we can into $\psi$ by analyzing the body of the function. We then information we can into $\psi$ by analyzing the body of the function. We then
......
...@@ -17,7 +17,7 @@ function but not whether it has a specific function type (\emph{cf.}, Footnote~\ ...@@ -17,7 +17,7 @@ function but not whether it has a specific function type (\emph{cf.}, Footnote~\
implementation becomes complete (see Corollary~\ref{app:completeness} in the appendix for a formal proof). implementation becomes complete (see Corollary~\ref{app:completeness} in the appendix for a formal proof).
Our implementation is written in OCaml and uses CDuce as a library to Our implementation is written in OCaml and uses CDuce as a library to
provide the semantic sub-typing machinery. Besides a type-checking provide the semantic subtyping machinery. Besides a type-checking
algorithm defined on the base language, our implementation supports algorithm defined on the base language, our implementation supports
record types (Section \ref{ssec:struct}) and the refinement of function types record types (Section \ref{ssec:struct}) and the refinement of function types
(Section \ref{sec:refining} with the rule of Appendix~\ref{app:optimize}). The implementation is rather crude and (Section \ref{sec:refining} with the rule of Appendix~\ref{app:optimize}). The implementation is rather crude and
...@@ -25,8 +25,12 @@ consist of 2000 lines of OCaml code, including parsing, type-checking ...@@ -25,8 +25,12 @@ consist of 2000 lines of OCaml code, including parsing, type-checking
of programs, and pretty printing of types. We demonstrate the output of of programs, and pretty printing of types. We demonstrate the output of
our type-checking implementation in Table~\ref{tab:implem}. These our type-checking implementation in Table~\ref{tab:implem}. These
examples and others can be tested in the online toplevel available at examples and others can be tested in the online toplevel available at
\url{https://occtyping.github.io/} (the corresponding repository is \url{https://occtyping.github.io/}%
\ifsubmission
~(the corresponding repository is
anonymized). anonymized).
\else.
\fi
\input{code_table} \input{code_table}
In this table, the second column gives a code fragment and the third In this table, the second column gives a code fragment and the third
column the type deduced by our implementation. Code~1 is a column the type deduced by our implementation. Code~1 is a
...@@ -70,8 +74,8 @@ parameter by \Bool{} (which in CDuce is syntactic sugar for ...@@ -70,8 +74,8 @@ parameter by \Bool{} (which in CDuce is syntactic sugar for
\True$\vee$\False) yielding the type \True$\vee$\False) yielding the type
$(\True{\to}\False)\wedge(\False{\to}\True)$. $(\True{\to}\False)\wedge(\False{\to}\True)$.
The \texttt{or\_} connective (Code~5) is straightforward as far as the The \texttt{or\_} connective (Code~5) is straightforward as far as the
code goes, but we see that the overloaded type precisely capture all code goes, but we see that the overloaded type precisely captures all
the possible cases. Again we use a generalized version of the possible cases. Again we use a generalized version of the
\texttt{or\_} connective that accepts and treats any value that is not \texttt{or\_} connective that accepts and treats any value that is not
\texttt{true} as \texttt{false} and again, we could easily restrict the \texttt{true} as \texttt{false} and again, we could easily restrict the
domain to \Bool{} if desired. domain to \Bool{} if desired.
......
...@@ -33,7 +33,7 @@ Section~\ref{sec:practical}. Second, in our setting, {\em types\/} play ...@@ -33,7 +33,7 @@ Section~\ref{sec:practical}. Second, in our setting, {\em types\/} play
the role of formulæ. Using set-theoretic types, we can express the the role of formulæ. Using set-theoretic types, we can express the
complex types of variables without resorting to a meta-logic. This complex types of variables without resorting to a meta-logic. This
allows us to type all but two of their key examples (the notable allows us to type all but two of their key examples (the notable
exceptions being Example~8 and 14 which use the propagation of type exceptions being Example~8 and 14 in their paper, which use the propagation of type
information outside of the branches of a test). Also, while they information outside of the branches of a test). Also, while they
extend their core calculus with pairs, they only provide a simple {\tt extend their core calculus with pairs, they only provide a simple {\tt
cons?} predicate that allows them to test whether some value is a cons?} predicate that allows them to test whether some value is a
......
...@@ -59,7 +59,7 @@ ...@@ -59,7 +59,7 @@
\newcommand {\Rule}[1] {[\textsc{#1}]} \newcommand {\Rule}[1] {[\textsc{#1}]}
\newcommand{\tcase}[4]{\ensuremath{(#1{\in}#2)\,\texttt{\textup{?}}\,#3\,\texttt{\textup{:}}\,#4}} \newcommand{\tcase}[4]{\ensuremath{(#1{\in}#2)\,\texttt{\textup{?}}\,#3\,\texttt{\textup{:}}\,#4}}
\newcommand{\morecompact}{\baselineskip=2.8pt} \newcommand{\morecompact}{\baselineskip=9.5pt}
\newcommand{\tauUp}{\tau^\Uparrow} \newcommand{\tauUp}{\tau^\Uparrow}
\newcommand{\sigmaUp}{\sigma^\Uparrow} \newcommand{\sigmaUp}{\sigma^\Uparrow}
......
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