History and Philosophy of types
summary
Survey of a century of concrete episodes: Russell and Church invent types as formal fixes for paradoxes; Algol 58 renames classes to data types; later theory models types as sets of values then as relations for effect systems that track reads/writes; TypeScript and Dart are explicitly unsound in practice; F# type providers make compilation depend on the internet; dependent types act as full specifications. Claims include Lakatos/Feyerabend-style argument that rigid formalization can hamper the growth of knowledge and that different research programmes keep incompatible core assumptions.
AI-written summary · about
chapters (27)
- 0:00Introduction
- 0:45What are types
- 1:25What are types good for
- 3:56Part 1 History
- 5:18Origins of types
- 6:58Base formulas
- 7:58Bertrand Russell Alonzo Church
- 9:47Algol 58
- 12:10McCarthy Hoare
- 13:44Mutation
- 14:19Effect systems
- 15:11Types as relations
- 16:52New programming languages
- 19:02Its doesnt matter
- 19:47Francis Bacon
- 21:33Paul Firewood
- 27:12Stretching
- 28:38Charles Hermit
- 29:29shudder of horror
- 30:11the method
- 31:57what can we do
- 33:25summary
- 36:08References
- 36:38General abstractions
- 38:38Interesting concepts
- 40:36Practical vs philosophical
- 44:32Philosophy of science
