Types and Programming Languages

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