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
d48a9533
Commit
d48a9533
authored
May 09, 2021
by
Giuseppe Castagna
Browse files
Patched fixpoint combinator
parent
0af273e2
Changes
4
Hide whitespace changes
Inline
Side-by-side
code_table.tex
View file @
d48a9533
...
...
@@ -148,7 +148,7 @@ $(\Int\to\textsf{Empty})\land(\neg\Int\to{}2)$\newline
atom null
type Object = Null |
{
prototype = Object ..
}
type ObjectWithPropertyL =
{
l = Any ..
}
|
{
prototype = ObjectWithPropertyL ..
}
|
{
prototype = ObjectWithPropertyL ..
}
let has
_
property
_
l = fun (o:Object) ->
if o is ObjectWithPropertyL then true else false
...
...
@@ -158,7 +158,7 @@ let has_own_property_l = fun (o:Object) ->
let get
_
property
_
l = fun (self:Object->Any) o ->
if has
_
own
_
property
_
l o is True then o.l
else if o is N
i
l then n
i
l
else if o is N
ul
l then n
ul
l
else self (o.prototype)
\end{lstlisting}
&
\vfill\medskip\smallskip
$
(
\Keyw
{
ObjectWithPropertyL
}
\to\True
)
$
$
\land
$
...
...
fixpoint.tex
0 → 100644
View file @
d48a9533
\noindent
In our language, a fixpoint combinator can be defined as follows
\begin{alltt}
\color
{
darkblue
}
type X = X ->
\textit
{
S
}
->
\textit
{
T
}
let z = fun (((
\textit
{
S
}
->
\textit
{
T
}
) ->
\textit
{
S
}
->
\textit
{
T
}
) -> (
\textit
{
S
}
->
\textit
{
T
}
)) f ->
let delta = fun ( X -> (
\textit
{
S
}
->
\textit
{
T
}
) ) x ->
f ( fun (
\textit
{
S
}
->
\textit
{
T
}
) v -> ( x x v ))
in delta delta
\end{alltt}
which applied to any function
\code
{
f:(
\textit
{
S
}$
\to
$
\textit
{
T
}
)
$
\to
$
\textit
{
S
}$
\to
$
\textit
{
T
}}
returns a function
\code
{
(z
\,
f):
\textit
{
S
}$
\to
$
\textit
{
T
}}
such that
for every non
diverging expression
\code
{$
e
$}
of type
\code
{
\textit
{
S
}}
, the
expression
\code
{
(z
\,
f)
$
e
$}
(which is of type
\code
{
\textit
{
T
}}
) reduces to
\code
{
f((z
\,
f)
$
e
$
)
}
.
It is then clear that definition of
\code
{
get
\_
property
\_
l
}
in Code 11
of Table~
\ref
{
tab:implem
}
, is nothing but syntactic sugar for
\begin{alltt}
\color
{
darkblue
}
let get
_
property
_
l =
let aux = fun (self:Object->Any) -> fun (o:Object)->
if has
_
own
_
property
_
l o is True then o.l
else if o is Null then null
else self (o.prototype)
in z aux
\end{alltt}
where
\code
{
\textit
{
S
}}
is
\code
{
Object
}
and
\code
{
\textit
{
T
}}
is
\code
{
Any
}
.
main-elsarticle.tex
View file @
d48a9533
...
...
@@ -261,6 +261,10 @@ The authors thank Paul-André Melliès for his help on type ranking.
\newpage
\section
{
Fix-point combinator
}
\label
{
sec:fixpoint
}
\input
{
fixpoint
}
\iflongversion
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
...
...
practical.tex
View file @
d48a9533
...
...
@@ -187,26 +187,30 @@ This is precisely reflected by the case $\Int\to\Empty$ in the result.
Indeed our
{
\tt
example10
}
function can be applied to an integer, but
at runtime the application of
{
\tt
f
\,
x
}
will diverge.
Code~11 simulates the behavio
u
r of JavaScript property resolution, by looking
Code~11 simulates the behavior of JavaScript property resolution, by looking
for a property
\texttt
{
l
}
either in the object
\texttt
{
o
}
itself or in the
chained list of its
\texttt
{
prototype
}
objects. In that example, we first model
prototype
chaining by defining a type
\texttt
{
Object
}
that can be either the
prototype
-
chaining by defining a type
\texttt
{
Object
}
that can be either the
atom
\texttt
{
Null
}
or any record with a
\texttt
{
prototype
}
field which contains
(recursively) an
\texttt
{
Object
}
. To ease the reading, we defined a recursive
type
\texttt
{
ObjectWithPropertyL
}
which is either a record with a field
\texttt
{
l
}
or a record with a prototype of type
\texttt
{
ObjectWithPropertyL
}
. We
can then define two predicate function
\texttt
{
has
\_
property
\_
l
}
and
\texttt
{
has
\_
own
\_
property
\_
l
}
that test
s
whether an object has a property
through its prototype or directly. Lastly we can define a function
can then define two predicate function
s
\texttt
{
has
\_
property
\_
l
}
and
\texttt
{
has
\_
own
\_
property
\_
l
}
that test whether an object has a property
through its prototype or directly. Lastly
,
we can define a function
\texttt
{
get
\_
property
\_
l
}
which directly access the field if it is present, or
recursively search for it through the prototype chain
(
in our syntax, the
par
e
meter
\texttt
{
self
}
allows one to refer to the function itself
)
. Of
recursively search for it through the prototype chain
, where
in our syntax, the
explicitly-typed
par
a
meter
\texttt
{
self
}
allows one to refer to the function itself. Of
particular interest is the type deduced for the two predicate functions. Indeed,
we can see that
\texttt
{
has
\_
own
\_
property
\_
l
}
is given an overloaded type whose
first argument is in each case a recursive record type that describe precisely
whether
\texttt
{
l
}
is present at some point in the list or not (recall that
in a record type such as
$
\orecord
{
l
=
?
\Empty
}$
, indicate that field
\texttt
{
l
}
is absent for sure).
is absent for sure). As an aside notice that even if our language does
not explicitly include recursive expression, it is quite easy to
define a well-typed fix-point combinator (for the reader convinience
we show its definition both in
\Appendix\ref
{
sec:fixpoint
}
and in our
on-line prototype).
Finally, Code~12 implements the typical type-switching pattern used in
JavaScript. While languages such as Scheme and Racket provides specific
...
...
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