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
124a5a92
Commit
124a5a92
authored
Mar 02, 2020
by
Giuseppe Castagna
Browse files
corrected serveral typos
parent
e33ce86e
Changes
7
Hide whitespace changes
Inline
Side-by-side
abstract.tex
View file @
124a5a92
...
...
@@ -4,7 +4,7 @@ patterns used in untyped languages. Although occurrence typing was
tied from its inception to set-theoretic types---union types, in
particular---it never fully exploited the capabilities of these
types. Here we show how, by using set-theoretic types, it is possible
to develop a general typing frame
m
ork that encompasses and generalizes
to develop a general typing frame
w
ork that encompasses and generalizes
several aspects of current occurrence typing proposals and that can be
applied to tackle other problems such as the reconstruction of intersection
types for unannotated or partially annotated functions and the optimization of
...
...
conclusion.tex
View file @
124a5a92
In this work we presented the core of our analysis of occurrence
typing, extended it to record types and proposed a couple of novel
applications of the theory, namely the
inference
of
intersection types for functions and a static analysis to reduce the number of
applications of the theory, namely the
reconstruction
of
intersection types for
unannotated or partially annotated
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 functions and
...
...
icfp20-submission-main.pdf
0 → 100644
View file @
124a5a92
File added
icfp20-submission-supp.pdf
0 → 100644
View file @
124a5a92
File added
main.bib
View file @
124a5a92
...
...
@@ -317,7 +317,7 @@ series = {POPL ’12}
volume
=
{27}
,
DOI
=
{10.1017/S0960129515000353}
,
number
=
{5}
,
journal
=
{Mathematical Structures in
Computer Science}
,
publisher
=
{Cambridge University
Press}
,
author
=
{L
ÉVY, JEAN-JACQUES
}
,
year
=
{2017}
,
Press}
,
author
=
{L
évy, Jean-Jacques
}
,
year
=
{2017}
,
pages
=
{738–750}
}
...
...
practical.tex
View file @
124a5a92
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
a
type-checking
implementation is 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
...
...
@@ -9,25 +9,25 @@ 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
listing some examples none of which can be typed by current
systems (even though some system such as Flow and TypeScript
can type some of the
m
by adding explicit type annotation, the code 6,
systems (even though some system
s
such as Flow and TypeScript
can type some of the
se examples
by adding explicit type annotation
s
, the code 6,
7, 9, and 10 in Table~
\ref
{
tab:implem
}
and, even more, the
\code
{
and
\_
}
and
\code
{
xor
\_
}
functions at the end of this
section are out of reach of current systems, even when using the right
explicit annotations). These
examples
and others can be tested in the
explicit annotations). These and other
example
s can be tested in the
online toplevel available at
\url
{
https://occtyping.github.io/
}
%
\ifsubmission
~(the
corresponding
repository is
~(the repository is
anonymized).
\else
.
\fi
\input
{
code
_
table
}
In
this table
, the second column gives a code fragment and the third
In
Table~
\ref
{
tab:implem
}
, the second column gives a code fragment and the third
column the type deduced by our implementation. Code~1 is a
straightforward function similar to our introductory example
\code
{
foo
}
in (
\ref
{
foo
}
,
\ref
{
foo2
}
). Here the
programmer annotates the parameter of the function with a coarse type
$
\Int\vee\Bool
$
. Our implementation first type-checks the body of the
function under this assumption, but doing so collects that the type of
function under this assumption, but doing so
it
collects that the type of
$
\texttt
{
x
}$
is specialized to
\Int
{}
in the ``then'' case and to
\Bool
{}
in the ``else'' case. The function is thus type-checked twice more
under each hypothesis for
\texttt
{
x
}
, yielding the precise type
...
...
related.tex
View file @
124a5a92
...
...
@@ -92,7 +92,7 @@ on ``base types''). This is done in the context of a dynamic
language and their approach is extended with polymorphism, dynamic
dispatch and record types.
\citet
{
Kent16
}
bridge
s
the gap between prior work on occurence typing
\citet
{
Kent16
}
bridge the gap between prior work on occurence typing
and SMT based (sub) typing. It introduces the
$
\lambda
_{
RTR
}$
core calculus, an
extension of
$
\lambda
_{
TR
}$
where the logical formulæ embedded in
types are not limited to built-in type predicates, but accept
...
...
@@ -101,9 +101,9 @@ form of dependent typing (and in particular they provide an
implementation supporting bitvector and linear arithmetic theories).
The cost of this expressive power in types is however paid by the
programmer, who has to write logical
annotations (to help the external provers). Here, types and formul
\ae
remain
s
segregated. Subtyping of ``structural'' types is checked by
syntactic rules (as in
\cite
{
THF10
}
) while logical formul
\ae
present
annotations (to help the external provers). Here, types and formul
{
\ae
}
remain segregated. Subtyping of ``structural'' types is checked by
syntactic rules (as in
\cite
{
THF10
}
) while logical formul
{
\ae
}
present
in type predicates are verified by the SMT solver.
\citet
{
Cha2017
}
present the design and implementation of Flow by formalizing a relevant
...
...
@@ -126,7 +126,7 @@ rules looks like classic ones and are easy to understand, unions are
unions of values (and so are intersections and negations), and the
algorithmic part is---excepted for fix points---relatively simple
(algorithmically Flow relies on constraint generation and
solving). This is the reason why our system
i
s more adapted to study
solving). This is the reason why our system
seem
s more adapted to study
and understand occurrence typing and to extend it with additional
features (e.g., gradual typing and polymorphism) and we are eager to
test how much of their analysis we can capture and enhance by
...
...
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