-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
245 lines (188 loc) · 18.2 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
<!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>DVA311</title>
<!-- Bootstrap -->
<link href="css/bootstrap.min.css" rel="stylesheet">
<link href="css/custom.css" rel="stylesheet">
<link href="css/print.css" rel="stylesheet" media="print">
<!--[if lt IE 9]>
<script src="https://oss.maxcdn.com/html5shiv/3.7.2/html5shiv.min.js"></script>
<script src="https://oss.maxcdn.com/respond/1.4.2/respond.min.js"></script>
<![endif]-->
</head>
<body>
<!-- Begin page content -->
<div class="container">
<h2>Types and Programming Languages, 15hp</h2>
<div class="well hidden-print">
<ul>
<li><strong>2018-05-28</strong> Initial version.
</li>
</ul>
</div>
<div class="page-header nobreak">
<h2>Course plan</h2>
<p> This project course instance mixes theory and practice of types and programming languages. The course is
built on the excellent book
<strong>Types and Programming Languages</strong> by Benjamin Pierce. Every week treats a specific topic from
the book and is examined by an implementation. The result is a type checker and evaluator for a
small but powerful strict functional language. This page will serve as the project report - each week will
be extended with a short digest of the material of the week together with links to the implementation work.
</p>
<div class="list-group">
<div class="list-group-item">
<span class="date">Jun 18</span>
<h4 class="list-group-item-heading">#1; Untyped Lambda Calculus</h4>
<p>
The untyped lambda calculus was created by Alonzo Church in the 1930s. It is a small formal system which at the time of its creation had no direct relationship to computers. The system has three syntactic rules: function abstraction, function application, and variables. Despite it's mere size, the untyped lambda calculus is Turing complete, as proven by Alan Turing. As a model of computation, the system is unique in its simplicity and flexibility, allowing for different kinds of extensions. It's perhaps not surprising then that John McCarthy used the untyped lambda calculus as a foundation for the first functional programming language, Lisp, in 1958. Since then, lambda calculus has been prominent in the world of programming languages. It can be found in different forms at the core of every functional programming language and its ideas are featured in many other programming languages as well.
</p>
<p>
We choose to implement the untyped lambda calculus with an ML-inspired syntax, where abstractions are denoted with the fun keyword and a right-pointing arrow following the parameter, like so: <code>fun x -> x</code>. The motivation behind this decision is simple: throughout the course we will develop a functional programming language that is essentially a subset of ML. In line with the course material, evaluation is based on substitution, instead of a lookup-based approach, reflecting the goal of the course: developing an interpreter for the learning experience, not for the sake of creating an industry-grade product.
</p>
<p>
The lambda calculus can be implemented with different evaluation strategies: call-by-value, call-by-name and call-by-need. Since ML employs a strict call-by-value evaluation strategy, we choose to reflect this in our implementation. This means that the arguments in function applications are evaluated to value-form before they are substituted into the body. Finally, instead of representing variables explicitly by name, the evaluator makes use of de Brujin indexing, where variables are identified based on the depth that they occur in the abstract syntax tree.
</p>
<dl class="dl-horizontal">
<dt>Theory</dt>
<dd>TaPL; chapters 3, 5</dd>
<dt>Practice</dt>
<dd>Evaluator for untyped lambda calculus.</dd>
<dt>Code</dt>
<dd><a href="code/w1-untyped.zip">untyped lambda calculus</a></dd>
</dl>
</div>
<div class="list-group-item">
<span class="date">Jun 25</span>
<h4 class="list-group-item-heading">#2; Simply Typed Lambda Calculus</h4>
<p>
The simply typed lambda calculus is a constrained version of lambda calculus. In fact, the typing rules are so constraining that the simply typed calculus is not turing complete. In the untyped lambda calculus, recursion can be encoded with the help of the y-combinator. While in the simply typed lambda calculus, the y-combinator is not well typed. This is unfortunate for our purposes since we are interested in developing a useful programming language, and to do that we need recursion. Luckily there is a way to remedy this by introducing something called the fixed-point combinator, which we will see next week. Despite the loss of the ability to encode recursion, the simply typed lambda calculus is still useful for theoretical purposes. The typing rules makes the system strongly normalizing, which means that any well typed expressions can be rewritten to an irreducible term. Another way to interpret this: well typed programs always terminate.
</p>
<dl class="dl-horizontal">
<dt>Theory</dt>
<dd>TaPL; chapters 8, 9</dd>
<dt>Practice</dt>
<dd>Type checker and evaluator for simply typed lambda calculus.</dd>
<dt>Code</dt>
<dd><a href="code/w2-simply_typed.zip">simply typed lambda calculus</a></dd>
</dl>
</div>
<div class="list-group-item">
<span class="date">Jul 2</span>
<h4 class="list-group-item-heading">#3; Simple Extensions </h4>
<p>
As previously mentioned, we can introduce the capability for recursion using the fixed-point combinator. In our language, this feature is accessed through the ML-style letrec-construct <code>let rec f x = f x</code>. These recursive let bindings are desugared to let bindings that make use of the fixed-point operator. A recursive function <code>let rec f x = f x</code> is desugared into <code>let f = fix (fun f -> fun x -> f x)</code>. When we evaluate the fix operator, we substitute f in the body for the whole expression and return the body, like so: <code>fun f -> fun x -> (fix (fun f -> fun x -> f x)) x</code>.
</p>
<p>
In the book, Pierce notes that a let-binding like <code>let x = 1335 in x + 2</code> can be desugared into <code>(fun x -> x + 2) 1337</code>. However, our interpreter does not perform this transformation because explicitly representing the let-construct in the abstract syntax tree enables let-polymorphism, which is essential for Damas-Hindley-Milner style type inference.
</p>
<dl class="dl-horizontal">
<dt>Theory</dt>
<dd>TaPL; chapter 11</dd>
<dt>Practice</dt>
<dd>Extensions: let, tuples and records.</dd>
<dt>Code</dt>
<dd><a href="code/w3-simple_extensions.zip">simple extensions</a></dd>
</dl>
</div>
<div class="list-group-item">
<span class="date">Jul 9</span>
<h4 class="list-group-item-heading">#4; References</h4>
<p>
References in ML are pointers to locations in a store. For our implementation, we chose to represent the store as array of terms. Just like in ML, our language comes with syntax for creating, dereferencing, and assigning to references. Assignment and dereferencing looks the same way as in any other ML, but the syntax for creating references actually takes inspiration from C++ and Rust. While in ML, a reference to the number 1337 is created like so: <code>let x = ref 1337</code>, in our language it looks like this <code> let x = &1337</code>. With the addition of references, our language is no longer pure; we have introduced the capability of working with side effects.
</p>
<dl class="dl-horizontal">
<dt>Theory</dt> <dd>TaPL; chapter 13</dd>
<dt>Practice</dt> <dd>Extension: references.</dd>
<dt>Code</dt> <dd><a href="code/w4-references.zip">references</a></dd>
</dl>
</div>
<div class="list-group-item">
<span class="date">Jul 16</span>
<h4 class="list-group-item-heading">#5; Subtyping </h4>
<p>
Subtyping is a concept found in most modern programming languages, in the form of interfaces and inheritance between classes in C#, type classes in Haskell, and structural subtyping in OCaml. Although the concept manifests itself in different ways, the fundamental idea remains the same: if type A is a subtype of type B, we can treat an instance of type A like an instance of type B. This means that we safely call functions that were written for a type B with instances of type A. Except for saving us programmers from doing rewriting code, subtyping can aid in the design of systems, enabling modular architectures that otherwise would have been too complicated to implement.
</p>
<p>
In the book, Pierce deals predominantly with structural subtyping, as found in OCaml. Structural subtyping comes in two kinds: width subtyping and depth subtyping. In a system with width subtyping for records, the record type <code>T = {x: Int, y: Bool}</code> is considered to be a subtype of the record type <code> S = {x: Int}</code> because its members are a superset of those in <code>S</code>. With this established, we can use instances of the type <code>S</code> as arguments to functions that demand an instance of type <code>T</code>. Intuitively, this works since functions of <code>S</code> only require that the passed arguments contains a member named <code>x</code> with the type <code>Int</code>. Depth subtyping is an extension of this concept, where each individual member can be a subtype of the corresponding member in the supertype.
</p>
<p>
Subtyping interacts in interesting ways with already present language features. Since our language contains higher order functions, we must take into account that functions which are passed in and returned from other functions may be parameterized by records and thus we must have a subtyping rules for functions as well. Just like with records, use functions of different types as arguments and returns, as long as they are a subtype of the expected type. It turns out that for a function <code>f</code> to be a subtype of function <code>g</code>, the parameters of <code>f</code> have to be supertypes of those of <code>g</code>, and the return type of <code>f</code> has to be a subtype of <code>g</code>. We say that functions are contravariant in its parameter types and covariant in its return type
</p>
<dl class="dl-horizontal">
<dt>Theory</dt>
<dd>TaPL; chapters 15, 16</dd>
<dt>Practice</dt>
<dd>Extension: width subtyping for records.</dd>
<dt>Code</dt>
<dd><a href="code/w5-width_subtyping.zip">width subtyping</a></dd>
</dl>
</div>
<div class="list-group-item">
<span class="date">Jul 30</span>
<h4 class="list-group-item-heading">#6 - 7; Recursive Types</h4>
<p>
Pierce presents two ways to model recursive types: equi-recursive types, and iso-recursive types. In the equi-recursive model, we consider each recursive type to be a structure with infinite expansions of itself, essentially an infinite tree. This way, two type expressions can be considered equivalent when they have the same infinite expansion. Pierce notes that equi-recursive types are not practical for implementation purposes, but instead they are useful for theoretical work. The main reason for this is that the augmentation of equi-recursive types to an existing system does not affect the correctness of previously derived theorems. This saves us from having to reformulate the proofs we constructed in the initial system.
</p>
<p>
In the iso-recursive model, the recursion is contained with the help of two type constructs called fold and unfold. Wrapping a type with the fold construct allows us to represent a contraction of the recursion in a type, while unfold is the expansion of the recursion in a type. Fold and unfold are each others inverses and thus they cancel each other out. To enable the iso-recursive model, we have to insert folds and unfolds whenever a user of the programming language wants to work with recursive types.
</p><p>
Fortunately, with an ML style programming language we can easily hide this detail from the user because the points at which we need to insert fold and unfold naturally correspond with the syntactic constructs for working with algebraic data types. Whenever we see a constructor for an algebraic data type being used we insert a fold, and whenever we see a pattern match expression we insert an unfold. In our implementation we did not need to represent fold and unfold explicitly since the only well-typed way of working with an algebraic data type is to first construct it and then pattern match on it, a sequence which cancel each out in terms of fold and unfold. We avoid non-termination in the typechecker by representing self-references within a type as just a string equal to the name of the type instead of the whole structure. We believe this to be conceptually equivalent to explicitly representing fold and unfold; our approach is just a the different way to encode the same idea.
</p>
<dl class="dl-horizontal">
<dt>Theory</dt>
<dd>TaPL; chapters 20, 21</dd>
<dt>Practice</dt>
<dd>Extension: algebraic data types.</dd>
<dt>Code</dt>
<dd><a href="code/w7-adts.zip">algebraic data types</a></dd>
</dl>
</div>
<div class="list-group-item">
<span class="date">Aug 13</span>
<h4 class="list-group-item-heading">#8 - 9; Type Reconstruction </h4>
<p>
We implemented a variant of the original Algorithm W which is a bit different to Pierce's. The algorithm revolves around generating type constraints and solving them in order to accumulate a set of substitutions that when applied to an initial type of an expressions give us the most general type for that expression. While the algorithm is fine for a small language, we found that it quickly became unwieldy for our language - the code became hard to follow and hard to reason about. The problem stemmed from the algorithms intertwining of the generation of constraints and the solving of constraints. So, we decided to separate the algorithm into two passes; the first one generates constraints and the second one solves them.
</p>
<p>
While implementing the algorithm, we found that implicit structural subtyping for records does not work well with Damas-Hindley-Milner style type inference. Subtyping demands constraints that are directed, saying that a type is a subtype of a specific type. The unification in Algorithm W only works with undirected constraints, such as equality. Because of this, we decided to remove all support for implicit structural subtyping in the language. However, we do see the need for subtyping and we are considering it as a future addition to our language. More specifically, we are interested in subtyping in the style of type classes, as can be found in Haskell and Idris.
</p>
<dl class="dl-horizontal">
<dt>Theory</dt>
<dd>TaPL; chapter 22</dd>
<dt>Practice</dt>
<dd>Extension: Hindley-Milner type inference.</dd>
<dt>Code</dt>
<dd><a href="code/w9-inference.zip">type inference</a></dd>
</dl>
</div>
<div class="list-group-item">
<span class="date">Aug 20</span>
<h4 class="list-group-item-heading">#10; Interactive REPL</h4>
<p>
Finally, we have implemented an interactive REPL for working with our language. An image called jmldemo1.png is included with the source code in the attached .zip-file. The image shows a session of working with the REPL from the command line, showing the syntax for most of the constructs in the language as well as the quit commad. Except for <code>:quit</code>, there's also a command for clearing the screen <code>:clear</code>, and a command to change the verbosity of output, with three levels: <code>:show nothing</code>, <code>:show something</code> (the default), and <code>:show everything</code>. Remember to end a line with <code>;;</code> when you want your expression to be evaluated. To run the REPL you must have the latest version of dotnet core installed, you can find it <a href="https://www.microsoft.com/net/learn/get-started-with-dotnet-tutorial">here</a>. When you have dotnet core installed and in your path variable, cd into the project folder and run the command <code>dotnet run</code>.
</p>
<dl class="dl-horizontal">
<dt>Code</dt>
<dd><a href="code/w10-final.zip">final</a></dd>
</dl>
</div>
</div>
</div>
</div>
<footer class="footer hidden-print">
<div class="container">
<p class="text-muted">DVA311 - Types and Programming Languages</p>
</div>
</footer>
<!-- IE10 viewport hack for Surface/desktop Windows 8 bug -->
<script src="../../assets/js/ie10-viewport-bug-workaround.js"></script>
<!-- jQuery (necessary for Bootstrap's JavaScript plugins) -->
<script src="https://ajax.googleapis.com/ajax/libs/jquery/1.11.3/jquery.min.js"></script>
<!-- Include all compiled plugins (below), or include individual files as needed -->
<script src="js/bootstrap.min.js"></script>
</body>
</html>