# parametricity

2 messages
Open this post in threaded view
|

## parametricity

 Reynolds is stated as the inventor of parametricity. But it seems to me that thesame idea is stated quite clearly by Dijkstra in 1970 in this note:https://vanemden.wordpress.com/2018/10/29/history-of-structured-programming/#EWD288In addition, Dijkstra broaches the interesting idea that proofs ought to be constructedat the level of the flowchart first. Once that is done, using high level steps, it can berefined into code. But the proof of the code is essentially a refinement of the proof ofthe flowchart. This idea is interesting in that it is often the case that a flowchart mightsay "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 easierto prove than a low-level inductive proof of a program loop that implements the searchand involving issues such as finding invariants.To my mind, this "hierarchical proof technique" (my words, not Dijkstra's) is ratherinteresting.Tim _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Open this post in threaded view
|

## Re: parametricity

 I don't see where parametricity is stated in this note; you'll have to be morespecific.Reynolds credits Christopher Strachey for distinguishing ad hocand parametric polymorphism.  What Reynolds realized and proved is theparametricity theorem: every function in the polymorphic lambda calculus(and a few other type constructors) is parametric.  Giving a technicalformulation of this (related values of related types are mapped to relatedresults) is a major advance in our understanding of how to reason aboutprogramming languages as a whole and individual programs, too.  Amongother things, data abstraction (a concept Reynolds certainly did not invent)is a consequence of the parametricity theorem.  - FrankOn Wed, Nov 7, 2018 at 2:54 PM Tim Daly <[hidden email]> wrote:Reynolds is stated as the inventor of parametricity. But it seems to me that thesame idea is stated quite clearly by Dijkstra in 1970 in this note:https://vanemden.wordpress.com/2018/10/29/history-of-structured-programming/#EWD288In addition, Dijkstra broaches the interesting idea that proofs ought to be constructedat the level of the flowchart first. Once that is done, using high level steps, it can berefined into code. But the proof of the code is essentially a refinement of the proof ofthe flowchart. This idea is interesting in that it is often the case that a flowchart mightsay "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 easierto prove than a low-level inductive proof of a program loop that implements the searchand involving issues such as finding invariants.To my mind, this "hierarchical proof technique" (my words, not Dijkstra's) is ratherinteresting.Tim -- Frank Pfenning, ProfessorComputer Science DepartmentCarnegie Mellon UniversityPittsburgh, PA 15213-3891http://www.cs.cmu.edu/~fp+1 412 268-6343GHC 6017 _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer