320 lines
14 KiB
HTML
320 lines
14 KiB
HTML
<!DOCTYPE html>
|
||
<html lang="en"><head>
|
||
<meta charset="utf-8">
|
||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||
<meta name="viewport" content="width=device-width, initial-scale=1">
|
||
<title>Preface | Programming Language Foundations in Agda
|
||
</title><!-- Begin Jekyll SEO tag v2.6.1 -->
|
||
<meta name="generator" content="Jekyll v3.9.0" />
|
||
<meta property="og:title" content="Preface" />
|
||
<meta property="og:locale" content="en_US" />
|
||
<meta name="description" content="Programming Language Foundations in Agda" />
|
||
<meta property="og:description" content="Programming Language Foundations in Agda" />
|
||
<link rel="canonical" href="https://plfa.github.io/20.07/Preface/" />
|
||
<meta property="og:url" content="https://plfa.github.io/20.07/Preface/" />
|
||
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
||
<script type="application/ld+json">
|
||
{"url":"https://plfa.github.io/20.07/Preface/","headline":"Preface","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
|
||
<!-- End Jekyll SEO tag -->
|
||
<link rel="stylesheet" href="/20.07/assets/main.css"></head>
|
||
<body><header class="site-header" role="banner">
|
||
|
||
<div class="wrapper">
|
||
|
||
<a class="site-title" href="/20.07/">Programming Language Foundations in Agda
|
||
</a>
|
||
|
||
<nav class="site-nav">
|
||
<span class="menu-icon">
|
||
<svg viewBox="0 0 18 15" width="18px" height="15px">
|
||
<path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
|
||
<path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
|
||
<path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
|
||
</svg>
|
||
</span>
|
||
|
||
<div class="trigger">
|
||
<a class="page-link" href="/20.07/">The Book</a>
|
||
<a class="page-link" href="/20.07/Announcements/">Announcements</a>
|
||
<a class="page-link" href="/20.07/GettingStarted/">Getting Started</a>
|
||
<a class="page-link" href="/20.07/Citing/">Citing</a>
|
||
<a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a>
|
||
</div>
|
||
</nav>
|
||
|
||
</div>
|
||
|
||
</header>
|
||
<main class="page-content" aria-label="Content">
|
||
<div class="wrapper">
|
||
<article class="post">
|
||
|
||
<header class="post-header">
|
||
<h1 class="post-title">Preface</h1>
|
||
</header>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
<a alt="Previous chapter" href="/20.07/Dedication/">Prev</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
|
||
|
||
<a alt="Next chapter" href="/20.07/Naturals/">Next</a>
|
||
|
||
</p>
|
||
|
||
|
||
<div class="post-content">
|
||
<p>The most profound connection between logic and computation is a pun.
|
||
The doctrine of Propositions as Types asserts that a certain kind of
|
||
formal structure may be read in two ways: either as a proposition in
|
||
logic or as a type in computing. Further, a related structure may be
|
||
read as either the proof of the proposition or as a programme of the
|
||
corresponding type. Further still, simplification of proofs
|
||
corresponds to evaluation of programs.</p>
|
||
|
||
<p>Accordingly, the title of this book also has two readings. It may be
|
||
parsed as “(Programming Language) Foundations in Agda” or “Programming
|
||
(Language Foundations) in Agda” — the specifications we will write in
|
||
the proof assistant Agda both describe programming languages and are
|
||
themselves programmes.</p>
|
||
|
||
<p>The book is aimed at students in the last year of an undergraduate
|
||
honours programme or the first year of a master or doctorate degree.
|
||
It aims to teach the fundamentals of operational semantics of
|
||
programming languages, with simply-typed lambda calculus as the
|
||
central example. The textbook is written as a literate script in
|
||
Agda. The hope is that using a proof assistant will make the
|
||
development more concrete and accessible to students, and give them
|
||
rapid feedback to find and correct misapprehensions.</p>
|
||
|
||
<p>The book is broken into two parts. The first part, Logical
|
||
Foundations, develops the needed formalisms. The second part,
|
||
Programming Language Foundations, introduces basic methods of
|
||
operational semantics.</p>
|
||
|
||
<h2 id="personal-remarks">Personal remarks</h2>
|
||
|
||
<p>Since 2013, I have taught a course on Types and Semantics for
|
||
Programming Languages to fourth-year undergraduates and masters
|
||
students at the University of Edinburgh. An earlier version of that
|
||
course was based on Benjamin Pierce’s excellent <a href="https://www.cis.upenn.edu/~bcpierce/tapl/">TAPL</a>. My
|
||
version was based of Pierce’s subsequent textbook, <a href="https://softwarefoundations.cis.upenn.edu/">Software
|
||
Foundations</a>, written in collaboration with others and based on
|
||
Coq. I am convinced of Pierce’s claim that basing a course around a
|
||
proof assistant aids learning, as summarised in his ICFP Keynote,
|
||
<a href="https://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf">Lambda, The Ultimate TA</a>.</p>
|
||
|
||
<p>However, after five years of experience, I have come to the conclusion
|
||
that Coq is not the best vehicle. Too much of the course needs to
|
||
focus on learning tactics for proof derivation, to the cost of
|
||
learning the fundamentals of programming language theory. Every
|
||
concept has to be learned twice: e.g., both the product data type, and
|
||
the corresponding tactics for introduction and elimination of
|
||
conjunctions. The rules Coq applies to generate induction hypotheses
|
||
can sometimes seem mysterious. While the <code class="language-plaintext highlighter-rouge">notation</code> construct permits
|
||
pleasingly flexible syntax, it can be confusing that the same concept
|
||
must always be given two names, e.g., both <code class="language-plaintext highlighter-rouge">subst N x M</code> and <code class="language-plaintext highlighter-rouge">N [x :=
|
||
M]</code>. Names of tactics are sometimes short and sometimes long; naming
|
||
conventions in the standard library can be wildly inconsistent.
|
||
<em>Propositions as types</em> as a foundation of proof is present but
|
||
hidden.</p>
|
||
|
||
<p>I found myself keen to recast the course in Agda. In Agda, there is
|
||
no longer any need to learn about tactics: there is just
|
||
dependently-typed programming, plain and simple. Introduction is
|
||
always by a constructor, elimination is always by pattern
|
||
matching. Induction is no longer a mysterious separate concept, but
|
||
corresponds to the familiar notion of recursion. Mixfix syntax is
|
||
flexible while using just one name for each concept, e.g.,
|
||
substitution is <code class="language-plaintext highlighter-rouge">_[_:=_]</code>. The standard library is not perfect, but
|
||
there is a fair attempt at consistency. <em>Propositions as types</em> as a
|
||
foundation of proof is on proud display.</p>
|
||
|
||
<p>Alas, there is no textbook for programming language theory in
|
||
Agda. Stump’s <a href="https://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?cPath=24&products_id=908">Verified Functional Programming in Agda</a> covers
|
||
related ground, but focusses more on programming with dependent
|
||
types than on the theory of programming languages.</p>
|
||
|
||
<p>The original goal was to simply adapt <em>Software Foundations</em>,
|
||
maintaining the same text but transposing the code from Coq to Agda.
|
||
But it quickly became clear to me that after five years in the
|
||
classroom I had my own ideas about how to present the material. They
|
||
say you should never write a book unless you cannot <em>not</em> write the
|
||
book, and I soon found that this was a book I could not not write.</p>
|
||
|
||
<p>I am fortunate that my student, <a href="https://github.com/wenkokke">Wen Kokke</a>, was keen to help.
|
||
She guided me as a newbie to Agda and provided an infrastructure that
|
||
is easy to use and produces pages that are a pleasure to view.</p>
|
||
|
||
<p>Most of the text was written during a sabbatical in the first half of 2018.</p>
|
||
|
||
<p>— Philip Wadler, Rio de Janeiro, January–June 2018</p>
|
||
|
||
<h2 id="a-word-on-the-exercises">A word on the exercises</h2>
|
||
|
||
<p>Exercises labelled “(recommended)” are the ones students are
|
||
required to do in the class taught at Edinburgh from this textbook.</p>
|
||
|
||
<p>Exercises labelled “(stretch)” are there to provide an extra challenge.
|
||
Few students do all of these, but most attempt at least a few.</p>
|
||
|
||
<p>Exercises labelled “(practice)” are included for those who want extra
|
||
practice.</p>
|
||
|
||
<p>You may need to import library functions required for the solution.</p>
|
||
|
||
|
||
</div>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
<a alt="Previous chapter" href="/20.07/Dedication/">Prev</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
|
||
|
||
<a alt="Next chapter" href="/20.07/Naturals/">Next</a>
|
||
|
||
</p>
|
||
|
||
|
||
</article>
|
||
|
||
</div>
|
||
</main><footer class="site-footer h-card">
|
||
<data class="u-url" href="/20.07/"></data>
|
||
|
||
<div class="wrapper">
|
||
|
||
<h2 class="footer-heading">Programming Language Foundations in Agda
|
||
</h2><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Philip Wadler</li>
|
||
<li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Wen Kokke</li>
|
||
<li><a class="u-email" href="mailto:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Jeremy G. Siek</li>
|
||
<li><a class="u-email" href="mailto:jsiek@indiana.edu">jsiek@indiana.edu</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a>
|
||
</div>
|
||
</footer>
|
||
<!-- Import jQuery -->
|
||
<script type="text/javascript" src="/20.07/assets/jquery.js"></script>
|
||
|
||
<script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.2.2/anchor.min.js" integrity="sha256-E4RlfxwyJVmkkk0szw7LYJxuPlp6evtPSBDlWHsYYL8=" crossorigin="anonymous"></script>
|
||
<script type="text/javascript">
|
||
anchors.add();
|
||
</script>
|
||
|
||
<script type="text/javascript">
|
||
|
||
// Makes sandwhich menu works
|
||
$('.menu-icon').click(function(){
|
||
$('.trigger').toggle();
|
||
});
|
||
|
||
// Script which allows for foldable code blocks
|
||
$('div.foldable pre').each(function(){
|
||
var autoHeight = $(this).height();
|
||
var lineHeight = parseFloat($(this).css('line-height'));
|
||
|
||
var plus = $("<div></div>");
|
||
var horLine = $("<div></div>");
|
||
var verLine = $("<div></div>");
|
||
$(this).prepend(plus);
|
||
plus.css({
|
||
'position' : 'relative',
|
||
'float' : 'right',
|
||
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
||
'width' : lineHeight,
|
||
'height' : lineHeight});
|
||
verLine.css({
|
||
'position' : 'relative',
|
||
'height' : lineHeight,
|
||
'width' : '3px',
|
||
'background-color' : '#C1E0FF'});
|
||
horLine.css({
|
||
'position' : 'relative',
|
||
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
|
||
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
||
'height' : '3px',
|
||
'width' : lineHeight,
|
||
'background-color' : '#C1E0FF'});
|
||
plus.append(verLine);
|
||
plus.append(horLine);
|
||
|
||
$(this).height(2.0 * lineHeight);
|
||
$(this).css('overflow','hidden');
|
||
|
||
$(this).click(function(){
|
||
if ($(this).height() == autoHeight) {
|
||
$(this).height(2.0 * lineHeight);
|
||
plus.show();
|
||
}
|
||
else {
|
||
$(this).height('auto');
|
||
plus.hide();
|
||
}
|
||
});
|
||
});
|
||
</script>
|
||
|
||
<!-- Import KaTeX -->
|
||
<script type="text/javascript" src="/20.07/assets/katex.js"></script>
|
||
|
||
<!-- Script which renders TeX using KaTeX -->
|
||
<script type="text/javascript">
|
||
$("script[type='math/tex']").replaceWith(
|
||
function(){
|
||
var tex = $(this).text();
|
||
return "<span class=\"inline-equation\">" +
|
||
katex.renderToString(tex) +
|
||
"</span>";
|
||
});
|
||
$("script[type='math/tex; mode=display']").replaceWith(
|
||
function(){
|
||
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
|
||
return "<div class=\"equation\">" +
|
||
katex.renderToString("\\displaystyle "+tex) +
|
||
"</div>";
|
||
});
|
||
</script>
|
||
</body>
|
||
|
||
</html>
|