Reynolds is stated as the inventor of parametricity. But it seems to me that the same idea is stated quite clearly by Dijkstra in 1970 in this note:https://vanemden.wordpress.com/2018/10/29/history-of-structured-programming/#EWD288 In addition, Dijkstra broaches the interesting idea that proofs ought to be constructed at the level of the flowchart first. Once that is done, using high level steps, it can be refined into code. But the proof of the code is essentially a refinement of the proof of the flowchart. This idea is interesting in that it is often the case that a flowchart might say "find the largest value such that...", which when reduced to code would involve a loop. A proof that the largest value exists at the abstract "flowchart" level would be easier to prove than a low-level inductive proof of a program loop that implements the search and involving issues such as finding invariants. To my mind, this "hierarchical proof technique" (my words, not Dijkstra's) is rather interesting. Tim _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
I don't see where parametricity is stated in this note; you'll have to be more specific. Reynolds credits Christopher Strachey for distinguishing ad hoc and parametric polymorphism. What Reynolds realized and proved is the parametricity theorem: every function in the polymorphic lambda calculus (and a few other type constructors) is parametric. Giving a technical formulation of this (related values of related types are mapped to related results) is a major advance in our understanding of how to reason about programming languages as a whole and individual programs, too. Among other things, data abstraction (a concept Reynolds certainly did not invent) is a consequence of the parametricity theorem. - Frank On Wed, Nov 7, 2018 at 2:54 PM Tim Daly <[hidden email]> wrote:
Frank Pfenning, Professor Computer Science Department Carnegie Mellon University Pittsburgh, PA 15213-3891 +1 412 268-6343 GHC 6017 _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Free forum by Nabble | Edit this page |