6 results back to index

**
Masterminds of Programming: Conversations With the Creators of Major Programming Languages
** by
Federico Biancuzzi,
Shane Warden

Amazon: amazon.com — amazon.co.uk — amazon.de — amazon.fr

Benevolent Dictator For Life (BDFL), business intelligence, business process, cellular automata, cloud computing, commoditize, complexity theory, conceptual framework, continuous integration, data acquisition, domain-specific language, Douglas Hofstadter, Fellow of the Royal Society, finite state, Firefox, follow your passion, Frank Gehry, general-purpose programming language, Guido van Rossum, HyperCard, information retrieval, iterative process, John von Neumann, Larry Wall, linear programming, loose coupling, Mars Rover, millennium bug, NP-complete, Paul Graham, performance metric, Perl 6, QWERTY keyboard, RAND corporation, randomized controlled trial, Renaissance Technologies, Ruby on Rails, Sapir-Whorf hypothesis, Silicon Valley, slashdot, software as a service, software patent, sorting algorithm, Steve Jobs, traveling salesman, Turing complete, type inference, Valgrind, Von Neumann architecture, web application

When we first announced the Perl 6 effort, we got those 361 RFCs, and most of them assumed an incremental change from Perl 5 without any other changes. In a sense, the Perl 6 design is simply the result of summing up, simplifying, unifying, and rationalizing those incremental suggestions, but the actual leap from Perl 5 to Perl 6 will certainly feel revolutionary to anyone who did not participate in the design process. Yet most Perl 6 programs will look quite similar to what you’d write in Perl 5, because the underlying thought process will be similar. At the same time, Perl 6 will also make it much easier to branch out into the functional or OO modes of thought, if that’s how you think.

…

That’s why the Web was largely prototyped in Perl—because HTML is text, and people wanted to write HTML that glued in data from various sources including databases. The extensions to do that were already there, or were easy to write. But Perl is also Perl 6, where we’re trying to fix everything that’s wrong with Perl 5 without breaking anything that’s right with Perl 5. We recognize that this is impossible, but we’re going to do it anyway. We’re completely redesigning the language while keeping the same underlying design principles. Even in its current, partially implemented form, Perl 6 is already a spectacularly cool language in many people’s opinion, and when it’s done it will, hopefully, be both self-describing and self-parsing using highly derivable grammars, and thus optimized to evolve smoothly into any kind of a language we might want 20 years from now.

…

What are the minimal changes that we can make to how it actually works underneath that will actually do what they expect rather than what they don’t expect?” That process to the nth degree is, as you know, the Perl 6 design process. We’ve been in that mindset for the past few years. Can you give an example? Larry: In Perl 5, $var is a scalar, @var is an array, and %var is an associative array. New users often generalize that to think that @var[$index] and %foo{$key} are how you write the indexed forms, but for historical reasons that’s not how Perl 5 does it. The documents go through contortions to explain why things aren’t the way people expect. In Perl 6, we decided it would be better to fix the language than fix the user. In Perl 5, various functions default to an argument of $_ (the current topic) if no argument is supplied, and you basically have to memorize the list of functions that do so.

**
Higher-Order Perl: A Guide to Program Transformation
** by
Mark Jason Dominus

Amazon: amazon.com — amazon.co.uk — amazon.de — amazon.fr

always be closing, Defenestration of Prague, Donald Knuth, Isaac Newton, Larry Wall, P = NP, Paul Graham, Perl 6, slashdot, SpamAssassin

