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
deafed1b
Commit
deafed1b
authored
May 05, 2021
by
Giuseppe Castagna
Browse files
moved rule from appendix to section 4
parent
05e2fd1b
Changes
4
Hide whitespace changes
Inline
Side-by-side
main-elsarticle.tex
View file @
deafed1b
...
...
@@ -261,18 +261,20 @@ The authors thank Paul-André Melliès for his help on type ranking.
\newpage
\iflongversion\else
\iflongversion\else
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section
{
Record types operators
}
\label
{
app:recop
}
\input
{
record
_
operations
}
\fi
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
\newpage
\section
{
A more precise rule for inference
}
\label
{
app:optimize
}
In our prototype we have implemented for the inference of arrow type the following rule:
\input
{
optimize
}
\newpage
\fi
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
\newpage
\section
{
A Roadmap to Polymorphic Types
}
\label
{
app:roadmap
}
\input
{
roadmappolymorphism
}
...
...
optimize.tex
View file @
deafed1b
In our prototype we have implemented for the inference of arrow type the following rule:
\[
\begin
{
array
}{
l
}
{
\small\Rule
{
AbsInf
++
}}
\\
\frac
...
...
@@ -14,7 +13,9 @@ In our prototype we have implemented for the inference of arrow type the followi
\textstyle\Gamma\vdash\lambda
x
{
:
}
s.e:
{
\bigwedge
_{
(
s',t'
)
\in
T
}
s'
\to
t'
}
}
\end
{
array
}\]
instead of the simpler
\Rule
{
AbsInf+
}
. The difference w.r.t.
\ \Rule
{
AbsInf+
}
is that the typing of the body
instead of the simpler
\Rule
{
AbsInf+
}
given in
Section
\ref
{
sec:refining
}
. The difference of this new rule with
respect to
\Rule
{
AbsInf+
}
is that the typing of the body
is made under the hypothesis
$
x:s
\setminus\bigvee
_{
s'
\in\psi
(
x
)
}
s'
$
,
that is, the domain of the function minus all the input types
determined by the
$
\psi
$
-analysis. This yields an even better refinement
...
...
practical.tex
View file @
deafed1b
...
...
@@ -2,9 +2,18 @@ We have implemented the algorithmic system $\vdashA$. Our
implementation is written in OCaml and uses CDuce as a library to
provide the semantic subtyping machinery. Besides the 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
record types of Section
\ref
{
ssec:struct
}
) and the refinement of
function types
\iflongversion
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
described in Section
\ref
{
sec:refining
}
. Furthermore, our implementation uses for the inference of arrow types
the following improved rule:
\input
{
optimize
}
\else
of Section
\ref
{
sec:refining
}
with the rule of
Appendix~
\ref
{
app:optimize
}
.
\fi
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
The implementation is rather crude and
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
}
by
...
...
refining.tex
View file @
deafed1b
...
...
@@ -18,10 +18,10 @@ typing we developed in the first part of the paper. In particular, we
collect the different types that are assigned to the parameter of a function
in its body, and use this information to partition the domain of the function
and to re-type its body. Consider a more involved example in a pseudo
TypeScript that uses our
notation
TypeScript that uses our
syntax for type-cases
\begin{alltt}
\color
{
darkblue
}
\morecompact
function (x
\textcolor
{
darkred
}{
:
\(
\tau
\)}
)
\{
return (x
\(
\in
\)
Real) ? ((x
\(
\in
\)
Int) ? x+1 : sqrt(x)) : !x;
\refstepcounter
{
equation
}
\mbox
{
\color
{
black
}
\rm
(
\theequation
)
}
\label
{
foorefine
}
return (x
\(
\in
\)
Real) ? ((x
\(
\in
\)
Int) ? x+1 : sqrt(x)) : !x;
\refstepcounter
{
equation
}
\mbox
{
\color
{
black
}
\rm
(
\theequation
)
}
\label
{
foorefine
}
\}
\end{alltt}
where we assume that
\code
{
Int
}
is a
...
...
@@ -170,7 +170,13 @@ first typecheck the body of the function as usual (to check that the
arrow is valid) and collect the refined types for the parameter
$
x
$
.
Then we deduce all possible output types for this refined set of input
types and add the resulting arrows to the type deduced for the whole
function (see Appendix~
\ref
{
app:optimize
}
for an even more precise rule).
function (see
\iflongversion
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Section~
\ref
{
sec:practical
}
\else
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\else\Appendix\ref
{
app:optimize
}
\fi
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
for an even more precise rule).
\kim
{
We define the rule on the type system not the algorithm. I think
...
...
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