parametricity

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

parametricity

Tim Daly
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
Reply | Threaded
Open this post in threaded view
|

Re: parametricity

Frank Pfenning
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:
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

+1 412 268-6343
GHC 6017


_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer