[Haskell-cafe] use of models in proving program properties

[Ben Franksen]

This is something that has left me puzzled for years. My understanding
is that a model is a concrete realization of an abstract structure in
terms of some other mathematical structure, such that all the laws from
the first are satisfied in the latter. A simple example might be the
abstract (algebraic) structure "group" and a concrete realization e.g.
the integers with addition. Finding models for abstract theories is
certainly useful, for instance it shows that the theory is actually
'inhabited'; it may also shed light on the theory and give us ideas
about new theorems that might generalize to the abstract setting.

However, nobody would claim that from a theorem about integers I can
deduce one for abstract groups in general. But exactly this kind of
reasoning appears to be valid when proving things about e.g. the
polymorphic lambda calculus (aka System F).

For instance, in the famous "free theorems" paper by Wadler, the free
theorems appear as a consequence of modeling types in system F as
relations (this is most probably oversimplified, i can't remember the
details but I think they are not important here). The question is: How
can that imply anything about system F itself? Wouldn't it be necessary
to prove that these free theorems hold for /all/ models of System F, not
just one particular?

Besides, if such proofs using a suitable model are really valid, why
does it seem to be impossible to 'translate the proof back' from the
model to the original system and thus arrive at a direct proof?

I am sure there is something wrong with my understanding of these things
but I can't figure out what.

Cheers
Ben