If the input stream is exhausted, digest_maillog() terminates the output: sub digest_maillog { my ($s, $msg, $del) = @_; for ($msg, $del) { $_ = {} unless $_ } while ($s) { my ($date, $rec) = @{drop($s)}; next unless defined $date; if ($rec =˜ /ˆnew msg (\d+)/) { $msg->{$1} = { start => $date, id => $1, success => 0, failure => 0, deferral => 0 }; } elsif ($rec =˜ /ˆinfo msg (\d+): bytes (\d+) from (<[ˆ\>]*>)/) { next unless exists $msg->{$1}; $msg->{$1}{bytes} = $2; $msg->{$1}{from} = $3; } elsif ($rec =˜ /ˆstarting delivery (\d+): msg (\d+)/) { next unless exists $msg->{$2}; $del->{$1} = $2; push @{$msg->{$2}{deliveries}}, $1; } elsif ($rec =˜ /ˆdelivery (\d+):(success|failure|deferral)/) { next unless exists $del->{$1} && exists $msg->{$del->{$1}}; $msg->{$del->{$1}}{$2}++; } elsif ($rec =˜ /ˆend msg (\d+)/) { next unless exists $msg->{$1}; my $m = delete $msg->{$1}; $m->{total_deliveries} = @{$m->{deliveries}}; for (@{$m->{deliveries}}) { delete $del->{$_} }; $m->{end} = $date; return node($m, promise { digest_maillog($s, $msg, $del) }); } } return; } Now we can generate reports by transforming the stream of message structures into a stream of log records: use POSIX 'strftime'; sub format_digest { my $h = shift; join " ", $h->{id}, strftime("%d/%b/%Y:%T", localtime($h->{start})), strftime("%d/%b/%Y:%T", localtime($h->{end})), $h->{from}, $h->{total_deliveries}, $h->{success}, $h->{failure}, $h->{deferral}, ; } show(&transform(\&format_digest, digest_maillog($mail_log))); Typical output looks like this: ... 707045 28/Jan/2003:12:10:03 28/Jan/2003:12:10:03 <Paulmc@371.net> 1 1 0 0 707292 28/Jan/2003:12:10:03 28/Jan/2003:12:10:06 <Paulmc@371.net> 1 1 0 0 707046 28/Jan/2003:12:10:06 28/Jan/2003:12:10:07 <Paulmc@371.net> 4 3 1 0 707293 28/Jan/2003:12:10:07 28/Jan/2003:12:10:07 <guido@odiug.zope.com> 1 1 0 0 707670 28/Jan/2003:12:10:06 28/Jan/2003:12:10:08 <spam-return-133409-@plover.com-@[]> 2 2 0 0 707045 28/Jan/2003:12:10:07 28/Jan/2003:12:10:11 <guido@odiug.zope.com> 1 1 0 0 707294 28/Jan/2003:12:10:11 28/Jan/2003:12:10:11 <guido@odiug.zope.com> 1 1 0 0 707047 28/Jan/2003:12:10:22 28/Jan/2003:12:10:23 <ezmlm-return-10817-mjd-ezmlm=plover.com@list.cr.yp.to> 1 1 0 0 707048 28/Jan/2003:12:11:02 28/Jan/2003:12:11:02 <perl5-porters-return-71265-mjd-p5p2=plover.com@perl.org> 1 1 0 0 707503 24/Jan/2003:11:29:49 28/Jan/2003:12:11:35 <perl-qotw-discuss-return-1200-@plover.com-@[]> 388 322 2 64 707049 28/Jan/2003:12:11:35 28/Jan/2003:12:11:45 <> 1 1 0 0 707295 28/Jan/2003:12:11:41 28/Jan/2003:12:11:46 <perl6-internals-return-14784-mjd-perl6-internals=plover.com@perl.org> 1 1 0 0 ... That was all a lot of work, and at this point it’s probably not clear why the stream method has any advantage over the more usual method of reading the file one record at a time, tracking the same data structures, and printing output records as we go, something like this: while (<LOG>) { # analyze current record # update $msg and $del if (/ˆend msg/) { print ...; } } One advantage was that we could encapsulate the follow-the-changing-file behavior inside its own stream.

…

Dominus presents even the most complex ideas in simple, comprehensible ways, but never compromises on the precision and attention to detail for which he is so widely and justly admired. His writing is — as always — lucid, eloquent, witty, and compelling. Aptly named, this truly is a Perl book of a higher order, and essential reading for every serious Perl programmer. —Damian Conway, Co-designer of Perl 6 For Lorrie Higher-Order Perl Transforming Programs with Programs Mark-Jason Dominus Preface A well-known saying in the programming racket is that a good Fortran programmer can write Fortran programs in any language. The sad truth, though, is that Fortran programmers write Fortran programs in any language whether they mean to or not.

…

While this is occasionally useful enough to be worth the extra costs, it’s usually simpler to declare that calling start twice on the same iterator is erroneous. 4.5.7 Iterator Methods People can be funny about syntax, and Perl programmers are even more obsessed with syntax than most people. When Larry Wall described the syntax of Perl 6 for the first time, people were up in arms because he was replacing the -> operator with . and the . operator with _. Even though there is only a little difference between: $it->start and: $it->('start') people love the first one and hate the second one. It’s easy to make the first syntax available though.

**
The Architecture of Open Source Applications
** by
Amy Brown,
Greg Wilson

Amazon: amazon.com — amazon.co.uk — amazon.de — amazon.fr

8-hour work day, anti-pattern, bioinformatics, c2.com, cloud computing, collaborative editing, combinatorial explosion, computer vision, continuous integration, create, read, update, delete, David Heinemeier Hansson, Debian, domain-specific language, Donald Knuth, en.wikipedia.org, fault tolerance, finite state, Firefox, friendly fire, Guido van Rossum, linked data, load shedding, locality of reference, loose coupling, Mars Rover, MVC pattern, peer-to-peer, Perl 6, premature optimization, recommendation engine, revision control, Ruby on Rails, side project, Skype, slashdot, social web, speech recognition, the scientific method, The Wisdom of Crowds, web application, WebSocket

Audrey Tang (SocialCalc): Audrey is a self-educated programmer and translator based in Taiwan. She curently works at Socialtext, where her job title is "Untitled Page", as well as at Apple as contractor for localization and release engineering. She previously designed and led the Pugs project, the first working Perl 6 implementation; she has also served in language design committees for Haskell, Perl 5, and Perl 6, and has made numerous contributions to CPAN and Hackage. She blogs at http://pugs.blogs.com/audreyt/. Huy T. Vo (VisTrails): Huy is receiving his Ph.D. from the University of Utah in May, 2011. His research interests include visualization, dataflow architecture and scientific data management.

…

This asynchronous style of collaboration compelled us to produce self-descriptive artifacts (design sketch, code and tests), which in turn greatly improved our trust in each other. 19.8.4. Optimize for Fun In my 2006 keynote for the CONISLI conference [Tan06], I summarized my experience leading a distributed team implementing the Perl 6 language into a few observations. Among them, Always have a Roadmap, Forgiveness > Permission, Remove deadlocks, Seek ideas, not consensus, and Sketch ideas with code are particularly relevant for small distributed teams. When developing SocialCalc, we took great care in distributing knowledge among team members with collaborative code ownership, so nobody would become a critical bottleneck.

…

These cultural traits helped us foster a sense of anticipation and camaraderie despite the absence of face-to-face interaction, kept politics to a minimum, and made working on SocialCalc a lot of fun. 19.8.5. Drive Development with Story Tests Prior to joining Socialtext, I've advocated the "interleave tests with the specification" approach, as can be seen in the Perl 6 specification7, where we annotate the language specification with the official test suite. However, it was Ken Pier and Matt Heusser, the QA team for SocialCalc, who really opened my eyes to how this can be taken to the next level, bringing tests to the place of executable specification. In Chapter 16 of [GR09], Matt explained our story-test driven development process as follows: The basic unit of work is a "story," which is an extremely lightweight requirements document.

**
Types and Programming Languages
** by
Benjamin C. Pierce

Amazon: amazon.com — amazon.co.uk — amazon.de — amazon.fr

Albert Einstein, combinatorial explosion, experimental subject, finite state, Henri Poincaré, Perl 6, recommendation engine, sorting algorithm, Turing complete, Turing machine, type inference, Y Combinator

., 461 609 factorial, 52 fail, 16 failure vs. undefinedness, 16 families (of terms, types), 462 Featherweight Java, 247–264 fields, see instance variables; records finalizers, 515 finding type errors, 545 finite tree type, 285 finite-state generating function, 294 first-class polymorphism, 340 fixed point, 142–145 combinator, 65 of a generating function, 282 theorem (Tarski-Knaster), 283 typing, using recursive types, 273 FJ, see Featherweight Java flattened data structures, 341 Float type, 117 fold function, 63 fomsub implementation, 467–473 formal methods, lightweight, 1 Forsythe, 11, 199 Fortran, 8, 11 fragments of System F, 358–359 fragments of System Fω , 461 free variable, 55, 69 fresh variable, 120 full abstraction, 143 full beta-reduction, 56 full F<: , 391 fullequirec implementation, 267–280 fullerror implementation, 171–178 fullfomsub implementation, 389–409, 467–473 fullfsub implementation, 389–409, 417– 436 fullfsubref implementation, 411–416 fullisorec implementation, 275–278 fullomega implementation, 439–466 fullpoly implementation, 339–379 fullrecon implementation, 317–338 fullref implementation, 153–170, 225– 245 610 Index fullsimple implementation, 99–111, 117–146 fullsub implementation, 181–208 fulluntyped implementation, 51–73 fullupdate implementation, 475–489 <fun>, 118 function types, 99–100 functional languages, mostly, 153 functions, 16 higher-order, 58 multi-argument, 58 on types, see type operators Funnel, 409 FX, 11 garbage collection, 45, 158–165, 514– 515 tag free, 341 general recursion, 142–145 generating function, 282 generating set, 290 generation lemma, see inversion lemma generators, classes as, 229 generics, 341 gfp algorithm, 292, 295–298 GJ, 195, 248, 409 grammar, 24 graph reduction, 57 greatest fixed point of a generating function, 283 greatest lower bound, see joins and meets greedy type inference, 355 hash consing, 222 Haskell, 6, 45 heap, 153 hidden representation type, 364 higher-order bounded quantifiers, 468 higher-order functions, 58 higher-order polymorphism, 449–466 history of type systems, 10 hungry functions, 270 hybrid object models, 377 identity, object, 245 identity function, 55 imperative objects, see objects, imperative implementations allsome, 381–387 arith, 23–49 bot, 220 equirec, 281–313 fomsub, 467–473 fullequirec, 267–280 fullerror, 171–178 fullfomsub, 389–409, 467–473 fullfsub, 389–409, 417–436 fullfsubref, 411–416 fullisorec, 275–278 fullomega, 439–466 fullpoly, 339–379 fullrecon, 317–338 fullref, 153–170, 225–245 fullsimple, 99–111, 117–146 fullsub, 181–208 fulluntyped, 51–73 fullupdate, 475–489 joinexercise, 223 joinsub, 218–220 purefsub, 417–436 rcdsub, 181–224 recon, 317–338 reconbase, 330 simplebool, 113–116 tyarith, 91–98 untyped, 83–88 implicit type annotations, 330–331 implicitly typed languages, 101 impredicative polymorphism, 340, 360– 361 impure language features, 153 induction, 19 lexicographic, 19 logical relations proof technique, 150 mathematical foundations, 282–284 on derivations, 37 on natural numbers, 19 on terms, 29–32 Index inductive definitions, 23–29 inference, see type reconstruction inference rules, 26 mathematical foundations, 283 infinite types, 284–286 inheritance, 227 overrated, 245 injection into a sum type, 133 instance of an inference rule, 36 instance variables, 228, 230, 233–234 instanceof, 341 instantiation of a polymorphic function, 317–320, 342 intensional polymorphism, 340 interface, 226 interface types, 479 interfaces (in Java), 261 interference, syntactic control of, 170 intermediate language, 161 intermediate languages, typed, 11 internal language, 53, 120 internet, see web intersection types, 11, 206–207, 359, 489 and bounded quantification, 400, 409 and normal forms, 206 introduction rule, 108 invariant, 33 inversion lemma subtyping, 188 typing, 94, 104, 188, 457 iso-recursive types, 275, 280 subtyping, 311–312 Java, 6, 8–10, 45, 119, 137, 154, 174, 177, 178, 193, 195, 196, 198–199, 226, 232, 247–264, 341, 444 exception handling in, 174 parametric polymorphism, 195 reflection, 196 JINI, 9 joinexercise implementation, 223 joins and meets, 17 algorithms for calculating, 218–220 in System F<: , 432–435 611 joinsub implementation, 218–220 judgment, 36 KEA, 226 kernel F<: , 391 kinding, 439–447, 459 kinds dependent, 445 power, 445 row, 445 singleton, 445 Knaster-Tarski fixed point theorem, 283 λ-calculus, see lambda-calculus λNB, 63–66 λ→ , see simply typed lambda-calculus λω , see System λω λ<: , see simply typed lambda-calculus with subtyping label, 129 lambda cube, 465 lambda-& calculus, 226, 340 lambda-calculi, typed, 2 lambda-calculus, 51, 52 enriched, 63–68 simply typed, see simply typed lambdacalculus untyped, see untyped lambda-calculus lambda-term, 53 language definition, defined, 7 language design and type systems, 9– 10 language features, pure, 153 late binding, see objects, open recursion latent type system, 2 lazy evaluation, 57 least fixed point of a generating function, 283 least upper bound, see joins and meets left-associativity of application, 54 let bindings, 124–125 let-polymorphism, 331–336, 340 exponential behavior, 334 levels, de Bruijn, 81 612 Index lexical analysis, 53 lexicographic induction, 19 lexicographic order, 19 LF, 11, 465 lfp algorithm, 294 lightweight formal methods, 1 linear logic and type systems, 11, 109 linking, 367 lists, 146 Church encoding, 350–353, 500 defined using recursive types, 267– 270 polymorphic functions for, 345–347 subtyping, 197 local type inference, 355 location, 159 logic and type systems, 108 origins, 11 type systems in, 2 logical framework, 465 logical relations, 149 µ, see least fixed point µ notation for recursive types, 299– 304 marshaling, 252, 341 Martin-Löf type theory, see constructive type theory match function, 131 matching, pattern-, 130–131 matching relation on object types, 480 mathematics, formalization of, 11 meaning of terms, 32–34 meet, see joins and meets membership checking for (co-)inductively defined sets, 290–298 Mercury, 338 message, 226 meta-mathematics, 24 metalanguage, 24 metatheory, 24 metavariables, 24 naming conventions, 565 method, 226, 228 invocation, 226 multi-, see multi-method override, 233, 264 Milner-Mycroft Calculus, 338 minimal types, 218, 418–420 minimal typing theorem, 419 mini-ML, 337 ML, 6, 8, 9, 11, 174, 177 exception handling in, 174 history, 336–338 module system, 379 parametric datatypes, 445 polymorphism, 331–336 ML implementations evaluation, 87 simply typed lambda-calculus, 113– 116 subtyping, 221–224 System F, 381–387 untyped arithmetic expressions, 45– 49 untyped lambda-calculus, 83–88 ML-style polymorphism, 340 modal logics, 109 model checking, 1, 284 Modula-3, 7 modularity, 3 module systems, 364, 379, 465 monads, 153 monitoring, run-time, 1 monotone function, 282 monotype, 359 most general unifier, 327 mostly functional languages, 153 multi-argument functions, 58 multi-method, 226, 340 multiple inheritance, 489 multiple representations (of object types), 226 multi-step evaluation, 39 mutually recursive functions, 144 types, 253 Index ν, see greatest fixed point nameless form, see de Bruijn indices naming context, 77 naming conventions for metavariables and rules, 565–566 narrowing lemmas, 401, 425 National Science Foundation, xx natural deduction, 26 natural semantics, 32, 34, 43 natural-number induction, 19 nested induction, 19 NextGen, 196 nominal type systems, 251–254, 312 normal forms, 38 and intersection types, 206 uniqueness of, 39 normal order, 56 normalization, 149–152 by evaluation, 152 strong, 152 normalization theorem, 39, 152, 353 numeric values, 40 NuPRL, 11 object calculus, 11, 51, 184, 248, 251 object language, 24 Objective Caml see OCaml, xvii objects, 228, 368 as recursive records, 272 bounded quantification and, 411–416 encodings vs. primitive objects, 262– 263 existential, 372–377, 475–489 hybrid object models, 377 identity, 245 imperative, 157, 225–245, 411–416 interface types, 479 Java-style, 247–264 matching relation on object types, 480 object-oriented programming, defined, 225–227 open recursion, 227, 235–244 purely functional, 372–377, 475–489 613 vs. abstract data types, 374–377 OCaml, xvii, 7, 45, 208, 231, 489 OCaml implementations, see ML implementations occur check, 327, 338 omega, 65 open recursion, see objects, open recursion operational semantics, 32, see also evaluation big-step, 43 small-step, 42 operator associativity, 53 operator precedence, 53 Option type, 137–138 order, well-founded, 18 ordered sets, basic definitions, 16–18 ordinary induction, 19 overloading, 340 finitary, 206 overriding of method definitions, 233 P(S) powerset of S, 15 package, existential, 364 pairs, 126–127 Church encodings, see Church encodings, pairs parallel reduction, 454 parametric abbreviation, 439 data type, 142, 444 polymorphism, 319, 340 parametricity, 359–360 parentheses and abstract syntax, 25, 52 parsing, 53 partial evaluation, 109 partial function, 16 partial order, 17 partially abstract types, 406 Pascal, 11 pattern matching, 130–131 PCF, 143 Pebble, 465 Penn translation, 204 614 Index Perl, 6 permutation, 18 permutation lemma, 106 permutation rule for record subtyping, 184 performance issues, 201–202 pi-calculus, 51 Pict, 200, 356, 409 Pizza, 195 pointer, 154, see references arithmetic, 159 pointwise subtyping of type operators, 468 polarity, 473 PolyJ, 195 polymorphic functions for lists, 345–347 identity function, 342 recursion, 338 update, 482–485 polymorphism, 331 ad hoc, 340 data abstraction, 368–377 existential, see existential types existential types, 363–379 exponential behavior of ML-style, 334 F-bounded, 393, 408 higher-order, 449–466 impredicativity and predicativity, 360– 361 intensional, 340 ML-style, 331–336 parametric, 339–361 parametricity, 359–360 predicative, 360 prenex, 359 rank-2, 359 safety problems with references, 335– 336 stratified, 360 subtype, see subtyping universal, see universal types varieties of, 340–341 polytype, 359 portability, types and, 7 positive subtyping, 489 Postscript, 6 power types, 445, 472 precedence of operators, 53 predecessor for Church numerals, 62 predicate, 15 predicative polymorphism, 360–361 prenex polymorphism, 359 preorder, 17 preservation of a predicate by a relation, 16 preservation of shapes under type reduction, 456 preservation of types during evaluation, 95–98, 107, 168, 173, 189, 261, 353, 404, 457 preservation of typing under type substitution, 318 principal type, 317, 329–330 types theorem, 329 typing, 337 unifier, 327 principal solution, 329 principle of safe substitution, 182 product type, 126–127 programming languages Abel, 409 Algol-60, 11 Algol-68, 11 Amber, 311 C, 6, 45 C] , 7 C++, 6, 226 Cecil, 226, 340 Clean, 338 CLOS, 226, 340 CLU, 11, 408 Dylan, 226 Featherweight Java, 247–264 Forsythe, 11, 199 Fortran, 8, 11 Funnel, 409 615 Index FX, 11 GJ, 195, 248, 409 Haskell, 6, 45 Java, 6, 8–10, 45, 119, 137, 154, 174, 177, 178, 193, 195, 196, 198–199, 226, 232, 247–264, 341, 444 KEA, 226 Mercury, 338 ML, 6, 8, 9, 11, 174, 177, see also OCaml, Standard ML Modula-3, 7 NextGen, 196 Objective Caml, see OCaml OCaml, xvii, 7, 208, 231, 489 Pascal, 11 Pebble, 465 Perl, 6 Pict, 200, 356, 409 Pizza, 195 PolyJ, 195 Postscript, 6 Quest, 11, 409 Scheme, 2, 6, 8, 45 Simula, 11, 207 Smalltalk, 226 Standard ML, xvii, 7, 45 Titanium, 8 XML, 9, 207, 313 progress theorem, 38, 95–98, 105, 169, 173, 190, 262, 353, 405, 458 projection (from pairs, tuples, records), 126–131 promotion, 418 proof, defined, 20 proof-carrying code, 9 proof theory, 2 proper types, 442 propositions as types, 109 pure λ→ , 102 pure lambda-calculus, 51 pure language features, 153 pure type systems, xiv, 2, 444, 466 purefsub implementation, 417–436 qualified types, 338 quantification, see polymorphism Quest, 11, 409 ramified theory of types, 2 range of a relation, 16 rank-2 polymorphism, 359 raw type, 248 rcdsub implementation, 181–224 reachableF , 294 recon implementation, 317–338 reconbase implementation, 330 reconstruction, see type reconstruction record kinds, 445 records, 129–131 Cardelli-Mitchell calculus, 207 Church encoding, 396–400 concatenation, 207 row variables, 208, 337 recursion, 65–66, 142–145 fixed-point combinator, 65 polymorphic, 338 recursive types, 253, 267–280 Amadio-Cardelli algorithm, 309–311 and subtyping, 279 equi-recursive vs. iso-recursive, 275 history, 279–280 in ML, 277–278 in nominal systems, 253 metatheory, 281–313 µ notation, 299–304 subtyping, 281–290, 298–313 type reconstruction, 313, 338 recursive values from recursive types, 273 redex, 56 reduce function, 63 reducibility candidates, 150 reduction vs. evaluation (terminology), 34 references, 153–170 allocation, 154 and subtyping, 199–200 assignment, 154 dereferencing, 154 subtyping, 198 616 Index type safety problems, 158 type safety problems with polymorphism, 335–336 refinement types, 207 reflection, 196, 252 and casting, 196 reflexive closure, 17 reflexive relation, 16 reflexivity of subtyping, 182 region inference, 8 regular trees, 298–299 relation, 15 logical, see logical relations removenames, 78 representation independence, 371 representation of numbers by Church numerals, 67 representation type (of an object), 230 restorenames, 78 row kinds, 445 row variables, 11, 208, 337, 489 rule computation, 35, 72 congruence, 35, 72 naming conventions, 565 schema, 27 rule, inference, 27 rule schema, 27 rules B-IfFalse, 43 B-IfTrue, 43 B-IszeroSucc, 43 B-IszeroZero, 43 B-PredSucc, 43 B-PredZero, 43 B-Succ, 43 B-Value, 43 CT-Abs, 322, 542 CT-AbsInf, 330 CT-App, 322, 542 CT-False, 322 CT-Fix, 543 CT-If, 322 CT-IsZero, 322 CT-LetPoly, 332 CT-Pred, 322 CT-Proj, 545 CT-Succ, 322 CT-True, 322 CT-Var, 322, 542 CT-Zero, 322 E-Abs, 502 E-App1, 72, 103, 160, 166, 186, 343, 392, 446, 450, 470, 502, 503 E-App2, 72, 103, 160, 166, 186, 343, 392, 446, 450, 470, 502 E-AppAbs, 72, 81, 103, 160, 166, 186, 342, 343, 392, 446, 450, 470, 502, 503 E-AppErr1, 172 E-AppErr2, 172 E-AppRaise1, 175 E-AppRaise2, 175 E-Ascribe, 122, 194 E-Ascribe1, 122 E-AscribeEager, 123 E-Assign, 161, 166 E-Assign1, 161, 166 E-Assign2, 161, 166 E-Case, 132, 136 E-CaseInl, 132, 135 E-CaseInr, 132, 135 E-CaseVariant, 136 E-Cast, 258 E-CastNew, 258 E-Cons1, 147 E-Cons2, 147 E-Deref, 161, 166 E-DerefLoc, 161, 166 E-Downcast, 195 E-Field, 258 E-Fix, 144 E-FixBeta, 144 E-Fld, 276 E-Funny1, 40 E-Funny2, 40 E-GC, 514 E-Head, 147 Index E-HeadCons, 147 E-If, 34 E-If-Wrong, 42 E-IfFalse, 34 E-IfTrue, 34 E-Inl, 132, 135 E-Inr, 132, 135 E-Invk-Arg, 258 E-Invk-Recv, 258 E-InvkNew, 258 E-Isnil, 147 E-IsnilCons, 147 E-IsnilNil, 147 E-IsZero, 41 E-IsZero-Wrong, 42 E-IszeroSucc, 41 E-IszeroZero, 41 E-Let, 124, 131, 335 E-LetV, 124, 131, 332 E-New-Arg, 258 E-Pack, 366, 452 E-Pair1, 126 E-Pair2, 126 E-PairBeta1, 126 E-PairBeta2, 126 E-Pred, 41 E-Pred-Wrong, 42 E-PredSucc, 41, 48 E-PredZero, 41 E-Proj, 128, 129, 187 E-Proj1, 126 E-Proj2, 126 E-ProjNew, 258 E-ProjRcd, 129, 187, 201, 484 E-ProjTuple, 128 E-Raise, 175 E-RaiseRaise, 175 E-Rcd, 129, 187, 484 E-Ref, 162, 166 E-RefV, 162, 166 E-Seq, 120 E-SeqNext, 120 E-Succ, 41 E-Succ-Wrong, 42 617 E-Tail, 147 E-TailCons, 147 E-TApp, 343, 392, 450, 470 E-TappTabs, 342, 343, 385, 392, 450, 470 E-Try, 174, 175 E-TryError, 174 E-TryRaise, 175 E-TryV, 174, 175 E-Tuple, 128 E-Typetest1, 195 E-Typetest2, 195 E-Unfld, 276 E-UnfldFld, 276 E-Unpack, 366 E-UnpackPack, 366, 367, 452 E-UpdateV, 484 E-Variant, 136 E-Wildcard, 507 K-Abs, 446, 450, 470 K-All, 450, 470 K-App, 446, 450, 470 K-Arrow, 446, 450, 470 K-Some, 452 K-Top, 470 K-TVar, 446, 450, 470 M-Rcd, 131 M-Var, 131 P-Rcd, 509 P-Rcd’, 509 P-Var, 509 Q-Abs, 446, 451, 471 Q-All, 451, 471 Q-App, 446, 451, 471 Q-AppAbs, 441, 446, 451, 471 Q-Arrow, 446, 451, 471 Q-Refl, 446, 451, 471 Q-Some, 452 Q-Symm, 446, 451, 471 Q-Trans, 446, 451, 471 QR-Abs, 454 QR-All, 454 QR-App, 454 QR-AppAbs, 454 618 Index QR-Arrow, 454 QR-Refl, 454 S-Abs, 468, 471 S-All, 392, 394, 395, 427, 471 S-Amber, 311 S-App, 468, 471 S-Array, 198 S-ArrayJava, 198 S-Arrow, 184, 186, 211, 392, 471 S-Assumption, 311 S-Bot, 192 S-Eq, 468, 471 S-Inter1, 206 S-Inter2, 206 S-Inter3, 206 S-Inter4, 206 S-List, 197 S-ProdDepth, 187 S-ProdWidth, 187 S-Rcd, 211 S-RcdDepth, 183, 187, 484 S-RcdPerm, 184, 187 S-RcdVariance, 484 S-RcdWidth, 183, 187, 484 S-Ref, 198 S-Refl, 182, 186, 211, 392 S-RefSink, 199 S-RefSource, 199 S-Sink, 199 S-Some, 406, 476, 556 S-Source, 199 S-Top, 185, 186, 211, 392, 471 S-Trans, 183, 186, 209, 211, 392, 471 S-TVar, 392, 394, 471 S-VariantDepth, 197 S-VariantPerm, 197 S-VariantWidth, 197 SA-All, 422, 424 SA-Arrow, 212, 422, 424 SA-Bot, 220 SA-Rcd, 212 SA-Refl-TVar, 422, 424 SA-Top, 212, 422, 424 SA-Trans-TVar, 422, 424 T-Abs, 101, 103, 167, 186, 343, 392, 447, 451, 471 T-App, 102, 103, 167, 181, 186, 343, 392, 447, 451, 471 T-Ascribe, 122, 194 T-Assign, 159, 165, 167, 199 T-Case, 132, 136 T-Cast, 530 T-Cons, 147 T-DCast, 259 T-Deref, 159, 165, 167, 199 T-Downcast, 194 T-Eq, 441, 447, 451 T-Error, 172 T-Exn, 175 T-False, 93 T-Field, 259 T-Fix, 144 T-Fld, 276 T-Head, 147 T-If, 93, 102, 218 T-Inl, 132, 135 T-Inr, 132, 135 T-Invk, 259 T-Isnil, 147 T-IsZero, 93 T-Let, 124, 332, 509 T-LetPoly, 332, 333 T-Loc, 164, 167 T-New, 259 T-Nil, 147 T-Pack, 365, 366, 406, 452 T-Pair, 126 T-Pred, 93 T-Proj, 128, 129, 187, 484 T-Proj1, 126 T-Proj2, 126 T-Rcd, 129, 187, 484 T-Ref, 159, 165, 167 T-SCast, 259 T-Seq, 120 T-Sub, 182, 186, 209, 392, 471 T-Succ, 93 Index T-TAbs, 342, 343, 392, 395, 451, 471 T-Tail, 147 T-TApp, 342, 343, 392, 395, 451, 471 T-True, 93 T-Try, 174, 175 T-Tuple, 128 T-Typetest, 195 T-UCast, 259 T-Unfld, 276 T-Unit, 119, 167 T-Unpack, 366, 406, 435, 452 T-Update, 484 T-Var, 101, 103, 167, 186, 259, 343, 392, 447, 451, 471 T-Variant, 136, 197 T-Wildcard, 507 T-Zero, 93 TA-Abs, 217, 419 TA-App, 217, 419 TA-AppBot, 220 TA-If, 220, 526 TA-Proj, 217 TA-ProjBot, 220 TA-Rcd, 217 TA-TAbs, 419 TA-TApp, 419 TA-Unpack, 436 TA-Var, 217, 419 XA-Other, 418 XA-Promote, 418 run-time code generation, 109 run-time error, 42 trapped vs. untrapped, 7 run-time monitoring, 1 safety, 3, 6–8, 95–98 problems with references, 158 problems with references and polymorphism, 335–336 satisfaction of a constraint set by a substitution, 321 saturated sets, 150 Scheme, 2, 6, 8, 45 units, 368 scope, 55 619 scoping of type variables, 393–394 second-order lambda-calculus, 341, 461 security, type systems and, 9 self, 227, 234–244, 486–488 semantics alternative styles, 32–34 axiomatic, 33 denotational, 33 operational, 32 semi-unification, 338 semistructured databases, 207 sequences, basic notations, 18 sequencing notation, 119–121 and references, 155 sets, basic operations on, 15 sharing, 445, 465 shifting (of nameless terms), 78–80 ML implementation, 85–87 side effects, 153 simple theory of types, 2 simple types, 100 simplebool implementation, 113–116 simply typed lambda-calculus, 2, 11, 99–111 extensions, 117–146 ML implementation, 113–116 pure, 102 with type operators, 445 Simula, 11, 207 single-field variant, 138–140 singleton kinds, 441, 445, 465 size of a term, 29 small-step operational semantics, 32, 42 Smalltalk, 226 soundness, see safety soundness and completeness, 212 of algorithmic subtyping, 423 of constraint typing, 325 Source and Sink constructors, 199 spurious subsumption, 253 Standard ML, xvii, 7, 45 statement, 36 static distance, 76 620 Index static vs. dynamic typing, 2 store, 153 store typing, 162–165 stratified polymorphism, 360 streams, 270–271 strict vs. non-strict evaluation, 57 String type, 117 strong binary operations, 376 strong normalization, 152, 353 structural operational semantics, 32, 34 structural unfolding, 489 structural vs. nominal type systems, 251–254 stuck term, 41 stupid cast, 259–260 subclass, 227, 232 subexpressions of µ-types, 304–309 subject expansion, 98, 108 subject reduction, see preservation subscripting conventions, 566 subset semantics of subtyping, 182, 201–202 substitution, 69–72, 75–81, 83–88 capture-avoiding, 70 ML implementation, 85–87 type-, 317 substitution lemma, 106, 168, 189, 453 substitution on types, 342 ML implementation, 382 subsumption, 181–182 postponement of, 214 subtraction of Church numerals, 62 subtype polymorphism, see subtyping subtyping, 181–224, see also bounded quantification Top and Bot types, 191–193 algorithm, 209–213, 417–436 algorithmic, in nominal systems, 253 and ascription, 193–196 and base types, 200 and channel types, 200 and objects, 227 and references, 199–200 and type reconstruction, 338, 355 and variant types, 196–197 arrays, 198–199 coercion semantics, 200–206 depth, 183 higher-order, 11, 467–473 intersection types, 206–207 iso-recursive types, 311–312 joins and meets in System F<: , 432– 435 lists, 197 ML implementation, 221–224 objects, 229–230 positive, 489 power types, 472 record permutation, 184 recursive types, 279, 281–290, 298– 313 references, 198 reflexivity, 182 subset semantics, 182, 201–202 subtype relation, 182–187 transitivity, 183 type operators, 467–473 undecidability of System F<: , 427– 431 union types, 206–207 vs. other forms of polymorphism, 341 width, 183 sum types, 132–135 super, 234 supertype, 182 support, 290 surface syntax, 53 syllabi for courses, xvii symmetric relation, 16 syntactic control of interference, 170 syntactic sugar, 121 syntax, 26–29, 52–55, 69 ML implementation, 46–47, 383–385 syntax-directedness, 209 System F, 11, 339–361 fragments, 358–359 history, 341 Index ML implementation, 381–387 System Fω , 449–466 and higher-order logic, 109 fragments, 461 System Fω <: , 467–473 System F<: , 389–409 kernel and full variants, 391 System λω , 445–447 T , see terms tag, type-, 2 tag-free garbage collection, 341 tagged representation of atomic values, 201 tagging creating new types by, 133 tail recursion, 296 TAL, 11 Tarski-Knaster fixed point theorem, 283 termination measure, 39 terminology, reduction vs. evaluation, 34 terms, 24, 26 and expressions (terminology), 24 closed, 55 depth, 29 induction on, 29–32 inductive definition of (nameless form), 77 ML implementation, 46, 83–85 nameless form, see de Bruijn indices size, 29 stuck, 41 theorem proving, types in, 9, 464 this, see self thunk, 239 TinkerType, xx Titanium, 8 Top type, 185, 191–193 top-down subexpressions of a recursive type, 304 Top[K], 468 total function, 16 total order, 17 transitive closure, 17, 289 621 transitive relation, 16 transitivity and coinduction, 288–290 transitivity of subtyping, 183 translucent types, 11 trapped vs. untrapped errors, 7 tree, 538 abstract syntax, 25 derivation, 36 regular, 298–299 type, 285 treeof, 300 tuples, 126–129 two-counter machines, 430 tyarith implementation, 91–98 typability, 93, 109–110, 354–357 type abstraction, 342 type annotations, 3, 10, 111 type application, 342 type classes, 337, 338 type constructors, see type operators type destructors, 489 type environment, 101 type equivalence, 447, 453–456 type erasure, 110, 354 type errors, 3 finding, 545 type exposure, 417–418 type inference, see type reconstruction type names, 251 type operators, 100, 439–447 bounded, 473 co- and contravariant, 473 definition equivalence, 441 in nominal systems, 254 quantification over, 449–466 subtyping, 467–473 type reconstruction, 317–338, 354–357 colored local type inference, 355 greedy, 355 history, 336–338 local type inference, 355 recursive types, 313, 338 subtyping, 338, 355 type safety, see safety 622 Index type scheme, 359 type substitution, 317 ML implementation, 382 type systems and efficiency, 8 and portability, 7 and security, 9 and theorem provers, 9, 464 applications, 8–9 as formal methods, 1 category theory and, 12 defined, 1–4 history, 10 in mathematics and logic, 2 language design and, 9–10 role in computer science, 1–4 type tags, 2, 196, 252 type theory, see type systems constructive, 2 type variables, 319–320 type-assignment systems, 101 type-directed partial evaluation, 152 type-erasure semantics, 357 type-passing semantics, 357 typecase, 341 typed arithmetic expressions, 91–98 typed assembly language, 11 typed intermediate languages, 11 typed lambda-calculi, 2 types, 92 typing context, 101 typing derivations, 94 desugaring of, 125 semantics defined on, 111, 200–206 typing relation, 92–95, 100–103 algorithm, 213–218 ML implementation, 113–116 properties, 104–108 undecidability of full type reconstruction for System F, 354 of partial type reconstruction for System F, 354 of subtyping for System F<: , 427– 431 undefinedness vs. failure, 16 unification, 321, 326–329 union types, 142, 206–207 disjoint, 142 uniqueness of normal forms, 39 uniqueness of types, 94, 104, 511 and annotations, 135, 141 and sums, 134–135 Unit type, 118–119 unit value, 118–119 units (in Scheme), 368 universal domain, 273 universal set, 282 universal types, 339–361 unsafe declarations, 7 untyped implementation, 83–88 untyped arithmetic expressions, 23–44 untyped lambda-calculus, 11, 51–73 representation using recursive types, 273–275 up-cast, see casting update, polymorphic, 482–485 value, 34, 57 numeric, 40 value restriction, 336, 358 variable capture, 70 variables bound, 55, 69–72 free, 55 variant types, 132–142 and subtyping, 196–197 extensible, 177 single-field, 138–140 vs. datatypes, 140–142 weak binary operations, 375 weak head reduction, 460 weak pointers, 515 weak type variable, 336 weakening lemma, 106 web resources, xx well-formed context, 459 Index well-founded order, 18 set, 18 well-typed term, 93 width subtyping, 183 wildcard bindings, 119–121 witness type, 364 wrong, 42, 73 XML, 9, 207, 313 Y combinator, 65 Year 2000 problem, 9 Z combinator, 65 623

