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

last example of TH

parent a13c7518
......@@ -357,8 +357,45 @@ Table~\ref{tab:implem2}, type that is equivalent to $\Int\vee\String \to ((\Int,
Lifting this limitation through a control-flow
analysis is part of our future work.
\rev{%%%
In our system, however, it is possible to express dependencies between
different arguments of a function by uncurrying the function and typing its
arguments by a union of products. To understand this point, consider this
simple example:}
\begin{alltt}\color{darkblue}
let sum = fun (x : Int|String) -> fun (y : Int|String) ->
if x is String then concat x y else add x y
\end{alltt}
\rev{%%%
The definition above does not type-check in any system, and rightly
does so since nothing ensures
that \code{x} and \code{y} will be either both strings (so
that \code{concat} does not fail) or both integers (so that \code{add}
does not fail). It is however possible to state this dependency
between the type of the two arguments by
uncurring the function and using a union type:
}%%%rev
\begin{alltt}\color{darkblue}
let sum = fun (x : (Int,Int)|(String,String))
if fst x is String then concat(fst x)(snd x) else add(fst x)(snd x)
\end{alltt}
\rev{%%%
this function type-checks in our system (and, of course, in Typed
Racket as well) but the corresponding type-annontated version in JavaScript
}%%%rev
\begin{alltt}\color{darkblue}
function sum (x : [string,string]|[number,number]) \{
if (typeof x[0] === "string") \{
return x[0].concat(x[1]);
\} else \{
return x[0] + x[1];
\}
\}
\end{alltt}
\rev{%%%%
is rejected both by Flow and TypeScript since their type analyses fail to detect the
dependency of the types of the two projections.
}%%%rev
Although these experiments are still preliminary, they show how the
combination of occurrence typing and set-theoretic types, together
......
......@@ -27,6 +27,7 @@
\newcommand {\True} {\Keyw{True}}
\newcommand {\Int} {\Keyw{Int}}
\newcommand {\Bool} {\Keyw{Bool}}
\newcommand {\String} {\Keyw{String}}
\newcommand {\Empty} {\Keyw{Empty}}
\newcommand {\Domain} {\ensuremath{\mathcal{D}}}
\newcommand{\tobecut}[1]{{\color{lightgray}[\textsf{To be cut:} #1]}}
......@@ -443,22 +444,40 @@ set of types for \texttt{x} will be \texttt{String,\ Number}, but for
on page 27, a redundant test will make inference succeed.
\begin{answer}
Beppe: je ne sais pas comment gerer cette remarque. Est-ce
Typed-Racket fait mieux que nous. Si type les parametres avec
Int|String je pense que on n'est pas sorti de l'auberge. Si on type
avec (Int,Int)|(String,String) ca marche mais il faut typer la
paire. La seule solution qui ne demande pas de réécrire la fonction
est de inferer comme nous faison dans le nouveau papier.
@Mickael, check what happens in Typed Racket.
@STH. We are not sure we understand this point. It seems that if we
do not want to rewrite the whole function (using a single argument
that we could type as \texttt{(Int,Int)$\lor$(String,String)} is to either to have an
inference for the non-annotated function able to infer the
intersection type, or explicitly annotate the function with the
intersection type. And this in whatever system on considers,
e.g. Typed Racket, Flow, TypeScript ...
We apologize but we are not sure to completely understand the point
that the reviewer is trying to raise with this example. It seems to us
that the example above works in the same way for all existing
approaches, Typed Racket, Flow, Typescript, and ours.
The ideal situation would be a system that were able to deduce for the
function above the type
$((\String,\String)\to\String)\land((\Int,\Int)\to\Int)$ but even our
system (the only one that can reconstruct intersection types for
functions) cannot do it.
If we explicitly annotate the function with this intersection type
then the function type-checks in all systemes.
If we rewrite the function so that it has a single argument of type
\texttt{(Int,Int)$\lor$(String,String)}, that is
\begin{verbatim}
function (x : [string,string]|[number,number]) {
if (typeof x[0] === "string") {
return x[0].concat(x[1]);
} else {
return x[0] + x[1];
}
}
\end{verbatim}
then again it type checks in our system, in Typed Racket, but it fails in
Flow and in TypeScript.
So we do not really understand the purpose of the example, unless to
show an example that works in Typed Racket and our system work but not
in TypeScript and Flow. In the case that this were the correct
interpretation of the reamark of the reviewer,we added a comment in
lines ???-???
\end{answer}
......
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