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
occurrencetyping
Commits
2fb410b1
Commit
2fb410b1
authored
Sep 28, 2021
by
Giuseppe Castagna
Browse files
typos
parent
7c89ac87
Changes
1
Hide whitespace changes
Inline
Sidebyside
related.tex
View file @
2fb410b1
...
...
@@ 39,7 +39,7 @@ a functions that
disregards its argument and returns whether the variable
\code
{
y
}
is
an integer or not.
\footnote
{
Although such a function may appear
nonsensical,
\citet
{
kent19phd
}
argues that it corresponds a programming
patter that may
occu
r in Typed Racked due to the expansion of some
patter
n
that may
appea
r in Typed Racked due to the expansion of some
sophisticated macro definitions.
}
While our approach cannot deduce for this function but the
type
$
\Any\to\Bool
$
, the logical approach of TobinHochstadt and
Felleisen can record in the type of
\code
{
isyanumber
}
the fact that
...
...
@@ 64,7 +64,7 @@ wishes by using an overloaded function, as we have shown in
Section~
\ref
{
sec:practical
}
. Second, in our setting,
{
\em
types
\/
}
play the role of formulæ. Using settheoretic types, we can express
the complex types of variables without resorting to a metalogic. This
allows us to type all but two of the
ir
key examples (the notable
allows us to type all but two of the key examples
of~
\citet
{
THF10
}
(the notable
exceptions being Example~9 and 14 in their paper, which use the
propagation of type information outside of the branches of a
test). While Typed Racket supports structured data types such as pairs
...
...
@@ 198,8 +198,7 @@ restricted set of expressions). For instance, we use the operator
worra also to refine the type of the function in an application (see
discussion in Section~
\ref
{
sec:ideas
}
) while in Kent's approach
the analysis of an application
\texttt
{
f
\,
x
}
refines the properties of
the argument
\texttt
{
x
}
but not of the function
\texttt
{
f
}
(as our
approach does); and when such an application is the argument of a type
the argument
\texttt
{
x
}
but not of the function
\texttt
{
f
}
; and when such an application is the argument of a type
test, such as in
\texttt
{
number?
\,
(f
\,
x)
}
, then in Kent's approach it is no longer possible
to refine the information on the argument
\texttt
{
x
}
. The latter is
not is a flaw of the approach but a design choice: as we explain at
...
...
@@ 208,14 +207,14 @@ propositions according to the truthy or false value of an expression,
but also it does it only for a selected set of
\emph
{
pure
}
expressions of
the language, to cope with the possible presence of side effects (and
applications do not belong to this set since they can be be impure).
That said the very fact of focusing on truthy vs.
\
false results may
That said
,
the very fact of focusing on truthy vs.
\
false results may
make Kent's analysis fail even for pure Boolean tests where it would
be expected to work. For example, consider
be
naively
expected to work. For example, consider
the polymorphic function that when applied to two integers returns
whether they have the same parity and false
otherwise:
\code
{
have
\_
same
\_
parity:
$
(
\Int\To\Int\To\Bool
)
\land
(
\neg\Int\To\ANY\To\False
)
\land
(
\ANY\To\neg\Int\To\False
)
$}
. We
can imagine to use this function to implicitly test whether two
arguments are both integers, as in the body of the following function:
arguments are both integers, as in the body of the following function:
%
}
%%%rev
\begin{alltt}
\color
{
darkblue
}
let f = fun (x : Any) > fun (y : Any) >
...
...
@@ 229,13 +228,13 @@ application \code{have\_same\_parity\;x} returns the constant
function
\code
{
true
}
only if
\code
{
x
}
is an integer.
Finally, Kent's approach inherits all the advantages and
disadvantages that the logical propositions approach has with respect
to ours (e.g., flow sensitive analysis vs.
\
user
defined type
to ours (e.g., flow sensitive analysis vs.
\
user

defined type
predicates) that we already discussed at the beginning of this
section.
}
%%%rev
Another direction of research related to ours is the one o
f
semantic
Another direction of research related to ours is the one o
n
semantic
types. In particular, several attempts have been made recently to map
types to first order formul
\ae
. In that setting, subtyping between
types translates to logical implication between formul
\ae
.
...
...
@@ 289,16 +288,16 @@ instance, \cite{BHM14} studies a type system with refinement types,
polymorphism and full union and intersection (but no negation). While
the goal of their typesystem is to verify secure protocol
implementations, the core language RCF
$^{
\forall
}_{
\land\lor
}$
they
present, as well as the associated typesystem is a lambda
calculus
present, as well as the associated typesystem is a
$
\
lambda
$

calculus
with patternmatching, let bindings, and a refining test for equality
(as well as protocol
ori
t
ented constructs such as channel creation,
message passing and expression forking). While on the surface their
(as well as protocol

oriented constructs such as channel creation,
message passing
,
and expression forking). While on the surface their
types ressemble ours, they follow another direction. First, their
language is fully annotated (meaning that
e.g.
polymorphic terms must
be intantiated explicitely and intersection type must also be given
language is fully annotated (meaning that
, for instance,
polymorphic terms must
be intantiated explicitely and intersection type
s
must also be given
through an annotation). Second, since the subtyping relation they
provide is syntactic, it cannot in general take into account the
distributivity of logical connectives w
.r.t
type constructors. This
distributivity of logical connectives w
ith respect to
type constructors. This
limitation is hovever not a problem since the main goal of their
subtyping relation is to propagate a
\emph
{
kinding
}
information that
they use to characterize the level of knowledge an attacker may have
...
...
@@ 401,8 +400,8 @@ handled. On the one end of the spectrum lies our approach: our
analysis takes into account
\emph
{
all
}
expressions but, in its current
formulation, it works only for pure languages. On the other end of the
spectrum we find the approach of Typed Racket whose analysis reasons
about a limited and predetermined set of
\emph
{
pure
}
operations
(
all data structure
accessors
)
. Somewhere inbetween lies the approach of the
about a limited and predetermined set of
\emph
{
pure
}
operations
:
all data structure
accessors. Somewhere inbetween lies the approach of the
Flow language which, as hinted above, implements a complex effect systems to determine
pure expressions. While the system presented here does not work for
impure languages, we argue that its foundational nature predisposes it
...
...
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