In this work we presented to core of our analysis of occurrence

typing, extended it to record types and a proposed a couple of novel

applications of the theory, namely the inference of

applications of the theory, namely the inference of

intersection types for functions and a static analysis to reduce the number of

casts inserted when compiling gradually-typed programs.

One of the by products of our work is the ability to define type

predicates such as those used in \cite{THF10} as plain function and

have the inference procedure deduce automatically the correct

overloaded function type.

There is still a lot of work to do to fill the gap with real-word

programming languages. Some of it should be quite routine such as the

encoding of specific language constructions (e.g., \code{isInt},

\code{typeof},...), the handling of more complex

handling of more complex

kinds of checks (e.g., generic Boolean expression, multi-case

type-checks) and even encompass sophisticated type matching as the one

performed by the language CDuce. Some other will require more

performed by the CDuce language. Some other will require more

work. For example, our analysis cannot handle flow of information. In

particular, the result of a type test can flow only to the branches

but not outside the test. As a consequence the current system cannot

...

...

@@ -20,18 +23,20 @@ type a let binding such as

\end{alltt}

which is clearly safe when $y:\Int\vee\Bool$. Nor can this example be solved by partial evaluation since we do not handle nesting of tests in the condition\code{( ((y\(\in\)Int)?`yes:`no)\(\in\)`yes )? y+1 : not(y)},

and both are issues that system by~\citet{THF10} can handle. We think that it is possible

to reuse some of their ideas to perform a information flow analysis on the top of

to reuse some of their ideas to perform a information flow analysis on top of

our system to remove these limitations.

%

Information flow analysis would also be useful to improve

inference of intersection types presented in

Section~\ref{sec:refining}: there we said that type cases in the body of a

function are the tipping points that may change the type of the result

of the function; but they are not the only ones, the other being the

applications of overloaded functions. Therefore we plan to

detect the overloaded functions the parameter of an outer function

flows to, so as to use the partition of their domains to perform a

finer grained analysis of the outer function's type.

Some of the exensions we hinted to in Section~\ref{sec:practical}

warrant a formal treatment. In particular, the rule [{\sc OverApp}]

only detects the application of an overloaded function once, when

type-checking the body of the function against the coarse input type

(that is, $\psi$ is computed only once). But we could repeat this

process whilst type-checking the inferred arrows (that is we would

enrich $\psi$ while using it to find the various arrow types of the

lambda abstraction). Clearly, if untamed, such a process may never

reach a fix point. Studying whether this iterative refining can be

made to converge, and foremost whether it is of use in practice is one

of our objectives.

But the real challenges that lie ahead are the handling of side

effects and the addition of polymorphic types. Our analysis works in a