gdritter repos gcct / 70a2083
Added presentation Getty Ritter 9 years ago
6 changed file(s) with 898 addition(s) and 487 deletion(s). Collapse all Expand all
+0
-7
Makefile less more
1 all: gcct.pdf
2
3 gcct.pdf: gcct.tex
4 pdflatex gcct.tex
5
6 clean:
7 rm -rf gcct.aux gcct.log gcct.pdf
+0
-480
gcct.tex less more
1 \documentclass{scrartcl}
2 \usepackage[letterpaper]{geometry}
3 \usepackage{fullpage}
4 \usepackage{cmbright}
5 \usepackage[usenames,dvipsnames]{color}
6 % \newcommand{\both}[2]{\begin{tabular}{ p{4in} p{4in} } #1 && #2 \\ \end{tabular}}
7 \newcommand{\pos}[1]{\textcolor{BrickRed}{#1}}
8 \newcommand{\postt}[1]{\textcolor{BrickRed}{\texttt{#1}}}
9 \newcommand{\dual}[1]{\textcolor{NavyBlue}{#1}}
10 \newcommand{\dualtt}[1]{\textcolor{NavyBlue}{\texttt{#1}}}
11 \newenvironment{both}
12 { \begin{tabular}{ p{3in} p{3in} } }
13 { \\ \end{tabular} }
14 \begin{document}
15 \section{\pos{Data} and \dual{Codata}}
16
17 \begin{both}
18 \pos{Data} is defined by its \pos{introduction} rules.
19 & \dual{Codata} is defined by its \dual{elimination} rules.
20 \\
21 We can define a \pos{data} type with
22 & We can define a \dual{codata} type with
23 \\
24 \color{BrickRed}
25 \begin{verbatim}
26 data Either a b
27 = Left a
28 | Right b\end{verbatim}
29 &
30 \color{NavyBlue}
31 \begin{verbatim}
32 codata Both a b
33 = first a
34 & second b\end{verbatim}
35 \\
36 This definition introduces two functions:
37 & This definition introduces two functions:
38 \\
39 \color{BrickRed}
40 \begin{verbatim}
41 Left : a -> Either a b
42 Right : b -> Either a b\end{verbatim}
43 &
44 \color{NavyBlue}
45 \begin{verbatim}
46 first : Both a b -> a
47 second : Both a b -> b\end{verbatim}
48 \\
49 In order to \pos{destruct data} we have to use
50 \pos{patterns} which let you match on \pos{constructors}.
51 & In order to \dual{construct codata} we have to use
52 \dual{copatterns} which let you match on \dual{destructors}.
53 \\
54 \color{BrickRed}
55 \begin{verbatim}
56 (case e : Either a b of
57 Left (x : a) -> (e1 : c)
58 Right (y : b) -> (e2 : c)) : c\end{verbatim}
59 &
60 \color{NavyBlue}
61 \begin{verbatim}
62 (merge x : Both a b from
63 first x <- e1 : a
64 second x <- e2 : b) : Both a b\end{verbatim}
65 \\
66 Here, \postt{e} represents the \pos{value being
67 destructed}, and each branch represents a \pos{constructor
68 with which it might have been constructed}. We are effectively
69 \pos{dispatching on possible pasts} of
70 \postt{e}.
71 & Here, \dual{\texttt{x}} represents the \dual{value being
72 constructed}, and each branch represents a \dual{destructor
73 with which it might eventually be destructed}. We are effectively
74 \dual{dispatching on possible futures} of
75 \dualtt{x}.
76 \\
77 \end{both}
78
79 \section{Codata, Records, and Copatterns}
80 \raggedright
81
82 In the same way that named sums are a natural way to represent data,
83 records are a natural way to represent codata. In lieu of the above
84 syntax, one often sees codata represented as something more like
85
86 {\color{NavyBlue}
87 \begin{verbatim}
88 record Both a b = { .first : a, .second : b }
89
90 x : Both Int Bool
91 x = { .first = 2, .second = true }
92
93 x.first == 2, x.second == true
94 \end{verbatim}
95 }
96
97 The \dualtt{merge} syntax is used here for conceptual
98 symmetry with \postt{case}. Additionally, the use of
99 copatterns is nicely dual with the extra expressivity that
100 patterns offer. For example, we can use nested patterns with
101 constructors of various types, as in this function which
102 processes a list of \postt{Either Int Bool} values
103 by summing the integers in the list until it reaches a
104 \postt{false} value or the end of the list:
105
106 {\color{BrickRed}
107 \begin{verbatim}
108 f : List (Either Int Bool) -> Int
109 f lst = case lst of
110 Cons (Left i) xs -> i + f xs
111 Cons (Right b) xs -> if b then f xs else 0
112 Nil -> 0
113 \end{verbatim}
114 }
115
116 Similarly, we can define an infinite stream of pairs using
117 nested copatterns as so:
118
119 {\color{NavyBlue}
120 \begin{verbatim}
121 s : Int -> Stream (Both Int Bool)
122 s n = merge x from
123 first (head x) <- n
124 second (head x) <- n > 0
125 tail x <- x
126 \end{verbatim}
127 }
128
129 Copatterns are also practically expressive, as in this concise
130 and readable definition of the fibonacci numbers in terms of
131 the \dualtt{merge} expression:
132
133 {\color{NavyBlue}
134 \begin{verbatim}
135 codata Stream a
136 = head a
137 & tail (Stream a)
138
139 zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c
140 zipWith f s1 s2 = merge x from
141 head x <- f (head s1) (head s2)
142 tail x <- zipWith f (tail s1) (tail s2)
143
144 fibs : Stream Int
145 fibs = merge x from
146 head x <- 0
147 head (tail x) <- 1
148 tail (tail x) <- zipWith (+) x (tail x)
149 \end{verbatim}
150 }
151
152 \section{Generalizing \dual{Co}data}
153
154 \begin{both}
155 A \pos{Generalized Algebraic Data Type} adds extra
156 expressivity to \pos{data} types by allowing extra
157 restrictions on the value being \pos{constructed}.
158 & A \dual{Generalized Coalgebraic Codata Type} adds extra
159 expressivity to \dual{codata} types by allowing extra
160 restrictions on the value being \dual{destructed}.
161 \\
162 \color{BrickRed}
163 \begin{verbatim}
164 data Join a where
165 Unit : Int -> Join Int
166 Join : (Join a, Join a) ->
167 Join (a, a)\end{verbatim}
168 &
169 \color{NavyBlue}
170 \begin{verbatim}
171 codata Split a where
172 unit : Split Int -> Int
173 split : Split (a, a) ->
174 (Split a, Split a)\end{verbatim}
175 \\
176 This definition precludes the use of any value of the
177 type \pos{Join(Int, Bool)} because there is no way
178 to \pos{construct} a value of this type---we can only
179 \pos{construct} values with pairs of the same type,
180 or containing an \texttt{Int}.
181 &
182 This definition precludes the use of any value of the
183 type \dual{Split(Int, Bool)} because there is no way
184 to \dual{destruct} a value of this type---we can only
185 \dual{destruct} values with pairs of the same type,
186 or containing an \texttt{Int}.
187 \\
188 This gives us extra type information to omit nonsensical
189 branches in \postt{case}, as well. The following code
190 matches over a value of type \postt{Join Int}, and as
191 such only has an arm for the \pos{constructor}
192 \postt{Unit}---because it is the only \pos{constructor}
193 which can \pos{create} a value of that type!
194 &
195 This gives us extra type information to omit nonsensical
196 branches in \dualtt{merge}, as well. The following code
197 matches over a value of type \dualtt{Split Int}, and as
198 such only has an arm for the \dual{destructor}
199 \dualtt{unit}---because it is the only \dual{destructor}
200 which can \dual{destruct} a value of that type!
201 \\
202 \color{BrickRed}
203 \begin{verbatim}
204 f : Join Int -> Int
205 f x = case x of
206 Unit n -> n\end{verbatim}
207 &
208 \color{NavyBlue}
209 \begin{verbatim}
210 g : Int -> Split Int
211 g n = merge x from
212 unit x <- n\end{verbatim}
213 \\
214 We can \pos{construct} a value of type \postt{Join Int}
215 in conjunction with using \postt{f} like so:
216 & We can \dual{destruct} a value of type \dualtt{Split Int}
217 in conjunction with using \dualtt{g} like so:
218 \\
219 \color{BrickRed}
220 \begin{verbatim}
221 let y : Join Int
222 y = Unit 5
223 in
224 f y\end{verbatim}
225 &
226 \color{NavyBlue}
227 \begin{verbatim}
228 let y : Split Int
229 y = g 5
230 in
231 unit y\end{verbatim}
232 \\
233 \end{both}
234
235 \section{Focus on GCCTs}
236
237 To dispense with the dual presentation: a simple, high-level, handwavey
238 description of GCCTs is that they are \textit{records whose available
239 projections may be restricted by
240 the type of the record}. Like GADTs, they can introduce and use extra
241 typing information. For example, consider the following GCCT and its
242 instantiations:
243
244 {\color{NavyBlue}
245 \begin{verbatim}
246 codata Wrapper a where
247 contents : Wrapper a -> a
248 isZero : Wrapper Int -> Bool
249
250 mkStringW : String -> Wrapper String
251 mkStringW x = merge r from
252 contents r <- x
253
254 mkIntW : Int -> Wrapper Int
255 mkIntW x = merge r from
256 contents r <- x
257 isZero r <- x == 0
258 \end{verbatim}
259 }
260
261 A \dualtt{Wrapper} value is a wrapper over some other value, which can always be
262 extracted using the projection \dualtt{contents}. However, if the value
263 contained in the ``record'' is an \texttt{Int}, we have a second projection
264 available to us: we can also use \dualtt{isZero} to project out a boolean.
265
266 In fact, because of the type machinery afforded us by GCCTs, we can
267 actually collapse both \dualtt{mkStringW} and \dualtt{mkIntW} into a
268 single function, \dualtt{mkWrapper}, like so:
269
270 {\color{NavyBlue}
271 \begin{verbatim}
272 mkWrapper : a -> Wrapper a
273 mkWrapper x = merge r from
274 contents r <- x
275 isZero r <- x == 0
276 \end{verbatim}
277 }
278
279 The reason this is valid is that, like with GADTs, copattern matching on
280 \dualtt{isZero} gives us extra type information about \dualtt{x}, and so
281 will only be a valid branch when \dualtt{mkWrapper} is called with a
282 value of type \dualtt{Int}; otherwise it is merely a redundant branch
283 and is ignored.
284
285 \subsection{Finite State Automata}
286
287 We can use these in a few interesting ways: for example, consider the situation
288 in which we have a finite state automaton for recognizing a language. For
289 simplicity's sake, we'll restrict the states to \texttt{A}, \texttt{B}, and
290 \texttt{C}, and allow the following valid transitions:
291
292 \begin{verbatim}
293 A -> B,C
294 B -> C
295 C -> A
296 \end{verbatim}
297
298 We want a data structure which represents the transitions available. We can do
299 this, even in a strongly normalizing setting, by representing the FSA using
300 a piece of infinite codata with projections for each state transition:
301
302 {\color{NavyBlue}
303 \begin{verbatim}
304 data State = A | B | C
305 codata NFA (a : State) where
306 aToB : NFA A -> NFA B
307 aToC : NFA A -> NFA C
308 bToC : NFA B -> NFA C
309 cToA : NFA C -> NFA A
310 \end{verbatim}
311 }
312
313 This means that the following expressions (which use \texttt{.} to mean
314 function composition) type-check as they represent valid
315 state transitions
316
317 \begin{verbatim}
318 aState : NFA A
319 aToB aState : NFA B
320 (bToC . aToB) aState : NFA C
321 (cToA . bToC . aToB) aState : NFA A
322 \end{verbatim}
323
324 whereas the following do not
325
326 \begin{verbatim}
327 bToC aState -- cannot unify `NFA A` with `NFA B`
328 (aToC . aToB) aState -- cannot unify `NFA B` with `NFA A`
329 \end{verbatim}
330
331 We can construct an initial \dualtt{aState} value using the following
332 \dualtt{merge} expression, using an extra \texttt{let}-binding to improve
333 the sharing in this structure:
334
335 {\color{NavyBlue}
336 \begin{verbatim}
337 aState : NFA A
338 aState =
339 merge as from
340 let cState = (merge cs from cToA cs <- as) in
341 aToC as <- cState
342 aToB as <- (merge bs from bToC bs <- cState)
343 \end{verbatim}
344 }
345
346 or much more concisely by using nested copatterns:
347
348 {\color{NavyBlue}
349 \begin{verbatim}
350 aState : NFA A
351 aState = merge as from
352 cToA (aToC as) <- as
353 cToA (bToC (aToB as)) <- as
354 \end{verbatim}
355 }
356
357 We can make this more interesting (and more useful) by introducing an extra
358 operation: suppose we're using this to recognize a language equivalent to the
359 regular expression \texttt{/a(b?ca)*/}, and we want to be able to extract
360 the string we've matched, but \textit{only} in the accept state
361 \texttt{A}. We can change the codata definition to have such an accessor:
362
363 {\color{NavyBlue}
364 \begin{verbatim}
365 codata NFA (a : State) where
366 aToB : NFA A -> NFA B
367 aToC : NFA A -> NFA C
368 bToC : NFA B -> NFA C
369 cToA : NFA C -> NFA A
370 matchedString : NFA A -> String
371 \end{verbatim}
372 }
373
374 and change the construction of the NFA to this:
375
376 {\color{NavyBlue}
377 \begin{verbatim}
378 aState : NFA A
379 aState =
380 let f str =
381 merge as from
382 matchedString as <- str
383 cToA (aToC as) <- f (str ++ "ca")
384 cToA (bToC (aToB as)) <- f (str ++ "bca")
385 in f "a"
386 \end{verbatim}
387 }
388
389 Consequently the following holds true:
390
391 \begin{verbatim}
392 (matchedString . cToA . atoC . cToA . bToC . aToB) aState == "abcaca"
393 \end{verbatim}
394
395 whereas the following does not type-check:
396
397 \begin{verbatim}
398 (matchedString . bToC . aToB) aState
399 \end{verbatim}
400
401 \subsection{A Forth-Like Embedded Language}
402
403 Consider the following codata type:
404
405 {\color{NavyBlue}
406 \begin{verbatim}
407 codata Forth a where
408 push : Forth a -> b -> Forth (b, a)
409 get : Forth (a, b) -> a
410 drop : Forth (a, b) -> Forth b
411 swap : Forth (a, (b, c)) -> Forth (b, (a, c))
412 app : Forth (a, (b, c)) -> (a -> b -> d) -> Forth (d, c)
413 \end{verbatim}
414 }
415
416 This corresponds to a small embedded Forth-like sublanguage, in which
417 a value of type \dualtt{Forth} corresponds to the state of a stack whose
418 type is given by the type parameter. This means that not only is it an
419 embedded Forth-like language, it is a well-typed language that can take
420 arbitrary values in the host language and manipulate them on the stack.
421 Assuming the use of the operator \texttt{x \# f = f x}, we can write a
422 well-typed subprogram
423
424 {\color{NavyBlue}
425 \begin{verbatim}
426 initialState # push 5
427 # push 2
428 # push 3
429 # swap
430 # drop
431 # add
432 # get
433 \end{verbatim}
434 }
435
436 and also reject this ill-typed subprogram, where \texttt{add} requires
437 two integers but is given a stack with a boolean on top
438
439 {\color{NavyBlue}
440 \begin{verbatim}
441 initialState # push 5 # push true # add # get
442 \end{verbatim}
443 }
444
445 but also this one, in which \texttt{add} is only given a single argument
446
447 {\color{NavyBlue}
448 \begin{verbatim}
449 initialState # push 5 # add # get
450 \end{verbatim}
451 }
452
453 We have to create a helper function in order to create a value of this
454 type, which is the helper function \dualtt{push'}:
455
456 {\color{NavyBlue}
457 \begin{verbatim}
458 doPush : Forth a -> b -> Forth (b, a)
459 doPush s x = merge s' from
460 push s' <- doPush s'
461 get s' <- x
462 drop s' <- s
463 swap s' <- push (get s) (push x (drop s))
464 app s' <-
465 let doApp f = push (f x (get s)) (drop s)
466 in doApp
467 \end{verbatim}
468 }
469
470 And then we can create an actual value of type \dualtt{Forth ()}:
471
472 {\color{NavyBlue}
473 \begin{verbatim}
474 initialState : Forth ()
475 initialState = merge s'
476 push s' <- doPush s'
477 \end{verbatim}
478 }
479
480 \end{document}
+7
-0
overview/Makefile less more
1 all: gcct.pdf
2
3 gcct.pdf: gcct.tex
4 pdflatex gcct.tex
5
6 clean:
7 rm -rf gcct.aux gcct.log gcct.pdf
+581
-0
overview/gcct.tex less more
1 \documentclass{scrartcl}
2 \usepackage[letterpaper]{geometry}
3 \usepackage{fullpage}
4 \usepackage{cmbright}
5 \usepackage[usenames,dvipsnames]{color}
6 % \newcommand{\both}[2]{\begin{tabular}{ p{4in} p{4in} } #1 && #2 \\ \end{tabular}}
7 \newcommand{\pos}[1]{\textcolor{BrickRed}{#1}}
8 \newcommand{\postt}[1]{\textcolor{BrickRed}{\texttt{#1}}}
9 \newcommand{\dual}[1]{\textcolor{NavyBlue}{#1}}
10 \newcommand{\dualtt}[1]{\textcolor{NavyBlue}{\texttt{#1}}}
11 \newenvironment{both}
12 { \begin{tabular}{ p{3in} p{3in} } }
13 { \\ \end{tabular} }
14 \begin{document}
15 \section{\pos{Data} and \dual{Codata}}
16
17 \begin{both}
18 \pos{Data} is defined by its \pos{introduction} rules.
19 & \dual{Codata} is defined by its \dual{elimination} rules.
20 \\
21 We can define a \pos{data} type with
22 & We can define a \dual{codata} type with
23 \\
24 \color{BrickRed}
25 \begin{verbatim}
26 data Either a b
27 = Left a
28 | Right b\end{verbatim}
29 &
30 \color{NavyBlue}
31 \begin{verbatim}
32 codata Both a b
33 = first a
34 & second b\end{verbatim}
35 \\
36 This definition introduces two functions:
37 & This definition introduces two functions:
38 \\
39 \color{BrickRed}
40 \begin{verbatim}
41 Left : a -> Either a b
42 Right : b -> Either a b\end{verbatim}
43 &
44 \color{NavyBlue}
45 \begin{verbatim}
46 first : Both a b -> a
47 second : Both a b -> b\end{verbatim}
48 \\
49 In order to \pos{destruct data} we have to use
50 \pos{patterns} which let you match on \pos{constructors}.
51 & In order to \dual{construct codata} we have to use
52 \dual{copatterns} which let you match on \dual{destructors}.
53 \\
54 \color{BrickRed}
55 \begin{verbatim}
56 (case e : Either a b of
57 Left (x : a) -> (e1 : c)
58 Right (y : b) -> (e2 : c)) : c\end{verbatim}
59 &
60 \color{NavyBlue}
61 \begin{verbatim}
62 (merge x : Both a b from
63 first x <- e1 : a
64 second x <- e2 : b) : Both a b\end{verbatim}
65 \\
66 Here, \postt{e} represents the \pos{value being
67 destructed}, and each branch represents a \pos{constructor
68 with which it might have been constructed}. We are effectively
69 \pos{dispatching on possible pasts} of
70 \postt{e}.
71 & Here, \dual{\texttt{x}} represents the \dual{value being
72 constructed}, and each branch represents a \dual{destructor
73 with which it might eventually be destructed}. We are effectively
74 \dual{dispatching on possible futures} of
75 \dualtt{x}.
76 \\
77 \end{both}
78
79 \section{Codata, Records, and Copatterns}
80 \raggedright
81
82 In the same way that named sums are a natural way to represent data,
83 records are a natural way to represent codata. In lieu of the above
84 syntax, one often sees codata represented as something more like
85
86 {\color{NavyBlue}
87 \begin{verbatim}
88 record Both a b = { .first : a, .second : b }
89
90 x : Both Int Bool
91 x = { .first = 2, .second = true }
92
93 x.first == 2, x.second == true
94 \end{verbatim}
95 }
96
97 The \dualtt{merge} syntax is used here for conceptual
98 symmetry with \postt{case}. Additionally, the use of
99 copatterns is nicely dual with the extra expressivity that
100 patterns offer. For example, we can use nested patterns with
101 constructors of various types, as in this function which
102 processes a list of \postt{Either Int Bool} values
103 by summing the integers in the list until it reaches a
104 \postt{false} value or the end of the list:
105
106 {\color{BrickRed}
107 \begin{verbatim}
108 f : List (Either Int Bool) -> Int
109 f lst = case lst of
110 Cons (Left i) xs -> i + f xs
111 Cons (Right b) xs -> if b then f xs else 0
112 Nil -> 0
113 \end{verbatim}
114 }
115
116 Similarly, we can define an infinite stream of pairs using
117 nested copatterns as so:
118
119 {\color{NavyBlue}
120 \begin{verbatim}
121 s : Int -> Stream (Both Int Bool)
122 s n = merge x from
123 first (head x) <- n
124 second (head x) <- n > 0
125 tail x <- x
126 \end{verbatim}
127 }
128
129 Copatterns are also practically expressive, as in this concise
130 and readable definition of the fibonacci numbers in terms of
131 the \dualtt{merge} expression:
132
133 {\color{NavyBlue}
134 \begin{verbatim}
135 codata Stream a
136 = head a
137 & tail (Stream a)
138
139 zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c
140 zipWith f s1 s2 = merge x from
141 head x <- f (head s1) (head s2)
142 tail x <- zipWith f (tail s1) (tail s2)
143
144 fibs : Stream Int
145 fibs = merge x from
146 head x <- 0
147 head (tail x) <- 1
148 tail (tail x) <- zipWith (+) x (tail x)
149 \end{verbatim}
150 }
151
152 \section{Generalizing \dual{Co}data}
153
154 \begin{both}
155 A \pos{Generalized Algebraic Data Type} adds extra
156 expressivity to \pos{data} types by allowing extra
157 restrictions on the value being \pos{constructed}.
158 & A \dual{Generalized Coalgebraic Codata Type} adds extra
159 expressivity to \dual{codata} types by allowing extra
160 restrictions on the value being \dual{destructed}.
161 \\
162 \color{BrickRed}
163 \begin{verbatim}
164 data Join a where
165 Unit : Int -> Join Int
166 Join : (Join a, Join a) ->
167 Join (a, a)\end{verbatim}
168 &
169 \color{NavyBlue}
170 \begin{verbatim}
171 codata Split a where
172 unit : Split Int -> Int
173 split : Split (a, a) ->
174 (Split a, Split a)\end{verbatim}
175 \\
176 This definition precludes the use of any value of the
177 type \pos{Join(Int, Bool)} because there is no way
178 to \pos{construct} a value of this type---we can only
179 \pos{construct} values with pairs of the same type,
180 or containing an \texttt{Int}.
181 &
182 This definition precludes the use of any value of the
183 type \dual{Split(Int, Bool)} because there is no way
184 to \dual{destruct} a value of this type---we can only
185 \dual{destruct} values with pairs of the same type,
186 or containing an \texttt{Int}.
187 \\
188 This gives us extra type information to omit nonsensical
189 branches in \postt{case}, as well. The following code
190 matches over a value of type \postt{Join Int}, and as
191 such only has an arm for the \pos{constructor}
192 \postt{Unit}---because it is the only \pos{constructor}
193 which can \pos{create} a value of that type!
194 &
195 This gives us extra type information to omit nonsensical
196 branches in \dualtt{merge}, as well. The following code
197 matches over a value of type \dualtt{Split Int}, and as
198 such only has an arm for the \dual{destructor}
199 \dualtt{unit}---because it is the only \dual{destructor}
200 which can \dual{destruct} a value of that type!
201 \\
202 \color{BrickRed}
203 \begin{verbatim}
204 f : Join Int -> Int
205 f x = case x of
206 Unit n -> n\end{verbatim}
207 &
208 \color{NavyBlue}
209 \begin{verbatim}
210 g : Int -> Split Int
211 g n = merge x from
212 unit x <- n\end{verbatim}
213 \\
214 We can \pos{construct} a value of type \postt{Join Int}
215 in conjunction with using \postt{f} like so:
216 & We can \dual{destruct} a value of type \dualtt{Split Int}
217 in conjunction with using \dualtt{g} like so:
218 \\
219 \color{BrickRed}
220 \begin{verbatim}
221 let y : Join Int
222 y = Unit 5
223 in
224 f y\end{verbatim}
225 &
226 \color{NavyBlue}
227 \begin{verbatim}
228 let y : Split Int
229 y = g 5
230 in
231 unit y\end{verbatim}
232 \\
233 \end{both}
234
235 \section{Focus on GCCTs}
236
237 To dispense with the dual presentation: a simple, high-level, handwavey
238 description of GCCTs is that they are \textit{records whose available
239 projections may be restricted by
240 the type of the record}. Like GADTs, they can introduce and use extra
241 typing information. For example, consider the following GCCT and its
242 instantiations:
243
244 {\color{NavyBlue}
245 \begin{verbatim}
246 codata Wrapper a where
247 contents : Wrapper a -> a
248 isZero : Wrapper Int -> Bool
249
250 mkStringW : String -> Wrapper String
251 mkStringW x = merge r from
252 contents r <- x
253
254 mkIntW : Int -> Wrapper Int
255 mkIntW x = merge r from
256 contents r <- x
257 isZero r <- x == 0
258 \end{verbatim}
259 }
260
261 A \dualtt{Wrapper} value is a wrapper over some other value, which can always be
262 extracted using the projection \dualtt{contents}. However, if the value
263 contained in the ``record'' is an \texttt{Int}, we have a second projection
264 available to us: we can also use \dualtt{isZero} to project out a boolean.
265
266 In fact, because of the type machinery afforded us by GCCTs, we can
267 actually collapse both \dualtt{mkStringW} and \dualtt{mkIntW} into a
268 single function, \dualtt{mkWrapper}, like so:
269
270 {\color{NavyBlue}
271 \begin{verbatim}
272 mkWrapper : a -> Wrapper a
273 mkWrapper x = merge r from
274 contents r <- x
275 isZero r <- x == 0
276 \end{verbatim}
277 }
278
279 The reason this is valid is that, like with GADTs, copattern matching on
280 \dualtt{isZero} gives us extra type information about \dualtt{x}, and so
281 will only be a valid branch when \dualtt{mkWrapper} is called with a
282 value of type \dualtt{Int}; otherwise it is merely a redundant branch
283 and is ignored.
284
285 \subsection{Finite State Automata}
286
287 We can use these in a few interesting ways: for example, consider the situation
288 in which we have a finite state automaton for recognizing a language. For
289 simplicity's sake, we'll restrict the states to \texttt{A}, \texttt{B}, and
290 \texttt{C}, and allow the following valid transitions:
291
292 \begin{verbatim}
293 A -> B,C
294 B -> C
295 C -> A
296 \end{verbatim}
297
298 We want a data structure which represents the transitions available. We can do
299 this, even in a strongly normalizing setting, by representing the FSA using
300 a piece of infinite codata with projections for each state transition:
301
302 {\color{NavyBlue}
303 \begin{verbatim}
304 data State = A | B | C
305 codata NFA (a : State) where
306 aToB : NFA A -> NFA B
307 aToC : NFA A -> NFA C
308 bToC : NFA B -> NFA C
309 cToA : NFA C -> NFA A
310 \end{verbatim}
311 }
312
313 This means that the following expressions (which use \texttt{.} to mean
314 function composition) type-check as they represent valid
315 state transitions
316
317 \begin{verbatim}
318 aState : NFA A
319 aToB aState : NFA B
320 (bToC . aToB) aState : NFA C
321 (cToA . bToC . aToB) aState : NFA A
322 \end{verbatim}
323
324 whereas the following do not
325
326 \begin{verbatim}
327 bToC aState -- cannot unify `NFA A` with `NFA B`
328 (aToC . aToB) aState -- cannot unify `NFA B` with `NFA A`
329 \end{verbatim}
330
331 We can construct an initial \dualtt{aState} value using the following
332 \dualtt{merge} expression, using an extra \texttt{let}-binding to improve
333 the sharing in this structure:
334
335 {\color{NavyBlue}
336 \begin{verbatim}
337 aState : NFA A
338 aState =
339 merge as from
340 let cState = (merge cs from cToA cs <- as) in
341 aToC as <- cState
342 aToB as <- (merge bs from bToC bs <- cState)
343 \end{verbatim}
344 }
345
346 or much more concisely by using nested copatterns:
347
348 {\color{NavyBlue}
349 \begin{verbatim}
350 aState : NFA A
351 aState = merge as from
352 cToA (aToC as) <- as
353 cToA (bToC (aToB as)) <- as
354 \end{verbatim}
355 }
356
357 We can make this more interesting (and more useful) by introducing an extra
358 operation: suppose we're using this to recognize a language equivalent to the
359 regular expression \texttt{/a(b?ca)*/}, and we want to be able to extract
360 the string we've matched, but \textit{only} in the accept state
361 \texttt{A}. We can change the codata definition to have such an accessor:
362
363 {\color{NavyBlue}
364 \begin{verbatim}
365 codata NFA (a : State) where
366 aToB : NFA A -> NFA B
367 aToC : NFA A -> NFA C
368 bToC : NFA B -> NFA C
369 cToA : NFA C -> NFA A
370 matchedString : NFA A -> String
371 \end{verbatim}
372 }
373
374 and change the construction of the NFA to this:
375
376 {\color{NavyBlue}
377 \begin{verbatim}
378 aState : NFA A
379 aState =
380 let f str =
381 merge
382 matchedString _ <- str
383 cToA (aToC _) <- f (str ++ "ca")
384 cToA (bToC (aToB _)) <- f (str ++ "bca")
385 in f "a"
386 \end{verbatim}
387 }
388
389 Consequently the following holds true:
390
391 \begin{verbatim}
392 (matchedString . cToA . atoC . cToA . bToC . aToB) aState == "abcaca"
393 \end{verbatim}
394
395 whereas the following does not type-check:
396
397 \begin{verbatim}
398 (matchedString . bToC . aToB) aState
399 \end{verbatim}
400
401 \subsection{A Forth-Like Embedded Language}
402
403 Consider the following codata type:
404
405 {\color{NavyBlue}
406 \begin{verbatim}
407 codata Forth a where
408 push : Forth a -> b -> Forth (b, a)
409 get : Forth (a, b) -> a
410 drop : Forth (a, b) -> Forth b
411 swap : Forth (a, (b, c)) -> Forth (b, (a, c))
412 app : Forth (a, (b, c)) -> (a -> b -> d) -> Forth (d, c)
413 \end{verbatim}
414 }
415
416 This corresponds to a small embedded Forth-like sublanguage, in which
417 a value of type \dualtt{Forth} corresponds to the state of a stack whose
418 type is given by the type parameter. This means that not only is it an
419 embedded Forth-like language, it is a well-typed language that can take
420 arbitrary values in the host language and manipulate them on the stack.
421 Assuming the use of the operator \texttt{x \# f = f x}, we can write a
422 well-typed subprogram
423
424 {\color{NavyBlue}
425 \begin{verbatim}
426 initialState # push 5
427 # push 2
428 # push 3
429 # swap
430 # drop
431 # add
432 # get
433 \end{verbatim}
434 }
435
436 and also reject this ill-typed subprogram, where \texttt{add} requires
437 two integers but is given a stack with a boolean on top
438
439 {\color{NavyBlue}
440 \begin{verbatim}
441 initialState # push 5 # push true # add # get
442 \end{verbatim}
443 }
444
445 but also this one, in which \texttt{add} is only given a single argument
446
447 {\color{NavyBlue}
448 \begin{verbatim}
449 initialState # push 5 # add # get
450 \end{verbatim}
451 }
452
453 We have to create a helper function in order to create a value of this
454 type, which is the helper function \dualtt{push'}:
455
456 {\color{NavyBlue}
457 \begin{verbatim}
458 doPush : Forth a -> b -> Forth (b, a)
459 doPush s x = merge s' from
460 push s' <- doPush s'
461 get s' <- x
462 drop s' <- s
463 swap s' <- push (get s) (push x (drop s))
464 app s' <-
465 let doApp f = push (f x (get s)) (drop s)
466 in doApp
467 \end{verbatim}
468 }
469
470 And then we can create an actual value of type \dualtt{Forth ()}:
471
472 {\color{NavyBlue}
473 \begin{verbatim}
474 initialState : Forth ()
475 initialState = merge s'
476 push s' <- doPush s'
477 \end{verbatim}
478 }
479
480 \subsection{The Co\"operational Comonad}
481
482 Two convenient minimal definitions of a \texttt{Monad} are in terms
483 of \texttt{return} and either \texttt{join} and \texttt{fmap} or
484 \texttt{bind}:
485
486 \begin{verbatim}
487 class Monad m where
488 return : a -> m a
489 join : m (m a) -> m a
490 map : (a -> b) -> m a -> m b
491
492 bind : Monad m => (a -> m b) -> m a -> m b
493 bind f x = join (map f x)
494 \end{verbatim}
495
496 \begin{verbatim}
497 class Monad m where
498 return : a -> m a
499 bind : (a -> m b) -> m a -> m b
500
501 join : Monad m => m (m a) -> m a
502 join = map return
503
504 map : (a -> b) -> m a -> m b
505 map f x = bind (return . f) x
506 \end{verbatim}
507
508 This implies two ways of constructing a data structure that is
509 trivially a monad. The first is the traditional construction of
510 a free monad, which has two constructors which correspond to
511 \texttt{return} and \texttt{Join}:
512
513 \begin{verbatim}
514 data Free : (* -> *) -> * -> *
515 = Pure a
516 | Join (f (Free f a))
517 \end{verbatim}
518
519 In order to be a \texttt{Monad}, then the first parameter given
520 to \texttt{Free} must be a \texttt{Functor}, so that we get the
521 ability to \texttt{map} as well:
522
523 \begin{verbatim}
524 instance Functor f => Monad (Free f) where
525 return = Pure
526
527 map f (Pure x) = Pure (f x)
528 map f (Join xs) = Join (fmap f xs)
529
530 join (Pure x) = x
531 join (Join xs) = Join (fmap join xs)
532 \end{verbatim}
533
534 However, we could also write a data structure which is trivially
535 a monad whose type corresponds to \texttt{return} and \texttt{bind},
536 in which case we needn't have a functor constraint on the type
537 parameter. For this, we need GADTs:
538
539 \begin{verbatim}
540 data Oper : (* -> *) -> * -> * where
541 Return : a -> Oper f a
542 Bind : f a -> (a -> Oper f b) -> Oper f b
543
544 instance Monad (Oper f) where
545 return = Return
546
547 bind g (Return x) = g x
548 bind g (Bind x f) = Bind x (f >=> g)
549 \end{verbatim}
550
551 We can use the operational monad to combine various instructions
552 together: for example, we can construct a stack-like language
553 with the following instructions:
554
555 \begin{verbatim}
556 data StackInstr a where
557 Pop : StackInstr Int
558 Push : Int -> StackInstr ()
559
560 evaluate : Oper StackInstr a -> List Int -> a
561 evaluate (Return x) _ = x
562 evaluate (Bind Pop f) (s:ss) = evaluate (f s) ss
563 evaluate (Bind (Push s) f) ss = evaluate (f ()) (s:ss)
564
565 push : Oper StackInstr ()
566 push = return . Push
567
568 pop : Oper StackInstr Int
569 pop = return Pop
570
571 add : Oper StackInstr ()
572 add = bind pop (\ x ->
573 bind pop (\ y ->
574 push (x + y)))
575
576 sampleProgram : Int
577 sampleProgram = evalute program []
578 where program =
579 \end{verbatim}
580
581 \end{document}
+8
-0
presentation/Makefile less more
1 all: presentation.pdf
2
3 presentation.pdf: presentation.tex
4 pdflatex presentation.tex
5
6 clean:
7 rm -rf presentation.aux presentation.log presentation.pdf presentation.nav \
8 presentation.out presentation.snm presentation.toc presentation.vrb
+302
-0
presentation/presentation.tex less more
1 \documentclass{beamer}
2 \usepackage{cmbright}
3 % \usepackage[usenames,dvipsnames]{color}
4 \usepackage{listings}
5 \usepackage{xcolor}
6 \newcommand{\pos}[1]{\textcolor{red}{#1}}
7 \newcommand{\postt}[1]{\textcolor{red}{\texttt{#1}}}
8 \newcommand{\dual}[1]{\textcolor{blue}{#1}}
9 \newcommand{\dualtt}[1]{\textcolor{blue}{\texttt{#1}}}
10
11 \lstset{ keywordstyle={\bfseries}
12 , keywordstyle=[2]\color{red}\bfseries
13 , keywordstyle=[3]\color{blue}\bfseries
14 , basicstyle=\scriptsize\ttfamily,
15 , morekeywords={where,let,in,instance,type},
16 , morekeywords=[2]{data,case,of}
17 , morekeywords=[3]{codata,merge}
18 }
19
20 \newenvironment{both}
21 { \begin{tabular}{ p{2in} p{2in} } }
22 { \\ \end{tabular} }
23 \renewcommand{\ttdefault}{pcr}
24
25 \title{Generalized Coalgebraic Codata Types}
26 \subtitle{Excessive Amounts of Duality}
27 \author{G.~Ritter \and K.~Foner}
28 \date{\today}
29 \subject{Computer Science}
30
31 \begin{document}
32
33 \frame{\titlepage}
34
35 \begin{frame}[fragile]
36 \frametitle{Data and Codata: An Introduction}
37 \begin{both}
38 \begin{lstlisting}
39 -------------------
40 -- Defining data --
41
42 data Either a b
43 = Left a
44 | Right b
45
46 -----------------------
47 -- Constructing data --
48
49 Left : a -> Either a b
50 Right : b -> Either a b
51
52 ----------------------
53 -- Destructing data --
54
55 f : Either Int Bool -> Bool
56 f x = case x of
57 Left i -> i == 0
58 Right b -> b
59 \end{lstlisting}
60 &
61 \begin{lstlisting}
62 ---------------------
63 -- Defining codata --
64
65 codata Both a b
66 = First a
67 & Second b
68
69 ------------------------
70 -- Destructing codata --
71
72 First : Both a b -> a
73 Second : Both a b -> b
74
75 -------------------------
76 -- Constructing codata --
77
78 g : Int -> Both Int Bool
79 g x = merge
80 First p <- x
81 Second p <- x == 0
82 \end{lstlisting}
83 \\
84 \end{both}
85 \end{frame}
86
87 \begin{frame}[fragile]
88 \frametitle{Copatterns}
89 \begin{lstlisting}[basicstyle=\normalsize\ttfamily]
90 codata Stream a = Head a & Tail (Stream a)
91
92 zipWith : (a -> b -> c) -> Stream a ->
93 Stream b -> Stream c
94 Head (zipWith f s1 s2) =
95 f (Head s1) (Head s2)
96 Tail (zipWith f s1 s2) =
97 zipWith f (Tail s1) (Tail s2)
98
99 fibs : Stream Int
100 Head fibs = 0
101 Head (Tail fibs) = 1
102 Tail (fibsTail@(Tail fibs)) =
103 zipWith (+) fibs fibsTail
104 \end{lstlisting}
105 \end{frame}
106
107 \begin{frame}[fragile]
108 \frametitle{Copatterns}
109 \begin{lstlisting}[basicstyle=\normalsize\ttfamily]
110 codata Stream a = Head a & Tail (Stream a)
111
112 zipWith : (a -> b -> c) -> Stream a ->
113 Stream b -> Stream c
114 Head (zipWith f s1 s2) =
115 f (Head s1) (Head s2)
116 Tail (zipWith f s1 s2) =
117 zipWith f (Tail s1) (Tail s2)
118
119 merge
120 Head _ = 0
121 Head (Tail _) = 1
122 Tail (fibsTail@(Tail fibs)) =
123 zipWith (+) fibs fibsTail
124 \end{lstlisting}
125 \end{frame}
126
127 \begin{frame}[fragile]
128 \frametitle{Generalizing Types}
129 \begin{both}
130 \begin{lstlisting}
131 data T: * -> * where
132 U : Int -> T Int
133 X : (T a,T a) -> T (a,a)
134
135 --
136
137 U : Int -> T Int
138 X : (T a,T a) -> T (a,a)
139
140 --
141
142 sum : T a -> Int
143 sum x = case x of
144 U i -> i
145 X (a, b) -> sum a + sum b
146 \end{lstlisting}
147 &
148 \begin{lstlisting}
149 codata T': * -> * where
150 U' : T' Int -> Int
151 X' : T' (a,a) -> (T' a,T' a)
152
153 --
154
155 U' : T' Int -> Int
156 X' : T' (a,a) -> (T' a,T' a)
157
158 --
159
160 split : Int -> T' a
161 split i = merge
162 U' _ <- i
163 X' _ <- ( split 1
164 , split (i-1)
165 )
166 \end{lstlisting}
167 \end{both}
168 \end{frame}
169
170 \begin{frame}[fragile]
171 \frametitle{GCCTs}
172 \begin{lstlisting}[basicstyle=\normalsize\ttfamily]
173 codata Wrapper: * -> * where
174 G : Wrapper a -> a
175 Z : Wrapper Int -> Bool
176
177 mkBoolWrapper : Bool -> Wrapper Bool
178 G (mkBoolWrapper b) = b
179
180 mkIntWrapper : Int -> Wrapper Int
181 G (mkIntWrapper i) = i
182 Z (mkIntWrapper i) = i == 0
183
184 mkWrapper : a -> Wrapper a
185 G (mkWrapper x) = x
186 Z (mkWrapper x) = x == 0
187 \end{lstlisting}
188 \end{frame}
189
190 \begin{frame}[fragile]
191 \frametitle{NFA}
192 \begin{lstlisting}[basicstyle=\normalsize\ttfamily]
193 data S = A | B | C
194
195 codata FSA: S -> * where
196 aToB : FSA A -> FSA B
197 bToC : FSA B -> FSA C
198 aToC : FSA A -> FSA C
199 cToA : FSA C -> FSA A
200
201 aState : FSA A
202 aState = merge
203 cToA (aToC a) <- a
204 cToA (bToC (aToB a)) <- a
205
206 cToA . bToC . aToB == id
207 cToA . aToB -- fails to type-check
208 \end{lstlisting}
209 \end{frame}
210
211 \begin{frame}[fragile]
212 \frametitle{NFA}
213 \begin{lstlisting}[basicstyle=\normalsize\ttfamily]
214 codata FSA: S -> * where
215 aToB : FSA A -> FSA B
216 bToC : FSA B -> FSA C
217 aToC : FSA A -> FSA C
218 cToA : FSA C -> FSA A
219 matchedString : FSA A -> String
220
221 aState : FSA A
222 aState =
223 let f str = merge
224 cToA (aToC _) <- f (str ++ "ca")
225 cToA (bToC (aToB _)) <- f (str ++ "bca")
226 matchedString _ <- str
227 in f "a"
228 \end{lstlisting}
229 \end{frame}
230
231 \begin{frame}[fragile]
232 \frametitle{NFA}
233 \begin{lstlisting}[basicstyle=\normalsize\ttfamily]
234 codata FSA: S -> * where
235 aToB : FSA A -> FSA B
236 bToC : FSA B -> FSA C
237 aToC : FSA A -> FSA C
238 cToA : FSA C -> FSA A
239 matchedString : FSA _ -> String
240
241 aState : FSA A
242 aState =
243 let f str = merge
244 cToA (aToC _) <- f (str ++ "ca")
245 cToA (bToC (aToB _)) <- f (str ++ "bca")
246 matchedString _ <- str
247 matchedString (aToB _) <- str ++ "b"
248 matchedString (aToC _) <- str ++ "c"
249 matchedString (bToC (aToB _)) <- str ++ "bc"
250 in f "a"
251 \end{lstlisting}
252 \end{frame}
253
254 \begin{frame}[fragile]
255 \frametitle{Operational}
256 \begin{lstlisting}[basicstyle=\normalsize\ttfamily]
257 data Oper : (* -> *) -> * -> * where
258 Return : a -> Oper t a
259 Bind : t a -> (a -> Oper t b) -> Oper t b
260
261 instance Monad (Oper t) where
262 return = Return
263 Return x >>= g = g x
264 Bind x f >>= g = Bind x (f >=> g)
265 \end{lstlisting}
266 \end{frame}
267
268 \begin{frame}[fragile]
269 \frametitle{Co-operational}
270 \begin{lstlisting}[basicstyle=\normalsize\ttfamily]
271 codata Coop : (* -> *) -> * -> * where
272 Extract : Coop t a -> a
273 Extend : Coop t a -> (Coop t a -> b) -> t b
274
275 instance Comonad (Coop t) where
276 extract = Extract
277 Extract (x <<= f) = f x
278 Extend (x <<= f) g =
279 Extend x (f =>= g)
280 \end{lstlisting}
281 \end{frame}
282
283 \begin{frame}[fragile]
284 \frametitle{Co-operational}
285 \begin{lstlisting}[basicstyle=\normalsize\ttfamily]
286 codata Op : * -> * where
287 Pop : Op (a, b) -> a
288 Drop : Op (a, b) -> Op b
289
290 type Stack a = Coop Op a
291
292 push : a -> Stack b -> Stack (a, b)
293 push x s = s <<= go
294 where go y = (x, extract y)
295
296 dup : Stack (a, b) -> Stack (a, (a, b))
297 dup s = s <<= go
298 where go y = (fst (extract y), extract y)
299 \end{lstlisting}
300 \end{frame}
301
302 \end{document}