[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Thursday, 2 February 2017, Paul B Levy <[email protected]> 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/>*