…

., 461 609 factorial, 52 fail, 16 failure vs. undefinedness, 16 families (of terms, types), 462 Featherweight Java, 247–264 fields, see instance variables; records finalizers, 515 finding type errors, 545 finite tree type, 285 finite-state generating function, 294 first-class polymorphism, 340 fixed point, 142–145 combinator, 65 of a generating function, 282 theorem (Tarski-Knaster), 283 typing, using recursive types, 273 FJ, see Featherweight Java flattened data structures, 341 Float type, 117 fold function, 63 fomsub implementation, 467–473 formal methods, lightweight, 1 Forsythe, 11, 199 Fortran, 8, 11 fragments of System F, 358–359 fragments of System Fω , 461 free variable, 55, 69 fresh variable, 120 full abstraction, 143 full beta-reduction, 56 full F<: , 391 fullequirec implementation, 267–280 fullerror implementation, 171–178 fullfomsub implementation, 389–409, 467–473 fullfsub implementation, 389–409, 417– 436 fullfsubref implementation, 411–416 fullisorec implementation, 275–278 fullomega implementation, 439–466 fullpoly implementation, 339–379 fullrecon implementation, 317–338 fullref implementation, 153–170, 225– 245 610 Index fullsimple implementation, 99–111, 117–146 fullsub implementation, 181–208 fulluntyped implementation, 51–73 fullupdate implementation, 475–489 <fun>, 118 function types, 99–100 functional languages, mostly, 153 functions, 16 higher-order, 58 multi-argument, 58 on types, see type operators Funnel, 409 FX, 11 garbage collection, 45, 158–165, 514– 515 tag free, 341 general recursion, 142–145 generating function, 282 generating set, 290 generation lemma, see inversion lemma generators, classes as, 229 generics, 341 gfp algorithm, 292, 295–298 GJ, 195, 248, 409 grammar, 24 graph reduction, 57 greatest fixed point of a generating function, 283 greatest lower bound, see joins and meets greedy type inference, 355 hash consing, 222 Haskell, 6, 45 heap, 153 hidden representation type, 364 higher-order bounded quantifiers, 468 higher-order functions, 58 higher-order polymorphism, 449–466 history of type systems, 10 hungry functions, 270 hybrid object models, 377 identity, object, 245 identity function, 55 imperative objects, see objects, imperative implementations allsome, 381–387 arith, 23–49 bot, 220 equirec, 281–313 fomsub, 467–473 fullequirec, 267–280 fullerror, 171–178 fullfomsub, 389–409, 467–473 fullfsub, 389–409, 417–436 fullfsubref, 411–416 fullisorec, 275–278 fullomega, 439–466 fullpoly, 339–379 fullrecon, 317–338 fullref, 153–170, 225–245 fullsimple, 99–111, 117–146 fullsub, 181–208 fulluntyped, 51–73 fullupdate, 475–489 joinexercise, 223 joinsub, 218–220 purefsub, 417–436 rcdsub, 181–224 recon, 317–338 reconbase, 330 simplebool, 113–116 tyarith, 91–98 untyped, 83–88 implicit type annotations, 330–331 implicitly typed languages, 101 impredicative polymorphism, 340, 360– 361 impure language features, 153 induction, 19 lexicographic, 19 logical relations proof technique, 150 mathematical foundations, 282–284 on derivations, 37 on natural numbers, 19 on terms, 29–32 Index inductive definitions, 23–29 inference, see type reconstruction inference rules, 26 mathematical foundations, 283 infinite types, 284–286 inheritance, 227 overrated, 245 injection into a sum type, 133 instance of an inference rule, 36 instance variables, 228, 230, 233–234 instanceof, 341 instantiation of a polymorphic function, 317–320, 342 intensional polymorphism, 340 interface, 226 interface types, 479 interfaces (in Java), 261 interference, syntactic control of, 170 intermediate language, 161 intermediate languages, typed, 11 internal language, 53, 120 internet, see web intersection types, 11, 206–207, 359, 489 and bounded quantification, 400, 409 and normal forms, 206 introduction rule, 108 invariant, 33 inversion lemma subtyping, 188 typing, 94, 104, 188, 457 iso-recursive types, 275, 280 subtyping, 311–312 Java, 6, 8–10, 45, 119, 137, 154, 174, 177, 178, 193, 195, 196, 198–199, 226, 232, 247–264, 341, 444 exception handling in, 174 parametric polymorphism, 195 reflection, 196 JINI, 9 joinexercise implementation, 223 joins and meets, 17 algorithms for calculating, 218–220 in System F<: , 432–435 611 joinsub implementation, 218–220 judgment, 36 KEA, 226 kernel F<: , 391 kinding, 439–447, 459 kinds dependent, 445 power, 445 row, 445 singleton, 445 Knaster-Tarski fixed point theorem, 283 λ-calculus, see lambda-calculus λNB, 63–66 λ→ , see simply typed lambda-calculus λω , see System λω λ<: , see simply typed lambda-calculus with subtyping label, 129 lambda cube, 465 lambda-& calculus, 226, 340 lambda-calculi, typed, 2 lambda-calculus, 51, 52 enriched, 63–68 simply typed, see simply typed lambdacalculus untyped, see untyped lambda-calculus lambda-term, 53 language definition, defined, 7 language design and type systems, 9– 10 language features, pure, 153 late binding, see objects, open recursion latent type system, 2 lazy evaluation, 57 least fixed point of a generating function, 283 least upper bound, see joins and meets left-associativity of application, 54 let bindings, 124–125 let-polymorphism, 331–336, 340 exponential behavior, 334 levels, de Bruijn, 81 612 Index lexical analysis, 53 lexicographic induction, 19 lexicographic order, 19 LF, 11, 465 lfp algorithm, 294 lightweight formal methods, 1 linear logic and type systems, 11, 109 linking, 367 lists, 146 Church encoding, 350–353, 500 defined using recursive types, 267– 270 polymorphic functions for, 345–347 subtyping, 197 local type inference, 355 location, 159 logic and type systems, 108 origins, 11 type systems in, 2 logical framework, 465 logical relations, 149 µ, see least fixed point µ notation for recursive types, 299– 304 marshaling, 252, 341 Martin-Löf type theory, see constructive type theory match function, 131 matching, pattern-, 130–131 matching relation on object types, 480 mathematics, formalization of, 11 meaning of terms, 32–34 meet, see joins and meets membership checking for (co-)inductively defined sets, 290–298 Mercury, 338 message, 226 meta-mathematics, 24 metalanguage, 24 metatheory, 24 metavariables, 24 naming conventions, 565 method, 226, 228 invocation, 226 multi-, see multi-method override, 233, 264 Milner-Mycroft Calculus, 338 minimal types, 218, 418–420 minimal typing theorem, 419 mini-ML, 337 ML, 6, 8, 9, 11, 174, 177 exception handling in, 174 history, 336–338 module system, 379 parametric datatypes, 445 polymorphism, 331–336 ML implementations evaluation, 87 simply typed lambda-calculus, 113– 116 subtyping, 221–224 System F, 381–387 untyped arithmetic expressions, 45– 49 untyped lambda-calculus, 83–88 ML-style polymorphism, 340 modal logics, 109 model checking, 1, 284 Modula-3, 7 modularity, 3 module systems, 364, 379, 465 monads, 153 monitoring, run-time, 1 monotone function, 282 monotype, 359 most general unifier, 327 mostly functional languages, 153 multi-argument functions, 58 multi-method, 226, 340 multiple inheritance, 489 multiple representations (of object types), 226 multi-step evaluation, 39 mutually recursive functions, 144 types, 253 Index ν, see greatest fixed point nameless form, see de Bruijn indices naming context, 77 naming conventions for metavariables and rules, 565–566 narrowing lemmas, 401, 425 National Science Foundation, xx natural deduction, 26 natural semantics, 32, 34, 43 natural-number induction, 19 nested induction, 19 NextGen, 196 nominal type systems, 251–254, 312 normal forms, 38 and intersection types, 206 uniqueness of, 39 normal order, 56 normalization, 149–152 by evaluation, 152 strong, 152 normalization theorem, 39, 152, 353 numeric values, 40 NuPRL, 11 object calculus, 11, 51, 184, 248, 251 object language, 24 Objective Caml see OCaml, xvii objects, 228, 368 as recursive records, 272 bounded quantification and, 411–416 encodings vs. primitive objects, 262– 263 existential, 372–377, 475–489 hybrid object models, 377 identity, 245 imperative, 157, 225–245, 411–416 interface types, 479 Java-style, 247–264 matching relation on object types, 480 object-oriented programming, defined, 225–227 open recursion, 227, 235–244 purely functional, 372–377, 475–489 613 vs. abstract data types, 374–377 OCaml, xvii, 7, 45, 208, 231, 489 OCaml implementations, see ML implementations occur check, 327, 338 omega, 65 open recursion, see objects, open recursion operational semantics, 32, see also evaluation big-step, 43 small-step, 42 operator associativity, 53 operator precedence, 53 Option type, 137–138 order, well-founded, 18 ordered sets, basic definitions, 16–18 ordinary induction, 19 overloading, 340 finitary, 206 overriding of method definitions, 233 P(S) powerset of S, 15 package, existential, 364 pairs, 126–127 Church encodings, see Church encodings, pairs parallel reduction, 454 parametric abbreviation, 439 data type, 142, 444 polymorphism, 319, 340 parametricity, 359–360 parentheses and abstract syntax, 25, 52 parsing, 53 partial evaluation, 109 partial function, 16 partial order, 17 partially abstract types, 406 Pascal, 11 pattern matching, 130–131 PCF, 143 Pebble, 465 Penn translation, 204 614 Index Perl, 6 permutation, 18 permutation lemma, 106 permutation rule for record subtyping, 184 performance issues, 201–202 pi-calculus, 51 Pict, 200, 356, 409 Pizza, 195 pointer, 154, see references arithmetic, 159 pointwise subtyping of type operators, 468 polarity, 473 PolyJ, 195 polymorphic functions for lists, 345–347 identity function, 342 recursion, 338 update, 482–485 polymorphism, 331 ad hoc, 340 data abstraction, 368–377 existential, see existential types existential types, 363–379 exponential behavior of ML-style, 334 F-bounded, 393, 408 higher-order, 449–466 impredicativity and predicativity, 360– 361 intensional, 340 ML-style, 331–336 parametric, 339–361 parametricity, 359–360 predicative, 360 prenex, 359 rank-2, 359 safety problems with references, 335– 336 stratified, 360 subtype, see subtyping universal, see universal types varieties of, 340–341 polytype, 359 portability, types and, 7 positive subtyping, 489 Postscript, 6 power types, 445, 472 precedence of operators, 53 predecessor for Church numerals, 62 predicate, 15 predicative polymorphism, 360–361 prenex polymorphism, 359 preorder, 17 preservation of a predicate by a relation, 16 preservation of shapes under type reduction, 456 preservation of types during evaluation, 95–98, 107, 168, 173, 189, 261, 353, 404, 457 preservation of typing under type substitution, 318 principal type, 317, 329–330 types theorem, 329 typing, 337 unifier, 327 principal solution, 329 principle of safe substitution, 182 product type, 126–127 programming languages Abel, 409 Algol-60, 11 Algol-68, 11 Amber, 311 C, 6, 45 C] , 7 C++, 6, 226 Cecil, 226, 340 Clean, 338 CLOS, 226, 340 CLU, 11, 408 Dylan, 226 Featherweight Java, 247–264 Forsythe, 11, 199 Fortran, 8, 11 Funnel, 409 615 Index FX, 11 GJ, 195, 248, 409 Haskell, 6, 45 Java, 6, 8–10, 45, 119, 137, 154, 174, 177, 178, 193, 195, 196, 198–199, 226, 232, 247–264, 341, 444 KEA, 226 Mercury, 338 ML, 6, 8, 9, 11, 174, 177, see also OCaml, Standard ML Modula-3, 7 NextGen, 196 Objective Caml, see OCaml OCaml, xvii, 7, 208, 231, 489 Pascal, 11 Pebble, 465 Perl, 6 Pict, 200, 356, 409 Pizza, 195 PolyJ, 195 Postscript, 6 Quest, 11, 409 Scheme, 2, 6, 8, 45 Simula, 11, 207 Smalltalk, 226 Standard ML, xvii, 7, 45 Titanium, 8 XML, 9, 207, 313 progress theorem, 38, 95–98, 105, 169, 173, 190, 262, 353, 405, 458 projection (from pairs, tuples, records), 126–131 promotion, 418 proof, defined, 20 proof-carrying code, 9 proof theory, 2 proper types, 442 propositions as types, 109 pure λ→ , 102 pure lambda-calculus, 51 pure language features, 153 pure type systems, xiv, 2, 444, 466 purefsub implementation, 417–436 qualified types, 338 quantification, see polymorphism Quest, 11, 409 ramified theory of types, 2 range of a relation, 16 rank-2 polymorphism, 359 raw type, 248 rcdsub implementation, 181–224 reachableF , 294 recon implementation, 317–338 reconbase implementation, 330 reconstruction, see type reconstruction record kinds, 445 records, 129–131 Cardelli-Mitchell calculus, 207 Church encoding, 396–400 concatenation, 207 row variables, 208, 337 recursion, 65–66, 142–145 fixed-point combinator, 65 polymorphic, 338 recursive types, 253, 267–280 Amadio-Cardelli algorithm, 309–311 and subtyping, 279 equi-recursive vs. iso-recursive, 275 history, 279–280 in ML, 277–278 in nominal systems, 253 metatheory, 281–313 µ notation, 299–304 subtyping, 281–290, 298–313 type reconstruction, 313, 338 recursive values from recursive types, 273 redex, 56 reduce function, 63 reducibility candidates, 150 reduction vs. evaluation (terminology), 34 references, 153–170 allocation, 154 and subtyping, 199–200 assignment, 154 dereferencing, 154 subtyping, 198 616 Index type safety problems, 158 type safety problems with polymorphism, 335–336 refinement types, 207 reflection, 196, 252 and casting, 196 reflexive closure, 17 reflexive relation, 16 reflexivity of subtyping, 182 region inference, 8 regular trees, 298–299 relation, 15 logical, see logical relations removenames, 78 representation independence, 371 representation of numbers by Church numerals, 67 representation type (of an object), 230 restorenames, 78 row kinds, 445 row variables, 11, 208, 337, 489 rule computation, 35, 72 congruence, 35, 72 naming conventions, 565 schema, 27 rule, inference, 27 rule schema, 27 rules B-IfFalse, 43 B-IfTrue, 43 B-IszeroSucc, 43 B-IszeroZero, 43 B-PredSucc, 43 B-PredZero, 43 B-Succ, 43 B-Value, 43 CT-Abs, 322, 542 CT-AbsInf, 330 CT-App, 322, 542 CT-False, 322 CT-Fix, 543 CT-If, 322 CT-IsZero, 322 CT-LetPoly, 332 CT-Pred, 322 CT-Proj, 545 CT-Succ, 322 CT-True, 322 CT-Var, 322, 542 CT-Zero, 322 E-Abs, 502 E-App1, 72, 103, 160, 166, 186, 343, 392, 446, 450, 470, 502, 503 E-App2, 72, 103, 160, 166, 186, 343, 392, 446, 450, 470, 502 E-AppAbs, 72, 81, 103, 160, 166, 186, 342, 343, 392, 446, 450, 470, 502, 503 E-AppErr1, 172 E-AppErr2, 172 E-AppRaise1, 175 E-AppRaise2, 175 E-Ascribe, 122, 194 E-Ascribe1, 122 E-AscribeEager, 123 E-Assign, 161, 166 E-Assign1, 161, 166 E-Assign2, 161, 166 E-Case, 132, 136 E-CaseInl, 132, 135 E-CaseInr, 132, 135 E-CaseVariant, 136 E-Cast, 258 E-CastNew, 258 E-Cons1, 147 E-Cons2, 147 E-Deref, 161, 166 E-DerefLoc, 161, 166 E-Downcast, 195 E-Field, 258 E-Fix, 144 E-FixBeta, 144 E-Fld, 276 E-Funny1, 40 E-Funny2, 40 E-GC, 514 E-Head, 147 Index E-HeadCons, 147 E-If, 34 E-If-Wrong, 42 E-IfFalse, 34 E-IfTrue, 34 E-Inl, 132, 135 E-Inr, 132, 135 E-Invk-Arg, 258 E-Invk-Recv, 258 E-InvkNew, 258 E-Isnil, 147 E-IsnilCons, 147 E-IsnilNil, 147 E-IsZero, 41 E-IsZero-Wrong, 42 E-IszeroSucc, 41 E-IszeroZero, 41 E-Let, 124, 131, 335 E-LetV, 124, 131, 332 E-New-Arg, 258 E-Pack, 366, 452 E-Pair1, 126 E-Pair2, 126 E-PairBeta1, 126 E-PairBeta2, 126 E-Pred, 41 E-Pred-Wrong, 42 E-PredSucc, 41, 48 E-PredZero, 41 E-Proj, 128, 129, 187 E-Proj1, 126 E-Proj2, 126 E-ProjNew, 258 E-ProjRcd, 129, 187, 201, 484 E-ProjTuple, 128 E-Raise, 175 E-RaiseRaise, 175 E-Rcd, 129, 187, 484 E-Ref, 162, 166 E-RefV, 162, 166 E-Seq, 120 E-SeqNext, 120 E-Succ, 41 E-Succ-Wrong, 42 617 E-Tail, 147 E-TailCons, 147 E-TApp, 343, 392, 450, 470 E-TappTabs, 342, 343, 385, 392, 450, 470 E-Try, 174, 175 E-TryError, 174 E-TryRaise, 175 E-TryV, 174, 175 E-Tuple, 128 E-Typetest1, 195 E-Typetest2, 195 E-Unfld, 276 E-UnfldFld, 276 E-Unpack, 366 E-UnpackPack, 366, 367, 452 E-UpdateV, 484 E-Variant, 136 E-Wildcard, 507 K-Abs, 446, 450, 470 K-All, 450, 470 K-App, 446, 450, 470 K-Arrow, 446, 450, 470 K-Some, 452 K-Top, 470 K-TVar, 446, 450, 470 M-Rcd, 131 M-Var, 131 P-Rcd, 509 P-Rcd’, 509 P-Var, 509 Q-Abs, 446, 451, 471 Q-All, 451, 471 Q-App, 446, 451, 471 Q-AppAbs, 441, 446, 451, 471 Q-Arrow, 446, 451, 471 Q-Refl, 446, 451, 471 Q-Some, 452 Q-Symm, 446, 451, 471 Q-Trans, 446, 451, 471 QR-Abs, 454 QR-All, 454 QR-App, 454 QR-AppAbs, 454 618 Index QR-Arrow, 454 QR-Refl, 454 S-Abs, 468, 471 S-All, 392, 394, 395, 427, 471 S-Amber, 311 S-App, 468, 471 S-Array, 198 S-ArrayJava, 198 S-Arrow, 184, 186, 211, 392, 471 S-Assumption, 311 S-Bot, 192 S-Eq, 468, 471 S-Inter1, 206 S-Inter2, 206 S-Inter3, 206 S-Inter4, 206 S-List, 197 S-ProdDepth, 187 S-ProdWidth, 187 S-Rcd, 211 S-RcdDepth, 183, 187, 484 S-RcdPerm, 184, 187 S-RcdVariance, 484 S-RcdWidth, 183, 187, 484 S-Ref, 198 S-Refl, 182, 186, 211, 392 S-RefSink, 199 S-RefSource, 199 S-Sink, 199 S-Some, 406, 476, 556 S-Source, 199 S-Top, 185, 186, 211, 392, 471 S-Trans, 183, 186, 209, 211, 392, 471 S-TVar, 392, 394, 471 S-VariantDepth, 197 S-VariantPerm, 197 S-VariantWidth, 197 SA-All, 422, 424 SA-Arrow, 212, 422, 424 SA-Bot, 220 SA-Rcd, 212 SA-Refl-TVar, 422, 424 SA-Top, 212, 422, 424 SA-Trans-TVar, 422, 424 T-Abs, 101, 103, 167, 186, 343, 392, 447, 451, 471 T-App, 102, 103, 167, 181, 186, 343, 392, 447, 451, 471 T-Ascribe, 122, 194 T-Assign, 159, 165, 167, 199 T-Case, 132, 136 T-Cast, 530 T-Cons, 147 T-DCast, 259 T-Deref, 159, 165, 167, 199 T-Downcast, 194 T-Eq, 441, 447, 451 T-Error, 172 T-Exn, 175 T-False, 93 T-Field, 259 T-Fix, 144 T-Fld, 276 T-Head, 147 T-If, 93, 102, 218 T-Inl, 132, 135 T-Inr, 132, 135 T-Invk, 259 T-Isnil, 147 T-IsZero, 93 T-Let, 124, 332, 509 T-LetPoly, 332, 333 T-Loc, 164, 167 T-New, 259 T-Nil, 147 T-Pack, 365, 366, 406, 452 T-Pair, 126 T-Pred, 93 T-Proj, 128, 129, 187, 484 T-Proj1, 126 T-Proj2, 126 T-Rcd, 129, 187, 484 T-Ref, 159, 165, 167 T-SCast, 259 T-Seq, 120 T-Sub, 182, 186, 209, 392, 471 T-Succ, 93 Index T-TAbs, 342, 343, 392, 395, 451, 471 T-Tail, 147 T-TApp, 342, 343, 392, 395, 451, 471 T-True, 93 T-Try, 174, 175 T-Tuple, 128 T-Typetest, 195 T-UCast, 259 T-Unfld, 276 T-Unit, 119, 167 T-Unpack, 366, 406, 435, 452 T-Update, 484 T-Var, 101, 103, 167, 186, 259, 343, 392, 447, 451, 471 T-Variant, 136, 197 T-Wildcard, 507 T-Zero, 93 TA-Abs, 217, 419 TA-App, 217, 419 TA-AppBot, 220 TA-If, 220, 526 TA-Proj, 217 TA-ProjBot, 220 TA-Rcd, 217 TA-TAbs, 419 TA-TApp, 419 TA-Unpack, 436 TA-Var, 217, 419 XA-Other, 418 XA-Promote, 418 run-time code generation, 109 run-time error, 42 trapped vs. untrapped, 7 run-time monitoring, 1 safety, 3, 6–8, 95–98 problems with references, 158 problems with references and polymorphism, 335–336 satisfaction of a constraint set by a substitution, 321 saturated sets, 150 Scheme, 2, 6, 8, 45 units, 368 scope, 55 619 scoping of type variables, 393–394 second-order lambda-calculus, 341, 461 security, type systems and, 9 self, 227, 234–244, 486–488 semantics alternative styles, 32–34 axiomatic, 33 denotational, 33 operational, 32 semi-unification, 338 semistructured databases, 207 sequences, basic notations, 18 sequencing notation, 119–121 and references, 155 sets, basic operations on, 15 sharing, 445, 465 shifting (of nameless terms), 78–80 ML implementation, 85–87 side effects, 153 simple theory of types, 2 simple types, 100 simplebool implementation, 113–116 simply typed lambda-calculus, 2, 11, 99–111 extensions, 117–146 ML implementation, 113–116 pure, 102 with type operators, 445 Simula, 11, 207 single-field variant, 138–140 singleton kinds, 441, 445, 465 size of a term, 29 small-step operational semantics, 32, 42 Smalltalk, 226 soundness, see safety soundness and completeness, 212 of algorithmic subtyping, 423 of constraint typing, 325 Source and Sink constructors, 199 spurious subsumption, 253 Standard ML, xvii, 7, 45 statement, 36 static distance, 76 620 Index static vs. dynamic typing, 2 store, 153 store typing, 162–165 stratified polymorphism, 360 streams, 270–271 strict vs. non-strict evaluation, 57 String type, 117 strong binary operations, 376 strong normalization, 152, 353 structural operational semantics, 32, 34 structural unfolding, 489 structural vs. nominal type systems, 251–254 stuck term, 41 stupid cast, 259–260 subclass, 227, 232 subexpressions of µ-types, 304–309 subject expansion, 98, 108 subject reduction, see preservation subscripting conventions, 566 subset semantics of subtyping, 182, 201–202 substitution, 69–72, 75–81, 83–88 capture-avoiding, 70 ML implementation, 85–87 type-, 317 substitution lemma, 106, 168, 189, 453 substitution on types, 342 ML implementation, 382 subsumption, 181–182 postponement of, 214 subtraction of Church numerals, 62 subtype polymorphism, see subtyping subtyping, 181–224, see also bounded quantification Top and Bot types, 191–193 algorithm, 209–213, 417–436 algorithmic, in nominal systems, 253 and ascription, 193–196 and base types, 200 and channel types, 200 and objects, 227 and references, 199–200 and type reconstruction, 338, 355 and variant types, 196–197 arrays, 198–199 coercion semantics, 200–206 depth, 183 higher-order, 11, 467–473 intersection types, 206–207 iso-recursive types, 311–312 joins and meets in System F<: , 432– 435 lists, 197 ML implementation, 221–224 objects, 229–230 positive, 489 power types, 472 record permutation, 184 recursive types, 279, 281–290, 298– 313 references, 198 reflexivity, 182 subset semantics, 182, 201–202 subtype relation, 182–187 transitivity, 183 type operators, 467–473 undecidability of System F<: , 427– 431 union types, 206–207 vs. other forms of polymorphism, 341 width, 183 sum types, 132–135 super, 234 supertype, 182 support, 290 surface syntax, 53 syllabi for courses, xvii symmetric relation, 16 syntactic control of interference, 170 syntactic sugar, 121 syntax, 26–29, 52–55, 69 ML implementation, 46–47, 383–385 syntax-directedness, 209 System F, 11, 339–361 fragments, 358–359 history, 341 Index ML implementation, 381–387 System Fω , 449–466 and higher-order logic, 109 fragments, 461 System Fω <: , 467–473 System F<: , 389–409 kernel and full variants, 391 System λω , 445–447 T , see terms tag, type-, 2 tag-free garbage collection, 341 tagged representation of atomic values, 201 tagging creating new types by, 133 tail recursion, 296 TAL, 11 Tarski-Knaster fixed point theorem, 283 termination measure, 39 terminology, reduction vs. evaluation, 34 terms, 24, 26 and expressions (terminology), 24 closed, 55 depth, 29 induction on, 29–32 inductive definition of (nameless form), 77 ML implementation, 46, 83–85 nameless form, see de Bruijn indices size, 29 stuck, 41 theorem proving, types in, 9, 464 this, see self thunk, 239 TinkerType, xx Titanium, 8 Top type, 185, 191–193 top-down subexpressions of a recursive type, 304 Top[K], 468 total function, 16 total order, 17 transitive closure, 17, 289 621 transitive relation, 16 transitivity and coinduction, 288–290 transitivity of subtyping, 183 translucent types, 11 trapped vs. untrapped errors, 7 tree, 538 abstract syntax, 25 derivation, 36 regular, 298–299 type, 285 treeof, 300 tuples, 126–129 two-counter machines, 430 tyarith implementation, 91–98 typability, 93, 109–110, 354–357 type abstraction, 342 type annotations, 3, 10, 111 type application, 342 type classes, 337, 338 type constructors, see type operators type destructors, 489 type environment, 101 type equivalence, 447, 453–456 type erasure, 110, 354 type errors, 3 finding, 545 type exposure, 417–418 type inference, see type reconstruction type names, 251 type operators, 100, 439–447 bounded, 473 co- and contravariant, 473 definition equivalence, 441 in nominal systems, 254 quantification over, 449–466 subtyping, 467–473 type reconstruction, 317–338, 354–357 colored local type inference, 355 greedy, 355 history, 336–338 local type inference, 355 recursive types, 313, 338 subtyping, 338, 355 type safety, see safety 622 Index type scheme, 359 type substitution, 317 ML implementation, 382 type systems and efficiency, 8 and portability, 7 and security, 9 and theorem provers, 9, 464 applications, 8–9 as formal methods, 1 category theory and, 12 defined, 1–4 history, 10 in mathematics and logic, 2 language design and, 9–10 role in computer science, 1–4 type tags, 2, 196, 252 type theory, see type systems constructive, 2 type variables, 319–320 type-assignment systems, 101 type-directed partial evaluation, 152 type-erasure semantics, 357 type-passing semantics, 357 typecase, 341 typed arithmetic expressions, 91–98 typed assembly language, 11 typed intermediate languages, 11 typed lambda-calculi, 2 types, 92 typing context, 101 typing derivations, 94 desugaring of, 125 semantics defined on, 111, 200–206 typing relation, 92–95, 100–103 algorithm, 213–218 ML implementation, 113–116 properties, 104–108 undecidability of full type reconstruction for System F, 354 of partial type reconstruction for System F, 354 of subtyping for System F<: , 427– 431 undefinedness vs. failure, 16 unification, 321, 326–329 union types, 142, 206–207 disjoint, 142 uniqueness of normal forms, 39 uniqueness of types, 94, 104, 511 and annotations, 135, 141 and sums, 134–135 Unit type, 118–119 unit value, 118–119 units (in Scheme), 368 universal domain, 273 universal set, 282 universal types, 339–361 unsafe declarations, 7 untyped implementation, 83–88 untyped arithmetic expressions, 23–44 untyped lambda-calculus, 11, 51–73 representation using recursive types, 273–275 up-cast, see casting update, polymorphic, 482–485 value, 34, 57 numeric, 40 value restriction, 336, 358 variable capture, 70 variables bound, 55, 69–72 free, 55 variant types, 132–142 and subtyping, 196–197 extensible, 177 single-field, 138–140 vs. datatypes, 140–142 weak binary operations, 375 weak head reduction, 460 weak pointers, 515 weak type variable, 336 weakening lemma, 106 web resources, xx well-formed context, 459 Index well-founded order, 18 set, 18 well-typed term, 93 width subtyping, 183 wildcard bindings, 119–121 witness type, 364 wrong, 42, 73 XML, 9, 207, 313 Y combinator, 65 Year 2000 problem, 9 Z combinator, 65 623

