[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] parametricity

From: Frank Pfenning
Subject: Re: [Axiom-developer] parametricity
Date: Wed, 7 Nov 2018 20:18:33 -0500

I don't see where parametricity is stated in this note; you'll have to be more

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 <address@hidden> 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:

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


Frank Pfenning, Professor
Computer Science Department
Carnegie Mellon University
Pittsburgh, PA 15213-3891

+1 412 268-6343
GHC 6017

reply via email to

[Prev in Thread] Current Thread [Next in Thread]