Semantic Domain
Wednesday, August 21, 2019
On the Relationship Between Static Analysis and Type Theory
Some months ago, Ravi Mangal sent
me an email with a very interesting question, which I reproduce in part
below:
The question that has been bothering me is, "How are static analyses
and type systems related?". Besides Patrick Cousot's /Types as
abstract interpretations/ , I have
failed to find other material directly addressing this. Perhaps, the
answer is obvious, or maybe it has just become such a part of the
community's folklore that it hasn't been really written down.
However, to me, it's not clear how one might even phrase this
question in a precise mathematical manner.
The reason this question is so interesting is because some very
beautiful answers to it have been worked out, but have for some reason
never made it into our community's folklore. Indeed, I didn't know the
answers to this question until quite recently.
The short answer is that there are two views of what type systems are,
and in one view type systems are just another static analysis, and in
another they form the substrate upon which static analyses can be built
-- and both views are true at the same time.
Static Analysis (including Types) as Properties
One valid view of a type system, is that it is just another species of
static analysis. At a high level, the purpose of a static analysis is to
answer the question, "Can I tell what properties this program satisfies
*without* running it?"
Abstract interpretation, model checking, dataflow analysis and type
inference are all different ways of answering this question, each with
somewhat different emphases and priorities. IMO, to understand the
relations between these styles of analysis, it's helpful to think about
the two main styles of semantics: operational semantics and denotational
semantics.
A denotational semantics turns a program into a mathematical object
(sets, domains, metric spaces, etc). This has the benefit that it lets
you turn the full power of mathematics towards reasoning about programs,
but it has the cost that deducing properties of arbitrary mathematical
gadgets can require arbitrary mathematical reasoning.
Operational semantics, on the other hand, turns a program into a state
machine. This has the benefit that this is relatively easy to do, and
close to how computers work. It has the cost that it only gives
semantics to whole programs, and in reality people tend to write
libraries and other partial programs. (Also, infinite-state operational
semantics doesn't make things obviously easier to work with than a
denotational semantics.)
Operational semantics gives rise to model checking: if you have a
program, you can view the sequence of states it takes on as a concrete
model of temporal logic. So model checking then checks whether a
temporal properties overapproximates or refines a concrete model.
So basically all static analyses work by finding some efficiently
representable approximation of the meaning of a program, and then using
that to define an algorithm to analyse the program, typically by some
form of model checking. For type systems, the approximations are the
types, and in abstract interpretation, this is what the abstract domains
are.
David A. Schmidt's paper /Abstract Interpretation from a Denotational
Semantics Perspective/ shows how you can see abstract domains as arising from domain
theory, by noting that domains arise as the infinite limit of a series
of finite approximations, and so you can get an abstract domain by
picking a finite approximation rather than going all the way to the limit.
Thomas Jensen's PhD thesis, /Abstract Interpretation in Logical Form/
, shows how an
abstract interpretation of a higher-order functional language
corresponds to a certain intersection type system for it. This helps
illustrate the idea that abstract domains and types are both
abstractions of a program. (FWIW, finding equivalences between abstract
domains and type systems used to be big topic back in the 90s, but seems
to have disappeared from view. I don't know why!)
Now, model checking an infinite-state system will obviously fail to
terminate in general. However, it can then be made effective and
algorithmic by using your abstractions (either from types or from
abstract interpretation) to turn the model into a finitary one that can
be exhaustively searched.
For dataflow analysis, David A. Schmidt works out this idea in detail in
his paper, /Data Flow Analysis is Model Checking of Abstract
Interpretations/ , where he shows how if you build
an abstraction of program traces and model-check against mu-calculus
formulas, you can get back most classical dataflow analyses. (If one
lesson you draw is that you should read everything David Schmidt has
written, well, you won't be wrong.)
It's less common to formulate type-based analyses in this form, but some
people have looked at it.
1.
There is a line of work on "higher-order model checking" which works
by taking higher-order programs, using type inference for special
type systems to generate abstractions for them which lie in special
subclasses of pushdown systems which are decidable for the
properties of interest for program analysis (eg, emptiness testing).
Luke Ong wrote an overview of the area for LICS 2015, in his paper /
Higher-Order Model Checking: an Overview/ .
2.
Dave Clarke and Ilya Sergey have a nice IPL 2012 paper, /A
correspondence between type checking via reduction and type checking
via evaluation/ , in which they show how you can view types as
abstract values, and use this perspective to derive an abstract
interpreter for a program which operates on these abstract values.
They don't state it explicitly, since it was too obvious to mention,
but you can check that a program |e| has the type |int| by asserting
that |e| will eventually evaluate to the abstract value |int|. This
is easy to check since every program in their abstract semantics
terminates -- and so you can just evaluate |e| and see if the result
is |int|.
Types as Grammar
However, while types can be seen as a way of stating program properties,
they have a second life as a way of defining /what the valid programs
are/. A type system can also be seen as a way of statically ruling out
certain programs from consideration. That is, an expression like |
3("hi")|, which applies the argument |"hi"| to the number |3|, is valid
Javascript or Python code, but is not a valid program in OCaml or Java,
as it would be rejected at compile time by the typechecker.
As a result, type systems can also be used to simplify the semantics: if
a term is statically ruled out, you don't have to give semantics to it.
The benefit of doing this is that this can dramatically simplify your
static analyses.
For example, if you have a typed functional language with integers and
function types, then building an abstract interpretation to do a sign
analysis is simplified by the fact that you don't have to worry about
function values flowing into the integer domain. You can just take the
obvious abstract domains for each type and then rely on the type system
to ensure that only programs where everything fits together the way you
want are ever allowed, freeing you of the need for a jumbo abstract
domain that abstracts all values.
For cultural reasons, this methodology is often used in type systems
research, but relatively rarely in static analysis work. Basically, if
you tell a type systems researcher that you are changing the language to
make it easier to analyze, they will say "oh, okay", but if you tell a
static analysis researcher the same thing, they may express a degree of
skepticism about your ability to update all Java code everywhere.
Naturally, neither reaction is right or wrong: it's contextual. After
all, there /are/ billions of lines of Java code that won't change, *and
also* the Java language /does/ change from version to version.
However, as researchers we don't just pick up context from our problems,
but also from our peers, and so the culture of type systems research
tends to privilege new languages and the culture of static analysis
research tends to privilege applicability to existing codebases, even
though there is no fundamental technical reason for this linkage. After
all, all static analyses exploit the structure of the language whenever
they can in order to improve precision and scalability.
For example, in a typical intraprocedural dataflow analysis, we
initialize all the local variables to the bottom element of the dataflow
lattice. This is a sound thing to do, /because/ the language is
constrained so that local variables are freshly allocated on each
procedure invocation. If, on the other hand, we were doing dataflow
analysis of assembly code, different subroutines would all
simultaneously affect the dataflow values assigned to each register.
As a consequence, one thing I'm looking forward to is finding out what
static analysis researchers will do when they start taking a serious
look at Rust. Its type system enforces really strong invariants about
aliasing and data races, which ought to open the door to some really
interesting analyses.
The Relationship Between the Two Views
As you can see, grammaticality constraints and program analysis are not
opposed, and can overlap in effect. Furthermore, this means people
writing papers on type systems are often blurry about which perspective
they are taking -- in one section of a paper they may talk about types-
as-properties, and in another they may talk about types-as-grammar. This
ambiguity is technically harmless, but can be confusing to a reader
coming to type systems from other areas within formal methods.
The reason this ambiguity is mostly harmless is because for well-
designed languages there will be a nice relationship between these two
views of what types are. John C Reynolds explained this, in his lovely
paper /The Meaning of Types: From Intrinsic to Extrinsic Semantics/
. (In
his language, "intrinsic types" are types-as-grammar, and "extrinsic
types" are types-as-property.)
Basically, he noted that when you give a denotational semantics under a
types-as-grammar view, you interpret /typing derivations/, and when you
give a denotational semantics in the types-as-property view, you
interpret /program terms/. For types-as-grammar to make sense, its
semantics must be /coherent/: two typing derivations of the same program
must have the same semantics. (Otherwise the semantics of a program can
be ambiguous.) But once coherence holds, it becomes feasible to prove
the equivalence between the intrinsic and extrinsic semantics, because
there is a tight connection between the syntax of the language and the
typing derivations.
Noam Zeilberger and Paul-Andre Melliès wrote a POPL 2015 paper, /
Functors are Type Refinement Systems/ , where they work out
the general semantic structure underpinning Reynolds' work, in terms of
the relationship between intersection types (or program logic) and a
base language.
Compositionality
Another cultural effect is the importance type systems research places
on compositionality. It is both absolutely the case that there is no /a
priori/ reason a type system has to be compositional, and also that most
type systems researchers -- including myself! -- will be very doubtful
of any type system which is not compositional.
To make this concrete, here's an example of a type system which is
pragmatic, reasonable, and yet which someone like me would still find
distasteful.
Consider a Java-like language whose type system explicitly marks
nullability. We will say that method argument |(x : C)| means that |x|
is a possibly |null| value of type |C|, and an argument |x : C!| means
that |x| is definitely of class |C|, with no |null| value. Now, suppose
that in this language, we decide that null tests should refine the type
of a variable:
| // x : C outside the if-block
if (x !== null) {
doSomething(x); // x : C! inside the if-block
} |
Basically, we checked that |x| was not |null|, so we promoted its type
from |C| to |C!|. This is a reasonable thing to do, which industrial
languages like Kotlin support, and yet you
will be hard-pressed to find many formal type theories supporting
features like this.
The reason is that the culture of type theory says that type systems
should satisfy a /substitution principle/: a variable stands in for a
term, and so substituting a term of the same type as the variable should
result in a typeable term. In this case, suppose that |e| is a very
complicated expression of type |C|. Then if we do a substitution of |e|
for |x|, we get:
| if (e !== null) {
doSomething(e); // e : C! -- but how?
} |
Now we somehow have to ensure that |e| has the type |C!| inside the
scope of the conditional. For variables this requires updating the
context, but for arbitrary terms it will be much harder, if it is even
possible at all!
The culture of static analysis says that since it's easy for variables,
we should handle that case, whereas the culture of type theory says that
anything you do for variables should work for general terms. Again,
which view is right or wrong is contextual: it's genuinely useful for
Kotlin programmers to have dataflow-based null-tracking, but at the same
time it's much easier to reason about programs if substitution works.
The reason type theorists have this culture is that type theory has two
parents. On one side are Scott and Strachey, who consciously and
explicitly based denotational semantics upon the compositionality
principle; and the other side comes from the structural proof theory
originated by Gerhard Gentzen, which was invented precisely to prove
cut-eliminability (which basically just is a substitution principle). As
a result, the type-theoretic toolbox is full of tools which both assume
and maintain compositionality. So giving that up (or moving past it,
depending on how you want to load the wording emotionally) is something
which requires very careful judgement.
For example, the Typed Racket language extends the dynamically-typed Racket language with types, and to support
interoperation with idiomatic Racket code (which uses control-flow
sensitive type tests), they do flow-sensitive typing. At ESOP 2011,
Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi wrote a paper
about a particularly elegant way of combining flow analysis and
typechecking, /Typing Local Control and State Using Flow Analysis/
.
Conclusion
Finally, one might wonder whether it is worth it to try developing a
unified perspective on type theory and static analysis. It's a lot of
work to learn any one of these things, and (for example) David Schmidt's
papers, while deeply rewarding, are not for the faint of heart. So maybe
we should all specialize and not worry about what members of cousin
tribes are doing?
All I can say is that I think I benefited tremendously from the fact
that (largely by accident) I ended up learning separation logic,
denotational semantics and proof theory as part of my PhD. There
actually is a wholeness or consilience to the variety of techniques that
the semantics community has devised, and insights apply across domains
in surprising ways.
My recent PLDI paper with
Jeremy Yallop is a nice example of
this. Very little in this paper is hard, but what makes it easy is that
we felt free to switch perspectives as we needed.
Because I had learned to like automata theory from reading papers on
model checking, I ended up reading about Brüggemann-Klein and Wood's
characterization of the deterministic regular languages . Then,
because I share the aesthetics of denotational semantics, I realized
that they invented a superior, compositional characterization of the
FOLLOW sets used in LL(1) parsing. Then, because I knew about the
importance of substitution from type theory, this lead me to switch from
the BNF presentation of grammars, to the mu-regular expressions. This
let us offer the traditional parser combinator API, while under the hood
having a type system which identified just the LL(1)-parseable grammars.
Moreoever, the type inference algorithm we use in the implementation is
basically a dataflow analysis. And that set things up in a form to which
multistage programming techniques were applicable, letting us derive
parser combinators that run faster than yacc.
But beyond the direct applications like that, it is just good to be able
to go to a conference and be interested by what other people are doing.
Everyone attending has developed deep expertise in some very esoteric
subjects, and learning enough to learn from them is valuable. Research
communities are long-running conversations, and being able to hold up
your end of the conversation makes the community work better.
Posted by Neel Krishnaswami at 6:42 AM
4 comments:
1.
Kartik August
25, 2019 at 5:12 PM
Thanks for sharing these insights. As a beginner in the PL
community, I highly value these expository blog posts relating
different sub-fields and helping us gain a broader perspective. :)
Reply Delete
Replies
Reply
2.
Kyle Headley August 26, 2019 at 2:28 PM
I have increasingly considered types as static analysis, and your
insights further the trend.
I wonder if there is value in taking this further, and considering a
language as a graph of interdependent analyses. For example a parser
may be thought of as an analysis of text which might reveal meaning.
A grammar would be the configuration of this analysis, in a form
that communicates requirements to humans. Considering a program as
valid would require a specific subset of its language's analyses to
complete affirmatively. All analyses provide metadata for users and
IDEs, and the ones that run quickly with simple results are especial
helpful as continuous feedback.
I happen to like type-based analyses because they are fast and
provide strong guarantees, like compositionality that you mentioned.
Perhaps I should now consider them as grammar-based analyses? Which
are defined as analyses with a simple, small set of rules that are
easily checked and communicated.
Reply Delete
Replies
Reply
3.
Sam Tobin-Hochstadt August 26, 2019 at 8:20 PM
It's worth noting that unlike Kotlin, Typed Racket works very hard
to make this aspect of the type system compositional in precisely
the sense you describe, in large part for the very cultural reasons
you point out.
Reply Delete
Replies
Reply
4.
Neel Krishnaswami August 27, 2019 at 9:35 AM
Hi Sam, my apologies for implying that substitution doesn't hold for
Typed Racket! I originally meant to spend some time comparing it to
Arjun & co's system, but eventually didn't.
Reply Delete
Replies
Reply
Add comment
Load more...
Newer Post Older Post
Home
Subscribe to: Post Comments (Atom)
About Me
Neel Krishnaswami
View my complete profile
Blog Archive
* ► 2025 (1)
o ► January (1)
* ► 2024 (1)
o ► December (1)
* ► 2023 (3)
o ► October (1)
o ► September (1)
o ► July (1)
* ► 2022 (6)
o ► November (2)
o ► September (1)
o ► March (2)
o ► January (1)
* ► 2021 (6)
o ► December (2)
o ► November (1)
o ► September (1)
o ► July (1)
o ► February (1)
* ► 2020 (4)
o ► December (2)
o ► June (1)
o ► February (1)
* ▼ 2019 (8)
o ► October (1)
o ▼ August (3)
+ New Draft Paper: Survey on Bidirectional Typechecking
+ On the Relationship Between Static Analysis and Ty...
+ Michael Arntzenius on the Future of Coding Podcast
o ► July (1)
o ► May (2)
o ► April (1)
* ► 2018 (5)
o ► August (3)
o ► July (1)
o ► April (1)
* ► 2016 (7)
o ► September (1)
o ► May (2)
o ► April (2)
o ► March (2)
* ► 2015 (7)
o ► November (1)
o ► July (2)
o ► March (3)
o ► February (1)
* ► 2014 (13)
o ► December (2)
o ► November (2)
o ► October (1)
o ► July (2)
o ► June (2)
o ► March (2)
o ► February (1)
o ► January (1)
* ► 2013 (10)
o ► December (1)
o ► November (1)
o ► July (1)
o ► June (2)
o ► May (1)
o ► April (3)
o ► March (1)
* ► 2012 (15)
o ► December (1)
o ► November (4)
o ► August (5)
o ► July (1)
o ► May (1)
o ► April (1)
o ► March (1)
o ► January (1)
* ► 2011 (18)
o ► December (1)
o ► November (1)
o ► October (2)
o ► September (2)
o ► August (1)
o ► July (5)
o ► June (1)
o ► May (2)
o ► April (1)
o ► March (1)
o ► January (1)
* ► 2010 (1)
o ► November (1)
My Blog List
*
wingolog
guile lab notebook: on the move!
1 week ago
*
The n-Category Café
How to Count n-Ary Trees
2 weeks ago
*
Logic ForAll
Intuitionistic Modal Logic: are you sure?
4 weeks ago
*
Simon Marlow
Browsing Stackage with VS Code and Glean
5 weeks ago
*
QA9
A Script for Wadler’s Parable of LEM
2 months ago
*
Gagallium
Florian’s compiler weekly, 13 January 2025
6 months ago
*
Mathematics and Computation
Space-filling curves, constructively
1 year ago
*
Bob Atkey's blog
More Data Types with Negation at Fun in the REPL
1 year ago
*
Homotopy Type Theory
Workshop on Synthetic Algebraic Geometry
1 year ago
*
composition.al
CAREER: Building Reliable Distributed Systems with Refinement Types
3 years ago
*
niche computing science
Longest segment of balanced parentheses — an exercise in program
inversion in a segment problem
4 years ago
*
Theory Lunch
Positive expansivity is impossible for reversible cellular automata
5 years ago
*
The Programming Languages Enthusiast | Developments in PL, and why
they matter
“What is PL Research?” The Talk
6 years ago
*
pigworker in a space (Conor McBride)
Ming — a typecheckerchecker (episode 0)
6 years ago
*
A Neighborhood of Infinity
Why is nuclear fusion so hard?
6 years ago
*
Patterns in Functional Programming
How to design co-programs
6 years ago
*
Jeremy Siek
Reading list for getting started on Gradual Typing
6 years ago
*
Everything in Context
What we expect PhD students to know and learn
7 years ago
*
Why λλ?
Defining backticks using "pipe" operations
7 years ago
*
Existential Type
Proofs by contradiction, versus contradiction proofs
8 years ago
*
Notes from a Medium-Sized Island
8 years ago
*
The Lab Lunch
Moving sites
8 years ago
*
Lazily Typed
Fresh Start
9 years ago
*
carlo angiuli (blog)
J is singleton contractibility plus transport, definitionally
10 years ago
*
Herr Dreyer | Get used to disappointment.
Great Moments in Bureaucracy (Part 1: A Fistful of Euros)
10 years ago
*
Request for Logic
Life update, a TA blog
11 years ago
*
Proof Theory Abridged
Kripke models and the dialectica interpretation
11 years ago
*
The Paralyzing Paradoxes of Professor Polaro
reflecting and reifying the state monad
14 years ago
*
The Brown PLT Blog
*
Progress and Preservation
*
blog gallais
*
Bob Atkey's Blog
I use MathJax for mathematical layout.
Powered by Blogger .