8 results back to index

pages: 496 words: 174,084

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

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

This time, though, I’ve done a better job of involving the community in the incremental redesign process. 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. Some people will think that’s revolutionary.

…

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.

pages: 834 words: 180,700

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

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, MITM: man-in-the-middle, 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

His personal home page is http://www.pubbitch.org/. 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. He is a senior developer at VisTrails, Inc. He also holds a Research Assistant Professor appointment with the Polytechnic Institute of New York University.

…

We often completed an entire Design-Development-QA feedback cycle within a 24-hour day, with each aspect taking one person's 8-hour work day in their local daytime. 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. Furthermore, we pre-emptively resolved disputes by actually coding up alternatives to explore the design space, and were not afraid of replacing fully-working prototypes when a better design arrived.

…

Furthermore, we pre-emptively resolved disputes by actually coding up alternatives to explore the design space, and were not afraid of replacing fully-working prototypes when a better design arrived. 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.

pages: 525 words: 149,886

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

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

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. Similarly, we, as Perl programmers, have been writing C programs in Perl whether we meant o or not.

…

The cost of this is that the iterator has to remember a list of all the values it has ever produced, in case someone tells it to start over. It also complicates the programming. 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 first syntax is an object method call, so we need to make our iterators into Perl objects.

pages: 266 words: 79,297

**
Forge Your Future with Open Source
** by
VM (Vicky) Brasseur

AGPL, anti-pattern, Benevolent Dictator For Life (BDFL), call centre, continuous integration, Debian, DevOps, don't repeat yourself, en.wikipedia.org, Firefox, Guido van Rossum, Internet Archive, Larry Wall, microservices, Perl 6, premature optimization, pull request, Richard Stallman, risk tolerance, Turing machine

Use this chapter as a guideline, but always follow the established communication norms for the project. Now that you know how to communicate with others in a FOSS community, it’s time to get to know them, and what better way to do that than getting together in person? Footnotes [92] https://en.wikipedia.org/wiki/Linus_Torvalds; The inventor of Linux. [93] https://en.wikipedia.org/wiki/Larry_Wall; The inventor of rn, patch, Perl, and Perl 6. [94] https://en.wikipedia.org/wiki/Tim_Berners-Lee; The inventor of the World Wide Web. [95] https://en.wikipedia.org/wiki/Pastebin [96] https://www.xkcd.com/386/ [97] https://opensource.com/life/16/6/irc Copyright © 2018, The Pragmatic Bookshelf. Chapter 8 It’s About the People By now you’ve noticed a large part of the book is dedicated to methods and tips for interacting with others.

pages: 647 words: 43,757

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

Albert Einstein, combinatorial explosion, experimental subject, finite state, Henri Poincaré, Perl 6, Russell's paradox, sorting algorithm, Turing complete, Turing machine, type inference, Y Combinator

