Commit 347243be authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Correction to the rule [OverApp]

parent 8f323cb2
......@@ -142,7 +142,7 @@ url={http://www.cduce.org/papers/frisch_phd.pdf}
In this work I reexamine the result of that article in the light of recent advances in (sub-)typing theory and programming languages, taking a fresh look at this old issue.
Actually, the revamping of this problem is just an excuse for writing an essay that aims at explaining sophisticated type-theoretic concepts, in simple terms and by examples, to undergraduate computer science students and/or willing functional programmers.
Finally, I took advantage of this opportunity to describe some undocumented advanced techniques of type-systems implementation that are known only to few insiders that dug in the code of some compilers: therefore, even expert language designers and implementers may find this work worth of reading.},
note = {(Revised edition: first version 2013). To appear. \url{https://arxiv.org/abs/1809.01427}.},
note = {(Revised version: first version 2013). To appear. \url{https://arxiv.org/abs/1809.01427}.},
year = {2019},
annote = {types,ool,new},
}
......
......@@ -156,17 +156,17 @@ the following rule\\[1mm]
{ \Gamma \vdash\textstyle
{e}{~x}\triangleright\psi_1\cup\psi_2\cup\bigcup_{i\in I}\{
x\mapsto t\wedge t_i\} }
{}
{(t\wedge t_i\not\simeq\Empty)}
\)}\\
Whenever a function parameter is the argument of an
overloaded function, we record as possible types for this parameter
all the possible domains of the arrows that type the overloaded
function, restricted by the static type of the parameter. In Code~9,
since, \texttt{or\_} has type\\[.7mm]
all the domains $t_i$ of the arrows that type the overloaded
function, restricted (via intersection) by the static type $t$ of the parameter and provided that the type is not empty ($t\wedge t_i\not\simeq\Empty$). In Code~9,
since \texttt{or\_} has type\\[.7mm]
\centerline{$(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land
(\lnot\True\to\lnot\True\to\False)$}\\[.7mm]
We consider \True, \Any, and $\lnot\True$ as candidate types for
\texttt{x} which, in turn allows us to deduce a precise type given in the table. Finally, thanks to this rule it is no longer necessary to use a type case to force refinement. As a consequence we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as:
then \True, \Any, and $\lnot\True$ become candidate types for
\texttt{x} and this allows us to deduce the precise type given in the table. Finally, thanks to this rule it is no longer necessary to use a type case to force refinement. As a consequence we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as:
\begin{alltt}\color{darkblue}\morecompact
let and_ = fun (x : Any) -> fun (y : Any) -> not_ (or_ (not_ x) (not_ y))
let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y))
......
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