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 <axiom...@gmail.com> wrote: > 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 > > -- Frank Pfenning, Professor Computer Science Department Carnegie Mellon University Pittsburgh, PA 15213-3891 http://www.cs.cmu.edu/~fp +1 412 268-6343 GHC 6017
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