., 461 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 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 * * * * * * Index G 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 * * * * * * Index H 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 * * * * * * Index I 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 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 * * * * * * Index J 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 joinsub implementation, 218–220 judgment, 36 * * * * * * Index K KEA, 226 kernel F<:, 391 kinding, 439–447, 459 kinds dependent, 445 power, 445 row, 445 singleton, 445 Knaster-Tarski fixed point theorem, 283 * * * * * * Index L λ-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 lambda-calculus 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 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 * * * * * * Index M μ, 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 v, 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 * * * * * * Index O 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 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 * * * * * * Index P 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 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 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 * * * * * * Index Q qualified types, 338 quantification, see polymorphism Quest, 11, 409 * * * * * * Index R 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 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 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 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 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 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 * * * * * * Index S 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 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 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 ML implementation, 381-387 System Fω, 449-466 and higher-order logic, 109 fragments, 461 System , 467-473 System F<:, 389-409 kernel and full variants, 391 System λω, 445-447 * * * * * * Index T 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 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 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 * * * * * * Index U 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 * * * * * * Index V 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 * * * * * * Index W 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 well-founded order, 18 set, 18 well-typed term, 93 width subtyping, 183 wildcard bindings, 119-121 witness type, 364 wrong, 42, 73 * * * * * * Index X XML, 9, 207, 313 * * * * * * Index Y Y combinator, 65 Year 2000 problem, 9 * * * * * * Index Z Z combinator, 65 * * * * * * List of Figures Preface Figure P-1: Chapter Dependencies Figure P-2: Sample Syllabus for an Advanced Graduate Course Chapter 1: Introduction Figure 1-1: Capsule History of Types in Computer Science and Logic Chapter 3: Untyped Arithmetic Expressions Figure 3-1: Booleans (B) Figure 3-2: Arithmetic Expressions (NB) Chapter 5: The Untyped Lambda-Calculus Figure 5-1: The Predecessor Function's "Inner Loop" Figure 5-2: Evaluation of factorial c3 Figure 5-3: Untyped Lambda-Calculus (λ) Chapter 8: Typed Arithmetic Expressions Figure 8-1: Typing Rules for Booleans (B) Figure 8-2: Typing Rules for Numbers (NB) Chapter 9: Simply Typed Lambda-Calculus Figure 9-1: Pure Simply Typed Lambda-Calculus (λ→) Chapter 11: Simple Extensions Figure 11-1: Uninterpreted Base Types Figure 11-2: Unit Type Figure 11-3: Ascription Figure 11-4: Let Binding Figure 11-5: Pairs Figure 11-6: Tuples Figure 11-7: Records Figure 11-8: (Untyped) Record Patterns Figure 11-9: Sums Figure 11-10: Sums (With Unique Typing) Figure 11-11: Variants Figure 11-12: General Recursion Figure 11-13: Lists Chapter 13: References Figure 13-1: References Chapter 14: Exceptions Figure 14-1: Errors Figure 14-2: Error Handling Figure 14-3: Exceptions Carrying Values Chapter 15: Subtyping Figure 15-1: Simply Typed Lambda-Calculus with Subtyping (λ<:) Figure 15-2: Records (Same as Figure 11-7) Figure 15-3: Records and Subtyping Figure 15-4: Bottom Type Figure 15-5: Variants and Subtyping Chapter 16: Metatheory of Subtyping Figure 16-1: Subtype Relation with Records (Compact Version) Figure 16-2: Algorithmic Subtyping Figure 16-3: Algorithmic Typing Chapter 19: Case Study: Featherweight Java Figure 19-1: Featherweight Java (Syntax and Subtyping) Figure 19-2: Featherweight Java (Auxiliary Definitions) Figure 19-3: Featherweight Java (Evaluation) Figure 19-4: Featherweight Java (Typing) Chapter 20: Recursive Types Figure 20-1: Iso-Recursive Types (λμ) Chapter 21: Metatheory of Recursive Types Figure 21-1: Sample Tree Types.

…