**
Coders at Work
** by
Peter Seibel

Amazon: amazon.com — amazon.co.uk — amazon.de — amazon.fr

Ada Lovelace, bioinformatics, cloud computing, Conway's Game of Life, domain-specific language, don't repeat yourself, Donald Knuth, fault tolerance, Fermat's Last Theorem, Firefox, George Gilder, glass ceiling, Guido van Rossum, HyperCard, information retrieval, Larry Wall, loose coupling, Marc Andreessen, Menlo Park, Metcalfe's law, Perl 6, premature optimization, publish or perish, random walk, revision control, Richard Stallman, rolodex, Ruby on Rails, Saturday Night Live, side project, slashdot, speech recognition, the scientific method, Therac-25, Turing complete, Turing machine, Turing test, type inference, Valgrind, web application

Seibel: So you want types mostly so the compiler can optimize better? Fitzpatrick: No. I also want it to blow up at compile time to tell me like, “You're doing something stupid.” Then sometimes I don't care and I want it to coerce for me at runtime and do whatever. I don't want to be too optimistic about Perl 6, but they're preaching a lot of things I want to see. But I don't think it'll ever come out. Seibel: Do you like C++? Fitzpatrick: I don't mind it. The syntax is terrible and totally inconsistent and the error messages, at least from GCC, are ridiculous. You can get 40 pages of error spew because you forgot some semicolon.

