Commit 4e306958 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

more revision

parent b0cbf924
......@@ -259,7 +259,7 @@ system to satisfy the property of type preservation, the type system
must be able to deduce negated arrow types for functions---e.g. the
type $(\Int\to\Int)\wedge\neg(\Bool\to\Bool)$ for $\lambda^{\Int\to\Int}
x.x$. We demonstrated this with the expression in
equation \eqref{bistwo}, where type preservation holds only if we are
equation \eqref{bistwo}, for which type preservation holds only if we are
able to deduce for this expression the type
$(\Int\to t)\setminus(\Int\to\neg\Bool)$, that is, $(\Int\to t)\wedge\neg(\Int\to\neg\Bool)$.
}%%%rev
......
......@@ -66,6 +66,53 @@ for recursive types.}
%one performed by Code 8 for extensible records is not handled by the
%current typing systems.
\rev{%%%
For what concerns the first work by~\citet{THF08} it is interesting to
compare this work with ours because the comparison shows two rather
different approaches to deal with the property of type
preservation. \citet{THF08} define a first type-system that does not
satisfy type-preservation. The reason for that is that this first type
system checks all the branches of a type-case expression,
independently from whether they are selectable or not, and this may
result in a well-typed expression to reduces to an expression that it
is not well-typed because it contains a type-case expression that,
because of the reduction, has a branch that became non-selectable but
also ill-typed (see \cite[Section 3.3]{THF08}). To obviate this
problem they introduce a \emph{second} type system that extends the
previous one with some auxiliary typing rules that type type-case
expressions by skipping the typing of non selectable-branches and use
this second type-system only to prove type-preservation and obtain,
thus the soundness of their type system. In our work, instead, we
prefer to start directly with a system that satisfies
type-preservation. Our system does not have the problem of their first
system because we included the \Rule{Efq} rule for that very purpose,
that is skip the typing of non-selectable branches. The choice of one
or the other approach is a matter of taste and, in this specific case,
it boils down to deciding
whether some typing problems must be statically signalled by an error or a
warning. The approach of~\citet{THF08} ensures that every
subexpression of a program is well-typed and, if not, it generates a
type-error. Our approach allows some subexpression of a program to be ill-typed,
but only if they occurr in dead branches of type-cases. But in that case case any
reasonable implementation would flag a warning to signal the presence
of a dead branch. The very same reasons that explain the presence of \Rule{Eqf}
explain why in our system we included from the beginning the typing
rule \Rule{Abs-}
to deduce negated arrow types: we want a system that satisfies type
preservation (albeit, for a parallel reduction:
cf: \Appendix\ref{app:parallel}). We then defined an algorithmic
system that is not \emph{complete} with respect to the type-system but
from which it inherits its soundness. Of course we could have started
directly with a type-system corresponding to the algorithm (i.e., not
include the rule \Rule{Abs-}) and then extend this system with the
inference of negated arrows, to prove type preservation. ... the
advantage is that we can explore different subsystems that are
complete and argue that they are all we need in practice ....
}%%%rev
Another direction of research related to ours is the one of semantic
types. In particular, several attempts have been made recently to map
types to first order formul\ae. In that setting, subtyping between
......
......@@ -111,9 +111,14 @@ a more general set of propositions (here, about arbitrary expressions,
there, about expressions with a limited set a pure functions, but see
below) is also present in both. Similarly the need for an explosion
rule in order to circumvent difficulties in proofs of type soundness
is discussed in [22].
>> Kim: compare the rules added in Figure 6 of THF2008 and justified in section 3.3 with
>> the fact that we use ex-falso quodlibet
is discussed in [22].
>> Kim: compare the rules added in Figure 6 of THF2008 and justified
>> in section 3.3 with the fact that we use ex-falso quodlibet. We can
>> add that like
>> THF2008 we use a different system since we have to use type-schemes
>> (see Appendix A.3.2), but also a different reduction since we use
>> parallel reductions
## Discussion of pure expressions
......@@ -160,7 +165,9 @@ seem unneeded:
schemes. Why not simply present the system that's actually
implemented, which as the paper says is all that is really needed.
>> Beppe; answer on the interest of the fully complete system
>> Beppe; answer on the interest of the fully complete system (and
stress en passant that type schemes are needed to prove
type-preservation
- the treatment of interdependent tests. Is this needed for any real
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment