[TYPES] semantic coherence for simply typed lambda-calculus

[Paolo Giarrusso]

On Thursday, 2 February 2017, Paul B Levy <P.B.Levy at cs.bham.ac.uk> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Dear all,
>
> Take simply typed lambda-calculus with ->, x, +, 0, 1 types.
> Specifically the Curry-style formulation with no type annotations
> whatsoever, neither on lambda nor on inl nor on anything else.
>
> Here are the two "coherence" statements I'm interested in.
>
> (1) Any two derivations of Gamma |- M : A have the same denotation.
>
> (2) More generally, for any bicartesian closed category C, any two
> derivations of Gamma |- M : A have the same denotation in C.
>

To double-check: Gamma, M and A are all fixed, right?

It seems one can remove the ambiguity in typing by normalizing M first and
then relying on the subformula property. Here's a potential proof
sketch—I'd love to know if this approach makes sense. (And I'm not even
sure if all the steps I'm relying on have actually been proven).

Use untyped normalization on M to obtain M'. Since M is typable,
normalization terminates—even untyped normalization (right?), since types
don't affect evaluation.
By preservation, M' should have the same type (even though it's untyped
evaluation, right?). By the subformula property of normalization, all types
in the derivation of M' are "subformulas" of A so there is no ambiguity in
its derivation of Gamma |- M' : A.* Let's call that derivation D.

Since normalization preserves the denotation, if we have two derivations D1
and D2 of Gamma |- M : A, we have that
[[ D1 ]] = [[ D ]] = [[ D2 ]]
hence we have (1) (and I expect (2) as well).

* I think this is not so trivial; however, this step is confirmed by the
theory of bidirectional typechecking. Quoting Dunfield and Krishnaswami
(2013):

> As shown by Watkins et al. (2004), bidirectional typechecking can be
understood in terms of the normalization of intuitionistic type theory, in
which normal forms correspond to the checking mode of bidirectional
typechecking, and neutral (or atomic) terms correspond to the synthesis
mode. This enables a proof of the elegant property that type annotations
are only necessary at reducible expressions, and that normal forms need no
annotations at all.

Dunfield and Krishnaswami (2013). Complete and Easy Bidirectional
Typechecking for Higher-Rank Polymorphism, ICFP 2013, ACM.


-- 
Paolo G. Giarrusso - Ph.D. Student, Tübingen University
*http://ps.informatik.uni-tuebingen.de/team/giarrusso/
<http://ps.informatik.uni-tuebingen.de/team/giarrusso/>*