Types and Programming Languages

range of a relation, 16

rank-2 polymorphism, 359

raw type, 248

rcdsub implementation, 181–224

reachable_F, 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