Commit 8f323cb2 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Small typos and formatting

parent 06fabd3b
......@@ -19,7 +19,7 @@ let any_inf = fun (x : Any) ->
if x is Int then incr x else
if x is Bool then lnot x else x
\end{lstlisting} &\vfill
$(\Int\to\Int)\land(\lnot\Int\to\lnot\Int)\land$\newline
$(\Int\to\Int)\land(\lnot\Int\to\lnot\Int)\;\land$\newline
$(\Bool\to\Bool)\land(\lnot(\Int\vee\Bool)\to\lnot(\Int\vee\Bool))$\\
\hline
......@@ -53,7 +53,7 @@ let or_ = fun (x : Any) -> fun (y: Any) ->
else if y is True then true else false
\end{lstlisting}
&\smallskip\vfill
$(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land$\newline
$(\True\to\textsf{Any}\to\True)\land(\textsf{Any}\to\True\to\True)\;\land$\newline
$(\lnot\True\to\lnot\True\to\False)$
\\\hline
6 &
......@@ -64,7 +64,7 @@ let and_ = fun (x : Any) -> fun (y : Any) ->
\end{lstlisting}
&\vfill
$(\True\to((\lnot\True\to\False)\land(\True\to\True))$\newline
$ \land(\lnot\True\to\Any\to\False)$
$ \land(\lnot\True\to\textsf{Any}\to\False)$
\\\hline
7 &
\begin{lstlisting}
......@@ -139,7 +139,7 @@ $(\lnot\True\to((\True\to\True) \land (\lnot\True\to\False))$
let example10 = fun (x : Any) ->
if (f x, g x) is (Int, Bool) then 1 else 2
\end{lstlisting} &\vfill
\end{lstlisting} &\vfill\medskip\smallskip
$(\Int\to\textsf{Empty})\land(\neg\Int\to{}2)$\newline
\texttt{Warning: line 4, 39-40: unreachable expression}
\\\hline
......
......@@ -21,7 +21,7 @@ provide the semantic subtyping machinery. Besides a type-checking
algorithm defined on the base language, our implementation supports
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
consist of 2000 lines of OCaml code, including parsing, type-checking
consists of 2000 lines of OCaml code, including parsing, type-checking
of programs, and pretty printing of types. We demonstrate the output of
our type-checking implementation in Table~\ref{tab:implem}. These
examples and others can be tested in the online toplevel available at
......@@ -50,7 +50,7 @@ the first two arrows $(\Int\to\Int)\land(\Bool\to\Bool)$, and since
the union of their domain exactly covers the domain of the third arrow,
the latter is not needed. Code~2 shows what happens when the argument
of the function is left unannotated (i.e., it is annotated by the top
type \Any, written \texttt{Any} in our implementation). Here
type \Any, written ``\texttt{Any}'' in our implementation). Here
type-checking and refinement also work as expected, but the function
only type checks if all cases for \texttt{x} are covered (which means
that the function must handle the case of inputs that are neither in \Int{}
......
......@@ -6,7 +6,7 @@ As we explained in the introduction, both TypeScript and Flow deduce the type
\end{equation}
can be deduced by these languages only if they are instructed to do so: the
programmer has to explicitly annotate \code{foo} with the
type \eqref{tyinter}: we did it in \eqref{foo2} using Flow---the TypeScript annotation for it is much hevier. But this seems like overkill, since a simple
type \eqref{tyinter}: we did it in \eqref{foo2} using Flow---the TypeScript annotation for it is much heavier. But this seems like overkill, since a simple
analysis of the body of \code{foo} in \eqref{foo} shows that its execution may have
two possible behaviors according to whether the parameter \code{x} has
type \code{number} or not (i.e., or \code{(number$\vee$string)$\setminus$number}, that is \code{string}), and this is
......
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