Problems Posed By Types
WIP
Program : Type :: Solution : Problem
Problematic
What is a problem?
problem (n.)
late 14c., “a difficult question proposed for solution,” from Old French problème (14c.) and directly from Latin problema, from Greek problema “a task, that which is proposed, a question;” also “anything projecting, headland, promontory; fence, barrier;” also “a problem in geometry,” literally “thing put forward,” from proballein “propose,” from pro “forward” (from PIE root *per- (1) “forward”) + ballein “to throw” (from PIE root *gwele- “to throw, reach”).
The prevailing view on programming with types
The prevailing view1 on the meaning and purpose of types in programming can be gleaned from excerpts like the following
The main purpose of a type system is to reduce possibilities for bugs in computer programs by defining interfaces between different parts of a computer program, and then checking that the parts have been connected in a consistent way.
Types in programming languages are valuable but not essential. Two programming languages can be quite similar except for the use of types—for example, C and BCPL, or ML and Lisp. Programming languages use type checking to catch errors at compile time and to improve run-time efficiency.
Constructivism
Euclid
Spinoza
Construct objects.
Kant
Synthetic a priori.
Bishop
Constructive sets.
Martin-Lof
Types as problems, programs as solutions.
Precedent
- Martin Lof’s paper
- Types as problems
- Ref CTT and Harper’s lectures thereon
Implications
- As specifying and sharing requirements
- Precisely constructable specifications
- Think of a mockup as the “shell of a type”, the type which actually articulates the problem to solve should fill the form sketched by the mock up.
Example
type t : data platform * repo -> repo type fetch : data platform * (filter * data platform -> data) -> data disk type commit : repo * data disk -> repo
References
Footnotes:
Or, at least, “a very prominent view”.