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
146d51c7
Commit
146d51c7
authored
Feb 28, 2020
by
Kim Nguyễn
Browse files
Rewording and typos in related work.
parent
1f5115a3
Changes
1
Show whitespace changes
Inline
Side-by-side
related.tex
View file @
146d51c7
...
...
@@ -66,30 +66,18 @@ for recursive types.}
%one performed by Code 8 for extensible records is not handled by the
%current typing systems.
\citet
{
Kent16
}
introduce 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
predicates of arbitrary theories. This allows them to provide some
form of dependent typing (and in particular they provide an
implementation supporting bitvector and linear arithmetic theories).
While static invariants that can be enforced by such logic go well
beyond what can be proven by a static ``non dependent'' type
system as ours, they do so at the cost of having the programmer write logical
annotations (to help the external provers). While this work provides
richer logical statements than those by~
\citet
{
THF10
}
, it still remains
restricted to refining the types of variables, and not of arbitrary
constructs such as pairs, records or recursive types. The idea to
defer the subtyping check to an SMT solver is not new.
The work of
\citet
{
Bierman10
}
presents Dminor, a data-oriented
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
types translates to logical implication between formul
\ae
.
\citet
{
Bierman10
}
introduce Dminor, a data-oriented
language featuring a
{
\tt
SELECT
}
-like construct over
collections. Its type systems combine semantic subtyping and
refinement types. Syntactic types are mapped to first order formulæ
and subtyping is expressed as logicial implication. An SMT-solver is
then used to (try to) prove the logicial implication. The refinement
collections. Types are mapped to first order formulæ and an SMT-solver is
then used to (try to) prove their satisfiability. The refinement
types they present go well beyond what can be expressed with the set-theoretic
types we use (as they allow almost any pure expression to occur in
types). However, the system forgoes any notion of completeness
(since satisfiability of first order logic is undecidable)
and the
and the
subtyping algorithm is largely dependent on the subtle behaviour of
the SMT solver (which may timeout or give an incorrect model that
cannot be used as a counter-example to explain the type-error).
...
...
@@ -102,10 +90,21 @@ A similar approach is taken in \cite{Chugh12}, and extended to so-called nested
appear in a logical formula (where previous work only allowed formulae
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. As in
\cite
{
Bierman10
}
, the refined type
of a conditional does not flow to the outer context and the same
caveats to using an SMT solver apply.
dispatch and record types.
\citet
{
Kent16
}
bridges 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
predicates of arbitrary theories. This allows them to provide some
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
remains 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
fragment of the language. Since they target an industrial-grade
...
...
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