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

added example for Kent work

parent 978f3f6d
......@@ -194,7 +194,7 @@ just \texttt{False} or \texttt{$\lnot$False}), but also it tries to
perform this analysis for all possible expressions (and not just for a
restricted set of expressions). For instance, we use the operator
worra also to refine the type of the function in an application (see
discussion in Section~\ref{sec:ideas} while in Kent's approach
discussion in Section~\ref{sec:ideas}) while in Kent's approach
the analysis of an application \texttt{f\,x} refines the properties of
the argument \texttt{x} but not of the function \texttt{f} (as our
approach does); and when such an application is the argument of a type
......@@ -206,6 +206,25 @@ propositions according to the truthy or false value of an expression,
but it does it only for a selected set of \emph{pure} expressions of
the language, to cope with the possible presence of side effects (and
applications do not belong to this set since they can be be impure).
That said the very fact of focusing on truthy vs.\ false results may
make Kent's analysis fail even for pure Boolean tests where it would
be expected to work---e.g., if a result must be true rather than just truthy. For example, consider
the polymophic function that when applied to two integers returns
whether they have the same parity and false
otherwise: \code{have\_same\_parity:$(\Int\To\Int\To\Bool)\land(\neg\Int\To\ANY\To\False)\land(\ANY\To\neg\Int\To\False)$}. We
can imagine to use this function to implicitly test whether two
arguments are both integers, as in the body of the following function:
}%%%rev
\begin{alltt}\color{darkblue}
let f = fun (x : Any) -> fun (y : Any) ->
if have\_same\_parity x y is True then add x y else 0
\end{alltt}
\rev{%%%
While our approach can correctly deduce for this function the type
$\ANY\To\ANY\To\Int$, Kent's approach fails to type check it since
to type the ``then'' branch requires to deduce that the
application \code{have\_same\_parity\,x} returns the constant
function \code{true} only if \code{x} is an integer.
Finally, Kent's approach inherits all the advantages and
disadvantages that the logical propositions approach has with respect
to ours (e.g., flow sensitive analysis vs.\ user defined type
......@@ -214,10 +233,6 @@ section.
}%%%rev
\rev{HERE STRESS THAT THE WORK ON SOLVERS IS IN THE SAME VEIN AS THE
WORK OF TYPED RACKET THAT TRACKS FOR EXPRESSIONS WHEN THEY RETURN
FALSE AND WHEN NOT.
}
Another direction of research related to ours is the one of semantic
types. In particular, several attempts have been made recently to map
types to first order formul\ae. In that setting, subtyping between
......
......@@ -124,6 +124,7 @@
}{}
\DeclareSymbolFont{mathb}{U}{mathb}{m}{n}
\DeclareMathSymbol{\sqdot}{\mathbin}{mathb}{"0D}% name to be checked
\newcommand{\To}{{\to}}
\newcommand{\Cx}{\mathcal{C}}
\newcommand{\worra}[2]{#1\mathop{\,\sqdot\,} #2}
\newcommand{\apply}[2]{#1\circ#2}
......@@ -134,6 +135,7 @@
\newcommand {\False} {\Keyw{False}}
\newcommand {\True} {\Keyw{True}}
\newcommand {\Int} {\Keyw{Int}}
\newcommand {\ANY} {\Keyw{Any}}
\newcommand {\Bool} {\Keyw{Bool}}
\newcommand {\Char} {\Keyw{Char}}
\newcommand {\Real} {\Keyw{Real}}
......
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