**
Code Complete (Developer Best Practices)
** by
Steve McConnell

Amazon: amazon.com — amazon.co.uk — amazon.de — amazon.fr

Ada Lovelace, Albert Einstein, Buckminster Fuller, call centre, choice architecture, continuous integration, data acquisition, database schema, don't repeat yourself, Donald Knuth, fault tolerance, Grace Hopper, haute cuisine, if you see hoof prints, think horses—not zebras, index card, inventory management, iterative process, Larry Wall, late fees, loose coupling, Menlo Park, Perl 6, place-making, premature optimization, revision control, Sapir-Whorf hypothesis, slashdot, sorting algorithm, statistical model, Tacoma Narrows Bridge, the scientific method, Thomas Kuhn: the structure of scientific revolutions, Turing machine, web application

Table 4-1 shows typical ratios of source statements in several high-level languages to the equivalent code in C. A higher ratio means that each line of code in the language listed accomplishes more than does each line of code in C. Table 4-1. Ratio of High-Level-Language Statements to Equivalent C Code Language Level Relative to C C 1 C++ 2.5 Fortran 95 2 Java 2.5 Perl 6 Python 6 Smalltalk 6 Microsoft Visual Basic 4.5 Source: Adapted from Estimating Software Costs (Jones 1998), Software Cost Estimation with Cocomo II (Boehm 2000), and "An Empirical Comparison of Seven Programming Languages" (Prechelt 2000). Some languages are better at expressing programming concepts than others.