., 461 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 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 * * * * * * Index G 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 * * * * * * Index H 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 * * * * * * Index I 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 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 * * * * * * Index J 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 joinsub implementation, 218–220 judgment, 36 * * * * * * Index K KEA, 226 kernel F<:, 391 kinding, 439–447, 459 kinds dependent, 445 power, 445 row, 445 singleton, 445 Knaster-Tarski fixed point theorem, 283 * * * * * * Index L λ-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 lambda-calculus 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 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 * * * * * * Index M μ, 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 v, 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 * * * * * * Index O 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 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 * * * * * * Index P 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 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 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 * * * * * * Index Q qualified types, 338 quantification, see polymorphism Quest, 11, 409 * * * * * * Index R 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 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 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 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 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 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 * * * * * * Index S 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 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 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 ML implementation, 381-387 System Fω, 449-466 and higher-order logic, 109 fragments, 461 System , 467-473 System F<:, 389-409 kernel and full variants, 391 System λω, 445-447 * * * * * * Index T 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 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 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 * * * * * * Index U 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 * * * * * * Index V 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 * * * * * * Index W 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 well-founded order, 18 set, 18 well-typed term, 93 width subtyping, 183 wildcard bindings, 119-121 witness type, 364 wrong, 42, 73 * * * * * * Index X XML, 9, 207, 313 * * * * * * Index Y Y combinator, 65 Year 2000 problem, 9 * * * * * * Index Z Z combinator, 65 * * * * * * List of Figures Preface Figure P-1: Chapter Dependencies Figure P-2: Sample Syllabus for an Advanced Graduate Course Chapter 1: Introduction Figure 1-1: Capsule History of Types in Computer Science and Logic Chapter 3: Untyped Arithmetic Expressions Figure 3-1: Booleans (B) Figure 3-2: Arithmetic Expressions (NB) Chapter 5: The Untyped Lambda-Calculus Figure 5-1: The Predecessor Function's "Inner Loop" Figure 5-2: Evaluation of factorial c3 Figure 5-3: Untyped Lambda-Calculus (λ) Chapter 8: Typed Arithmetic Expressions Figure 8-1: Typing Rules for Booleans (B) Figure 8-2: Typing Rules for Numbers (NB) Chapter 9: Simply Typed Lambda-Calculus Figure 9-1: Pure Simply Typed Lambda-Calculus (λ→) Chapter 11: Simple Extensions Figure 11-1: Uninterpreted Base Types Figure 11-2: Unit Type Figure 11-3: Ascription Figure 11-4: Let Binding Figure 11-5: Pairs Figure 11-6: Tuples Figure 11-7: Records Figure 11-8: (Untyped) Record Patterns Figure 11-9: Sums Figure 11-10: Sums (With Unique Typing) Figure 11-11: Variants Figure 11-12: General Recursion Figure 11-13: Lists Chapter 13: References Figure 13-1: References Chapter 14: Exceptions Figure 14-1: Errors Figure 14-2: Error Handling Figure 14-3: Exceptions Carrying Values Chapter 15: Subtyping Figure 15-1: Simply Typed Lambda-Calculus with Subtyping (λ<:) Figure 15-2: Records (Same as Figure 11-7) Figure 15-3: Records and Subtyping Figure 15-4: Bottom Type Figure 15-5: Variants and Subtyping Chapter 16: Metatheory of Subtyping Figure 16-1: Subtype Relation with Records (Compact Version) Figure 16-2: Algorithmic Subtyping Figure 16-3: Algorithmic Typing Chapter 19: Case Study: Featherweight Java Figure 19-1: Featherweight Java (Syntax and Subtyping) Figure 19-2: Featherweight Java (Auxiliary Definitions) Figure 19-3: Featherweight Java (Evaluation) Figure 19-4: Featherweight Java (Typing) Chapter 20: Recursive Types Figure 20-1: Iso-Recursive Types (λμ) Chapter 21: Metatheory of Recursive Types Figure 21-1: Sample Tree Types.

pages: 309 words: 65,118

**
Ruby by example: concepts and code
** by
Kevin C. Baird

Benevolent Dictator For Life (BDFL), David Heinemeier Hansson, Debian, digital map, Donald Knuth, en.wikipedia.org, Firefox, fudge factor, general-purpose programming language, Guido van Rossum, Larry Wall, MVC pattern, Paul Graham, Perl 6, premature optimization, union organizing, web application

Haskell is a purely functional language designed by committee and released in 1998. It has several fascinating features, most notably lazy evaluation, whereby the value of a given piece of data does not need to be known (or even meaningful) until it needs to be used. This allows a programmer to define things in terms of infinite series, such as the set of all integers. Haskell is the language used for Pugs, an implementation of the new Perl 6 language, which some people think is drawing more attention to Haskell than to Perl itself. Haskell has an interactive environment similar to Ruby’s irb, but it doesn’t allow function definitions except in external files that are imported, whereas irb allows full definitions for classes, methods, and functions. Like C, Haskell has both strong and static typing. Haskell is an excellent language that’s very suitable for teaching purely functional techniques, as well as general-purpose programming.

pages: 1,201 words: 233,519

**
Coders at Work
** by
Peter Seibel

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

I would like to give the runtime hints in certain parts of the code and declare types. But if I want to be lazy and mock something out, I want to write in that style. 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. But—like anything else—you quickly memorize all the patterns. You don't even read the words; you just see the structure and think, “Oh, yeah, I probably forgot to close the namespace in a header file.”

pages: 1,758 words: 342,766

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

Ada Lovelace, Albert Einstein, Buckminster Fuller, call centre, 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, 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

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 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). C 1 C++ 2.5 Fortran 95 2 Java 2.5 Perl 6 Python 6 Smalltalk 6 Microsoft Visual Basic 4.5 Some languages are better at expressing programming concepts than others. You can draw a parallel between natural languages such as English and programming languages such as Java and C++. In the case of natural languages, the linguists Sapir and Whorf hypothesize a relationship between the expressive power of a language and the ability to think certain thoughts.