Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Giuseppe Castagna
occurrence-typing
Commits
0b36acea
Commit
0b36acea
authored
Mar 02, 2020
by
Giuseppe Castagna
Browse files
spacing
parent
f2e04704
Changes
2
Hide whitespace changes
Inline
Side-by-side
algorithm.tex
View file @
0b36acea
...
...
@@ -253,7 +253,12 @@ cases.
\subsubsection
{
Algorithmic typing rules
}
\label
{
sec:algorules
}
We now have all the notions we need for our typing algorithm, which is defined by the following rules.
We now have all the notions we need for our typing algorithm
%
\iflongversion
%
, which is defined by the following rules.
\else
%
:
\fi
\begin{mathpar}
\Infer
[Efq\Aa]
{
}
...
...
language.tex
View file @
0b36acea
...
...
@@ -197,7 +197,7 @@ arrow types, as long as these negated types do not make the type deduced for the
\Infer
[Abs-]
{
\Gamma
\vdash
\lambda
^{
\wedge
_{
i
\in
I
}
\arrow
{
s
_
i
}
{
t
_
i
}}
x.e:t
}
{
\Gamma
\vdash\lambda
^{
\wedge
_{
i
\in
I
}
\arrow
{
s
_
i
}
{
t
_
i
}}
x.e:
\neg
(t
_
1
\to
t
_
2)
}
{
((
\wedge
_{
i
\in
I
}
\arrow
{
s
_
i
}
{
t
_
i
}
)
\wedge\neg
(t
_
1
\to
t
_
2))
\not\simeq\Empty
}
\vspace
{
-1mm
}
{
((
\wedge
_{
i
\in
I
}
\arrow
{
s
_
i
}
{
t
_
i
}
)
\wedge\neg
(t
_
1
\to
t
_
2))
\not\simeq\Empty
}
\vspace
{
-1
.2
mm
}
\end{mathpar}
%\beppe{I have doubt: is this safe or should we play it safer and
% deduce $t\wedge\neg(t_1\to t_2)$? In other terms is is possible to
...
...
@@ -228,7 +228,7 @@ integer returns its successor and applied to anything else returns
%\[
\lambda
^{
(
\Int\to\Int
)
\wedge
(
\neg\Int\to\Bool
)
}
x
\,
.
\,\tcase
{
x
}{
\Int
}{
x
+
1
}{
\textsf
{
true
}}
%\]
\)}
\\
[
1
mm]
\)}
\\
[
.6
mm]
Clearly, the expression above is well typed, but the rule
\Rule
{
Abs+
}
alone
is not enough to type it. In particular, according to
\Rule
{
Abs+
}
we
have to prove that under the hypothesis that
$
x
$
is of type
$
\Int
$
the expression
...
...
@@ -253,7 +253,7 @@ expression whose type environment contains an empty assumption:
\end{mathpar}
Once more, this kind of deduction was already present in the system
by~
\citet
{
Frisch2008
}
to type full fledged overloaded functions,
though it was embedded in the typing rule for the type-case.
\pagebreak
though it was embedded in the typing rule for the type-case.
~
\pagebreak
Here we
need the rule
\Rule
{
Efq
}
, which is more general, to ensure the
property of subject reduction.
...
...
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