Types and programming languages【2025|PDF|Epub|mobi|kindle电子书版本百度云盘下载】

Types and programming languagesPDF格式电子书版下载

注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具

1 Introduction1

1.1 Types in Computer Science1

1.2 What Type Systems Are Good For4

1.3 Type Systems and Language Design9

1.4 Capsule History10

1.5 Related Reading12

2 Mathematical Preliminaries15

2.1 Sets， Relations， and Functions15

2.2 Ordered Sets16

2.3 Sequences18

2.4 Induction19

2.5 Background Reading20

Ⅰ Untyped Systems21

3 Untyped Arithmetic Expressions23

3.1 Introduction23

3.2 Syntax26

3.3 Induction on Terms29

3.4 Semantic Styles32

3.5 Evaluation34

3.6 Notes43

4 An ML Implementation of Arithmetic Expressions45

4.1 Syntax46

4.2 Evaluation47

4.3 The Rest of the Story49

5 The Untyped Lambda-Calculus51

5.1 Basics52

5.2 Programming in the Lambda-Calculus58

5.3 Formalities68

5.4 Notes73

6 Nameless Representation of Terms75

6.1 Terms and Contexts76

6.2 Shifting and Substitution78

6.3 Evaluation80

7 An ML Implementation of the Lambda-Calculus83

7.1 Terms and Contexts83

7.2 Shifting and Substitution85

7.3 Evaluation87

7.4 Notes88

Ⅱ Simple Types89

8 Typed Arithmetic Expressions91

8.1 Types91

8.2 The Typing Relation92

8.3 Safety=Progress ＋ Preservation95

9 Simply Typed Lambda-Calculus99

9.1 Function Types99

9.2 The Typing Relation100

9.3 Properties of Typing104

9.4 The Curry-Howard Correspondence108

9.5 Erasure and Typability109

9.6 Curry-Style vs.Church-Style111

9.7 Notes111

10 An ML Implementation of Simple Types113

10.1 Contexts113

10.2 Terms and Types115

10.3 Typechecking115

11 Simple Extensions117

11.1 Base Types117

11.2 The Unit Type118

11.3 Derived Forms： Sequencing and Wildcards119

11.4 Ascription121

11.5 Let Bindings124

11.6 Pairs126

11.7 Tuples128

11.8 Records129

11.9 Sums132

11.10 Variants136

11.11 General Recursion142

11.12 Lists146

12 Normalization149

12.1 Normalization for Simple Types149

12.2 Notes152

13 References153

13.1 Introduction153

13.2 Typing159

13.3 Evaluation159

13.4 Store Typings162

13.5 Safety165

13.6 Notes170

14 Exceptions171

14.1 Raising Exceptions172

14.2 Handling Exceptions173

14.3 Exceptions Carrying Values175

Ⅲ Subtyping179

15 Subtyping181

15.1 Subsumption181

15.2 The Subtype Relation182

15.3 Properties of Subtyping and Typing188

15.4 The Top and Bottom Types191

15.5 Subtyping and Other Features193

15.6 Coercion Semantics for Subtyping200

15.7 Intersection and Union Types206

15.8 Notes207

16 Metatheory of Subtyping209

16.1 Algorithmic Subtyping210

16.2 Algorithmic Typing213

16.3 Joins and Meets218

16.4 Algorithmic Typing and the Bottom Type220

17 An ML Implementation of Subtyping221

17.1 Syntax221

17.2 Subtyping221

17.3 Typing222

18 Case Study： Imperative Objects225

18.1 What Is Object-Oriented Programming？225

18.2 Objects228

18.3 Object Generators229

18.4 Subtyping229

18.5 Grouping Instance Variables230

18.6 Simple Classes231

18.7 Adding Instance Variables233

18.8 Calling Superclass Methods234

18.9 Classes with Self234

18.10 Open Recursion through Self235

18.11 Open Recursion and Evaluation Order237

18.12 A More Efficient Implementation241

18.13 Recap244

18.14 Notes245

19 Case Study： Featherweight Java247

19.1 Introduction247

19.2 Overview249

19.3 Nominal and Structural Type Systems251

19.4 Definitions254

19.5 Properties261

19.6 Encodings vs.Primitive Objects262

19.7 Notes263

Ⅳ Recursive Types265

20 Recursive Types267

20.1 Examples268

20.2 Formalities275

20.3 Subtyping279

20.4 Notes279

21 Metatheory of Recursive Types281

21.1 Induction and Coinduction282

21.2 Finite and Infinite Types284

21.3 Subtyping286

21.4 A Digression on Transitivity288

21.5 Membership Checking290

21.6 More Efficient Algorithms295

21.7 Regular Trees298

21.8 μ-Types299

21.9 Counting Subexpressions304

21.10 Digression： An Exponential Algorithm309

21.11 Subtyping Iso-Recursive Types311

21.12 Notes312

V Polymorphism315

22 Type Reconstruction317

22.1 Type Variables and Substitutions317

22.2 Two Views of Type Variables319

22.3 Constraint-Based Typing321

22.4 Unification326

22.5 Principal Types329

22.6 Implicit Type Annotations330

22.7 Let-Polymorphism331

22.8 Notes336

23 Universal Types339

23.1 Motivation339

23.2 Varieties of Polymorphism340

23.3 System F341

23.4 Examples344

23.5 Basic Properties353

23.6 Erasure， Typability， and Type Reconstruction354

23.7 Erasure and Evaluation Order357

23.8 Fragments of System F358

23.9 Parametricity359

23.10 Impredicativity360

23.11 Notes361

24 Existential Types363

24.1 Motivation363

24.2 Data Abstraction with Existentials368

24.3 Encoding Existentials377

24.4 Notes379

25 An ML Implementation of System F381

25.1 Nameless Representation of Types381

25.2 Type Shifting and Substitution382

25.3 Terms383

25.4 Evaluation385

25.5 Typing386

26 Bounded Quantification389

26.1 Motivation389

26.2 Definitions391

26.3 Examples396

26.4 Safety400

26.5 Bounded Existential Types406

26.6 Notes408

27 Case Study： Imperative Objects， Redux411

28 Metatheory of Bounded Quantification417

28.1 Exposure417

28.2 Minimal Typing418

28.3 Subtyping in Kernel F〈：421

28.4 Subtyping in Full F〈：424

28.5 Undecidability of Full F〈：427

28.6 Joins and Meets432

28.7 Bounded Existentials435

28.8 Bounded Quantification and the Bottom Type436

Ⅵ Higher-Order Systems437

29 Type Operators and Kinding439

29.1 Intuitions440

29.2 Definitions445

30 Higher-Order Polymorphism449

30.1 Definitions449

30.2 Example450

30.3 Properties453

30.4 Fragments of Fω461

30.5 Going Further： Dependent Types462

31 Higher-Order Subtyping467

31.1 Intuitions467

31.2 Definitions469

31.3 Properties472

31.4 Notes472

32 Case Study： Purely Functional Objects475

32.1 Simple Objects475

32.2 Subtyping476

32.3 Bounded Quantification477

32.4 Interface Types479

32.5 Sending Messages to Objects480

32.6 Simple Classes481

32.7 Polymorphic Update482

32.8 Adding Instance Variables485

32.9 Classes with “Self”486

32.10 Notes488

Appendices491

A Solutions to Selected Exercises493

B Notational Conventions565

B.1 Metavariable Names565

B.2 Rule Naming Conventions565

B.3 Naming and Subscripting Conventions566

References567

Index605