jana/eelco-visser-compiler-construction
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
eelco-visser-compiler-const.../lecture/4.html

967 lines
16 KiB
HTML
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
<meta name="description" content="">
<meta name="author" content="Eelco Visser">
<meta name="generator" content="Jekyll v3.8.5">
<title>Lecture 4: Type Checking and Type Constraints</title>
<!-- <base href="/2021"> -->
<!--link rel="canonical" href="https://getbootstrap.com/docs/4.3/examples/starter-template/"-->
<link rel="icon" href="../img/logo/pl_ico2_2B3_icon.ico" type="image/x-icon">
<!-- Bootstrap core CSS -->
<!--link href="https://getbootstrap.com/docs/4.3/dist/css/bootstrap.min.css" rel="stylesheet" integrity="sha384-ggOyR0iXCbMQv3Xipma34MD+dH/1fQ784/j6cY/iJTQUOhcWr7x9JvoRxT2MZw1T" crossorigin="anonymous"-->
<link rel="stylesheet" href="https://stackpath.bootstrapcdn.com/bootstrap/4.3.1/css/bootstrap.min.css" integrity="sha384-ggOyR0iXCbMQv3Xipma34MD+dH/1fQ784/j6cY/iJTQUOhcWr7x9JvoRxT2MZw1T" crossorigin="anonymous">
<style>
.bd-placeholder-img {
font-size: 1.125rem;
text-anchor: middle;
-webkit-user-select: none;
-moz-user-select: none;
-ms-user-select: none;
user-select: none;
}
@media (min-width: 768px) {
.bd-placeholder-img-lg {
font-size: 3.5rem;
}
}
</style>
<!-- Custom styles for this template -->
<link href="../css/main.css" rel="stylesheet">
<link href="../css/borders-responsive.css" rel="stylesheet">
<link rel="stylesheet" href="../css/pl.css">
</head>
<body>
<nav class="navbar navbar-expand-md navbar-dark bg-dark fixed-top">
<a class="navbar-brand" href="../index.html">
TU Delft | CS4200
</a>
<button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarsExampleDefault" aria-controls="navbarsExampleDefault" aria-expanded="false" aria-label="Toggle navigation">
<span class="navbar-toggler-icon"></span>
</button>
<div class="collapse navbar-collapse" id="navbarsExampleDefault">
<ul class="navbar-nav mr-auto">
<li class="nav-item active">
<a class="nav-link" href="../lectures/index.html" tabindex="-1" aria-disabled="true">Lectures</a>
</li>
<li class="nav-item active">
<a class="nav-link" href="../homework/index.html" tabindex="-1" aria-disabled="true">Homework</a>
</li>
<li class="nav-item active">
<a class="nav-link" href="../project/index.html" tabindex="-1" aria-disabled="true">Project</a>
</li>
<li class="nav-item active">
<a class="nav-link" href="../news/index.html" tabindex="-1" aria-disabled="true">News</a>
</li>
<li class="nav-item active">
<a class="nav-link" href="../blog/index.html" tabindex="-1" aria-disabled="true">Blog</a>
</li>
</ul>
</div>
</nav>
<div class="container">
<div class="row">
<div class="col-sm-12 col-md-12 col-lg-12 col-xl-12">
<a href="../lectures/2021/04-type-constraints/CS4200-2021-4-type-checking.pdf">
<img class="border border-dark" width="100%" src="../lectures/2021/04-type-constraints/CS4200-2021-4-type-checking/CS4200-2021-4-type-checking.047.png"/>
</a>
<div class="mt-3 mb-3 pt-3 pb-3 text-dark border-top border-bottom border-grey">
<div class="text-dark font-weight-bold">
<h1>
Lecture 4: Type Checking and Type Constraints
</h1>
</div>
<div>
Eelco Visser
</div>
<div>
Lecture
| <a class="text-primary" href="../lectures/2021/04-type-constraints/CS4200-2021-4-type-checking.pdf">PDF</a>
</div>
<div>
September 16, 2021
</div>
</div>
</div>
</div>
<div class="row">
<div class="col-sm-12 col-md-12 col-lg-9 border-lg-right border-grey">
<p>In this lecture we study types and relations in types in programming languages, and discuss the motivation for having types.</p>
<p>Next we look at the way type systems are formalized. In particular, we look at the inference rules in the ChocoPy reference manual.</p>
<p>Finally, we start our study of the Statix meta-language for the specification of type systems. Ending with a demonstration of the <a href="https://github.com/MetaBorgCube/statix-sandbox/tree/master/chicago">Chicago</a> project (available on github), as an example of the use of Statix.</p>
<p>There are no papers that give concrete examples of Statix code, but the <a href="https://eelcovisser.org/publications/2016/AntwerpenNTVW16.pdf">PEPM 2016</a> paper gives a good introduction to the use of constraints and scope graphs, albeit in a somewhat more limited language than Statix.</p>
<h3 id="slides">Slides</h3>
<ul>
<li><a href="../lectures/2021/04-type-constraints/CS4200-2021-4-type-checking.pdf">Slides</a></li>
<li><a href="../lectures/2021/04-type-constraints/CS4200-2021-4-type-checking-builds.pdf">Slides with builds</a></li>
</ul>
<h3 id="statix-tutorial">Statix Tutorial</h3>
<p>This is a recording of a tutorial on Statix at the PLDI conference.</p>
<iframe width="560" height="315" src="https://www.youtube.com/embed/0GPZiZF5znA" frameborder="0" allow="accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture" allowfullscreen=""></iframe>
<h3 id="references">References</h3>
<ul class="list-group list-group-flush pb-3">
<li class="list-group-item pl-lg-0 border-0 pb-0">
<div class="bd-callout border-danger pl-3">
<div>
<a name="AntwerpenPRV18"></a>
<a class="font-weight-bold text-dark" target="_blank" href="https://doi.org/10.1145/3276484">Scopes as types</a>
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
<a class="text-secondary" href="https://nl.linkedin.com/in/hendrikvanantwerpen">Hendrik van Antwerpen</a>, <a class="text-secondary" href="http://www.casperbp.net">Casper Bach Poulsen</a>, <a class="text-secondary" href="https://www.linkedin.com/in/arjen-rouvoet-760347a5/">Arjen Rouvoet</a>, <a class="text-secondary" href="http://eelcovisser.org">Eelco Visser</a>.
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
PACMPL 2(OOPSLA) 2018
[<a href="../publications/2018/AntwerpenPRV18.pdf" class="text-secondary" target="_blank">pdf</a>, <a class="text-secondary" href="https://doi.org/10.1145/3276484" target="_blank">doi</a>, <a class="text-secondary" target="_blank" href="https://researchr.org/publication/AntwerpenPRV18/bibtex">bib</a>, <a href="https://researchr.org/publication/AntwerpenPRV18" class="text-secondary" target="_blank">researchr</a>, <a class="text-secondary" data-toggle="collapse" href="4.html#AbstractAntwerpenPRV18" role="button" aria-expanded="false" aria-controls="AbstractAntwerpenPRV18"">abstract</a>]
<!-- -->
</div>
<div class="collapse mt-1 mb-2" id="AbstractAntwerpenPRV18">
<div class="">
Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java.
</div>
</div>
</div>
</li>
<li class="list-group-item pl-lg-0 border-0 pb-0">
<div class="bd-callout border-primary pl-3">
<div>
<a name="AntwerpenNTVW16"></a>
<a class="font-weight-bold text-dark" target="_blank" href="http://doi.acm.org/10.1145/2847538.2847543">A constraint language for static semantic analysis based on scope graphs</a>
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
<a class="text-secondary" href="https://nl.linkedin.com/in/hendrikvanantwerpen">Hendrik van Antwerpen</a>, <a class="text-secondary" href="https://researchr.org/profile/pierrejeanmichelneron/publications">Pierre Néron</a>, <a class="text-secondary" href="http://www.cs.pdx.edu/~apt">Andrew P. Tolmach</a>, <a class="text-secondary" href="http://eelcovisser.org">Eelco Visser</a>, <a class="text-secondary" href="https://www.linkedin.com/in/guidowachsmuth/">Guido Wachsmuth</a>.
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
PEPM 2016
[<a href="../publications/2016/AntwerpenNTVW16.pdf" class="text-secondary" target="_blank">pdf</a>, <a class="text-secondary" href="http://doi.acm.org/10.1145/2847538.2847543" target="_blank">doi</a>, <a class="text-secondary" target="_blank" href="https://researchr.org/publication/AntwerpenNTVW16/bibtex">bib</a>, <a href="https://researchr.org/publication/AntwerpenNTVW16" class="text-secondary" target="_blank">researchr</a>, <a class="text-secondary" data-toggle="collapse" href="4.html#AbstractAntwerpenNTVW16" role="button" aria-expanded="false" aria-controls="AbstractAntwerpenNTVW16"">abstract</a>]
<!-- -->
</div>
<div class="collapse mt-1 mb-2" id="AbstractAntwerpenNTVW16">
<div class="">
In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs -- such as record field access -- for which binding and typing are mutually dependent. We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for a wider range of scope relationships. We describe the details of constraint generation for a model language that illustrates many of the interesting static analysis issues associated with modules and records.
</div>
</div>
</div>
</li>
<li class="list-group-item pl-lg-0 border-0 pb-0">
<div class="bd-callout border-primary pl-3">
<div>
<a name="NeronTVW15"></a>
<a class="font-weight-bold text-dark" target="_blank" href="http://dx.doi.org/10.1007/978-3-662-46669-8\_9">A Theory of Name Resolution</a>
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
<a class="text-secondary" href="https://researchr.org/profile/pierrejeanmichelneron/publications">Pierre Néron</a>, <a class="text-secondary" href="http://www.cs.pdx.edu/~apt">Andrew P. Tolmach</a>, <a class="text-secondary" href="http://eelcovisser.org">Eelco Visser</a>, <a class="text-secondary" href="https://www.linkedin.com/in/guidowachsmuth/">Guido Wachsmuth</a>.
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
ESOP 2015
[<a href="../publications/2015/NeronTVW15.pdf" class="text-secondary" target="_blank">pdf</a>, <a class="text-secondary" href="http://dx.doi.org/10.1007/978-3-662-46669-8\_9" target="_blank">doi</a>, <a class="text-secondary" target="_blank" href="https://researchr.org/publication/NeronTVW15/bibtex">bib</a>, <a href="https://researchr.org/publication/NeronTVW15" class="text-secondary" target="_blank">researchr</a>, <a class="text-secondary" data-toggle="collapse" href="4.html#AbstractNeronTVW15" role="button" aria-expanded="false" aria-controls="AbstractNeronTVW15"">abstract</a>]
<!-- -->
</div>
<div class="collapse mt-1 mb-2" id="AbstractNeronTVW15">
<div class="">
We describe a language-independent theory for name binding and resolution, suitable for programming languages with complex scoping rules including both lexical scoping and modules. We formulate name resolution as a two-stage problem. First a language-independent scope graph is constructed using language-specific rules from an abstract syntax tree. Then references in the scope graph are resolved to corresponding declarations using a language-independent resolution process. We introduce a resolution calculus as a concise, declarative, and languageindependent specification of name resolution. We develop a resolution algorithm that is sound and complete with respect to the calculus. Based on the resolution calculus we develop language-independent definitions of α-equivalence and rename refactoring. We illustrate the approach using a small example language with modules. In addition, we show how our approach provides a model for a range of name binding patterns in existing languages.
</div>
</div>
</div>
</li>
</ul>
</div>
<div class="col-sm-12 col-md-12 col-lg-3 col-xl-3 " >
<div class="sticky-top top70 d-none d-lg-block d-xl-block">
<div class="pb4 mb3 border-bottom border-grey ">
<nav>
<ul class="pagination justify-content-left">
<li class="page-item">
<a class="page-link" href="3.html">
&laquo;
</a>
</li>
<li class="page-item">
<a class="page-link" href="../lectures/index.html">
^
</a>
</li>
<li class="page-item">
<a class="page-link" href="5.html">&raquo;</a>
</li>
</ul>
</nav>
</div>
<ul id="my_toc" class="toc list-group list-group-flush d-none d-lg-block d-xl-block p-0 ml-0 mt-3">
<li class="list-group-item pl-0 ml-0 border-0 pl-0 pt-0 pb-1 pr-0 m-0 mr-3"><a href="4.html#slides">Slides</a></li>
<li class="list-group-item pl-0 ml-0 border-0 pl-0 pt-0 pb-1 pr-0 m-0 mr-3"><a href="4.html#statix-tutorial">Statix Tutorial</a></li>
<li class="list-group-item pl-0 ml-0 border-0 pl-0 pt-0 pb-1 pr-0 m-0 mr-3"><a href="4.html#references">References</a></li>
</ul>
</div>
</div>
</div>
<div class="row">
<div class="col-12">
<div class="border-top border-bottom border-grey mt-3 pt-3">
<nav>
<ul class="pagination justify-content-center">
<li class="page-item">
<a class="page-link" href="3.html">
Previous
</a>
</li>
<li class="page-item">
<a class="page-link" href="5.html">Next</a>
</li>
<li class="page-item">
<a class="page-link" href="../lectures/index.html">
Index
</a>
</li>
</ul>
</nav>
</div>
</div>
</div>
</div>
<!-- Optional JavaScript -->
<!-- jQuery first, then Popper.js, then Bootstrap JS -->
<script src="https://code.jquery.com/jquery-3.3.1.slim.min.js" integrity="sha384-q8i/X+965DzO0rT7abK41JStQIAqVgRVzpbzo5smXKp4YfRvH+8abtTE1Pi6jizo" crossorigin="anonymous"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/popper.js/1.14.7/umd/popper.min.js" integrity="sha384-UO2eT0CpHqdSJQ6hJty5KVphtPhzWj9WO1clHTMGa3JDZwrnQq4sF86dIHNDz0W1" crossorigin="anonymous"></script>
<script src="https://stackpath.bootstrapcdn.com/bootstrap/4.3.1/js/bootstrap.min.js" integrity="sha384-JjSmVgyd0p3pXB1rRibZUAYoIIy6OrQ6VrjIEaFf/nJGzIxFDsf4x0xIM+B07jRM" crossorigin="anonymous"></script>
</body>
</html>
Reference in a new issue View git blame Copy permalink