Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Giuseppe Castagna
occurrence-typing
Commits
98f0d787
Commit
98f0d787
authored
May 07, 2021
by
Giuseppe Castagna
Browse files
finished example 14
parent
4bdf9ce9
Changes
2
Hide whitespace changes
Inline
Side-by-side
code_table2.tex
View file @
98f0d787
...
...
@@ -72,7 +72,7 @@ if
(if (is
_
int x) is True then (is
_
string y) else false)
is True then
add x (strlen y) else 0
\end{lstlisting}
&
\end{lstlisting}
&
\medskip\vfill
$
(
\Int
\to
\String
\to
\Int
)
\land
(
\Int
\to
\lnot
\String
\to
0
))
~
\land
$
\newline
$
(
\lnot
\Int
\to
\String
\to
0
)
\land
(
\lnot
\String
\to
0
)
$
(identical to example 5)
...
...
@@ -81,7 +81,7 @@ $(\lnot \Int \to \String \to 0) \land (\lnot \String \to 0)$
let example8 = fun (x : Any) ->
if or
_
(is
_
int x) (is
_
string x) is True then true
else false
\end{lstlisting}
&
\end{lstlisting}
&
\smallskip\vfill
$
(
\Int
\to
\True
)
\land
(
\String
\to
\True
)
~
\land
$
\newline
$
(
\lnot
(
\String\lor\Int
)
\to
\False
)
$
\\\hline
...
...
@@ -91,7 +91,7 @@ let example9 = fun (x : Any) ->
if
(if is
_
int x is True then is
_
int x else is
_
string x)
is True then f x else 0
\end{lstlisting}
&
\end{lstlisting}
&
\smallskip\vfill
$
(
\Int
\to
\Int
)
\land
(
\String
\to
\Int
)
~
\land
$
\newline
$
(
\lnot
(
\String\lor\Int
)
\to
0
)
$
\\\hline
...
...
@@ -113,7 +113,7 @@ let example11 = fun (p : (Any, Any)) ->
let example12 =
fun (p : (Any, Any)) ->
if is
_
int (fst p) is True then true else false
\end{lstlisting}
&
\vfill
\end{lstlisting}
&
\medskip
\vfill
$
((
\Int
,
\textsf
{
Any
}
)
-
>
\True
)
\land
((
\lnot
\Int
,
\textsf
{
Any
}
)
-
>
\False
)
)
$
\\\hline
13
&
\begin{lstlisting}
...
...
@@ -128,16 +128,15 @@ $(\lnot \Int \to \textsf{Any} \to 3)$
14
&
\begin{lstlisting}
let example14
_
alt = fun (input : Int | String) ->
fun (extra : (Any, Any)) ->
if (input, is
_
int (fst extra)) is (Int, True) then
add input (fst extra)
else if (input, is
_
int (fst extra)) is (Any,True) then
add (strlen input) (fst extra)
else 0
\end{lstlisting}
&
\vfill
$
(
\Int
\to
(
\Int
,
\textsf
{
Any
}
)
\to
\Int
)
~
\land
~
(
\Int
\to
(
\lnot
\Int
,
\textsf
{
Any
}
)
\to
0
)
~
\land
~
$
\newline
$
(
\String
\to
(
\Int
,
\textsf
{
Any
}
)
\to
\Int
)
~
\land
~
(
\String
\to
(
\lnot
\Int
,
\textsf
{
Any
}
)
\to
0
)
$
if and2
_
((is
_
int input),(is
_
int (fst extra))) is True
then add input (fst extra)
else if (is
_
int input,is
_
int (fst extra)) is (Any,True)
then add (strlen input) (fst extra)
else 0
\end{lstlisting}
&
\medskip\medskip\vfill
$
(
\Int
\to
((
\Int
,
\textsf
{
Any
}
)
\to
\Int
)
\wedge
((
\lnot\Int
,
\textsf
{
Any
}
)
\to
0
))
\wedge
$
\newline
$
(
\String
\to
((
\Int
,
\textsf
{
Any
}
)
\to
\Int
)
\wedge
((
\lnot\Int
,
\textsf
{
Any
}
)
\to
0
))
$
\\\hline
\end{tabular}
}
...
...
practical.tex
View file @
98f0d787
...
...
@@ -227,37 +227,36 @@ of the example is to show that indeed, the function is ill-typed
{
\definecolor
{
lightgray
}{
gray
}{
.8
}
\color
{
lightgray
}
OLD VERSION
%%
{\definecolor{lightgray}{gray}{.8}
%%
\color{lightgray}OLD VERSION
The original Example~14
could be written in our syntax as:
\begin{alltt}
\color
{
darkblue
}
let example14
_
orig = fun (input : Int | String) ->
fun (extra : (Any, Any)) ->
if (input, is
_
int (fst extra)) is (Int, True) then
add input (fst extra)
else if is
_
int (fst extra) is True then
add (strlen input) (fst extra)
else 0
\end{alltt}
Notice, in the version above the absence of an occurrence of
\texttt
{
input
}
in
the second
\texttt
{
if
}
statement. Indeed, if the first test fails, it is either
because
\texttt
{
is
\_
int (fst extra)
}
is not
\texttt
{
True
}
(i.e., if
\texttt
{
fst extra
}
is not an integer) or because
\texttt
{
input
}
is not an
integer. Therefore, in our setting, the type information propagated to the
second test is :
$
\texttt
{
(
input, is
\_
int
(
fst extra
))
}
\in
\lnot
(
\Int
,
\True
)
$
, that is
$
\texttt
{
(
input, is
\_
int
(
fst extra
))
}
\in
(
\lnot\Int
,
\True
)
\lor
(
\Int
,
\False
)
$
. Therefore, the type deduced for
\texttt
{
input
}
in the second
branch is
$
(
\String\lor\Int
)
\land
(
\lnot\Int
\lor
\Int
)
=
\String\lor\Int
$
which is not precise enough. By adding an occurrence of
\texttt
{
input
}
in our
\texttt
{
example14
\_
alt
}
, we can further restrict its type
typecheck the function. Lifting this limitation through a control-flow analysis
is part of our future work.
}
%%
The original Example~14
%%
could be written in our syntax as:
%%
\begin{alltt}\color{darkblue}
%%
let example14_orig = fun (input : Int | String) ->
%%
fun (extra : (Any, Any)) ->
%%
if (input, is_int (fst extra)) is (Int, True) then
%%
add input (fst extra)
%%
else if is_int (fst extra) is True then
%%
add (strlen input) (fst extra)
%%
else 0
%%
\end{alltt}
%%
Notice, in the version above the absence of an occurrence of \texttt{input} in
%%
the second \texttt{if} statement. Indeed, if the first test fails, it is either
%%
because \texttt{is\_int (fst extra)} is not \texttt{True} (i.e., if
%%
\texttt{fst extra} is not an integer) or because \texttt{input} is not an
%%
integer. Therefore, in our setting, the type information propagated to the
%%
second test is : $\texttt{(input, is\_int (fst extra))} \in \lnot (\Int,
%%
\True)$, that is $\texttt{(input, is\_int (fst extra))} \in (\lnot\Int,
%%
\True)\lor(\Int, \False)$. Therefore, the type deduced for \texttt{input} in the second
%%
branch is $(\String\lor\Int) \land (\lnot\Int \lor \Int) =
%%
\String\lor\Int$ which is not precise enough. By adding an occurrence of
%%
\texttt{input} in our \texttt{example14\_alt}, we can further restrict its type
%%
typecheck the function. Lifting this limitation through a control-flow analysis
%%
is part of our future work.
%%
}
The original Example~14
could be written in our syntax as:
The original Example~14 of~
\citet
{
THF10
}
can be written in our syntax as:
\begin{alltt}
\color
{
darkblue
}
let example14 = fun (input : Int|String) ->
fun (extra : (Any, Any)) ->
...
...
@@ -268,8 +267,9 @@ could be written in our syntax as:
else 0
\end{alltt}
where
\code
{
and2
\_
}
is the uncurried version of the
\code
{
and
\_
}
function in
\eqref
{
and+
}
.
Our system rejects this expression while the system in~
\cite
{
THF10
}
function we defined in
\eqref
{
and+
}
and
\code
{
is
\_
int
}
is the fuction
defined in the third row of Table~
\ref
{
tab:implem
}
.
Our system rejects the expression above, while the system in~
\cite
{
THF10
}
correctly infers the the function always return an integer. The reason
why our system rejects it is because the type it deduces for the
occurrence of
\code
{
input
}
in the 6th line of the code
...
...
@@ -291,12 +291,11 @@ is $\code{(input, is\_int(fst\,extra))} \in
whether
\code
{
is
\_
int(fst
\,
extra)
}
holds or not, then we could deduce
that the following occurrence of
\code
{
input
}
is of type
$
\lnot\Int
$
. But since
\code
{
input
}
does not occur in the test, this
is not done. Instead, the type deduced
refinement of the type of
\code
{
input
}
is not done. Instead, the type deduced
for
\code
{
input
}
in the second branch is
$
(
\String\lor\Int
)
\land
(
\lnot\Int
\lor
\Int
)
=
\String\lor\Int
$
which is not precise
enough to type the application
\code
{
strlen
\;
input
}
. Although
unsatisfactory, it not difficult
to patch this example in our system: it suffices to test
enough to type the application
\code
{
strlen
\;
input
}
. It not difficult
to patch, alas unsatisfactorly, this example in our system: it suffices to test
dummily in the second
\code
{
if
}
the whole argument of
\code
{
and2
\_
}
,
without really checking its first component:
\begin{alltt}
\color
{
darkblue
}
...
...
@@ -309,10 +308,10 @@ without really checking its first component:
else 0
\end{alltt}
Even if the type of
\code
{
is
\_
int
\,
input
}
is not really tested (any
result will
hav
e the same effect) its presence in the test triggers the
result will
produc
e the same effect) its presence in the test triggers the
refinement of the type of the last occurrence of
\code
{
input
}
, which
type checks with the (quite precise) type shown in the entry 14 of
Table~
\ref
{
tab:implem2
}
.
Table~
\ref
{
tab:implem2
}
, type that is equivalent to
$
\Int\vee\String
\to
((
\Int
,
\textsf
{
Any
}
)
\to
\Int
)
\wedge
((
\lnot\Int
,
\textsf
{
Any
}
)
\to
0
)
$
.
Lifting this limitation through a control-flow
analysis is part of our future work.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment