Well-going programs can be typed
The abstract:
Our idiomatically objectionable title is a pun on Milner's ``well-typed programs do not go wrong' --- because we provide a completeness result for type-checking rather than a soundness result.
We show that the well-behaved functions of untyped PCF are already expressible in typed PCF: any equivalence class of the partial logical equivalence generated from the flat natural numbers in the model given by PCF's operational semantics is inhabited by a well-typed term.
Its got Scott's $D_{\infty}$, PCF, Retractions, PERs, Logical Relations, . . .
And yet the paper itself is 50% tricks with Haskell type classes and GHC extensions.
I think the title is extremely misleading, at least based on my interpretation of the abstract. I thought the title meant: "if your untyped PCF program is well-behaved, then there is some way to add type annotations to yield a well-typed program (presumably with the same behavior)." But abstract semes to really be saying that if you have a well-behaved function, then there is some well-typed function with extensionally equivalent behavior; note the lack of constraint on the form of the typed program text and its relation to the untyped text.
