Sites Inria

Version française

Project-Team Séminars

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible

© INRIA Sophie Auvin - P comme Protocole

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible

  • Date : 12/12/2017
  • Place : INRIA - Paris - 2 rue Simone Iff - Salle Lions 2, bâtiment C
  • Guest(s) : William J. Bowman, Northeastern University
  • Organiser(s) : Marco Stronati

Dependently typed languages like Coq are used to specify and prove functional correctness of source programs.  By preserving dependent types through each compiler pass, we could preserve these  specifications and correctness proofs into the generated  target-language programs.  Unfortunately, in 2002 Barthe and Uustalu proved that type-preserving CPS is not possible for languages like Coq.  Specifically, they showed that for strong dependent pairs (Σ types), the standard typed call-by-name CPS is not type-preserving.  

They further proved that for dependent case analysis on sums, a class  of CPS translations---including the standard translation is not  possible.  In 2016, Morrisett noticed that the same problem arises in the standard call-by value CPS translation for dependent functions (Π) types).  In essence, the problem is that the standard typed CPS translation by double-negation, in which computations are assigned types of the form (A → ⊥) → ⊥, disrupts the term/type equivalence that is used during type-checking in a dependently typed language.

In this paper, we prove that type-preserving CPS translation for dependently typed languages is not not possible. We develop both call-by-name and call-by-value CPS translations from the Calculus of Constructions with both (Π) and (Σ) types (CC) to a dependently typed target language, and prove type preservation and compiler correctness of each translation.  Our target language is CC extended with an additional equivalence rule and an additional typing rule, which we prove consistent by giving a model in the extensional Calculus of Constructions.  Our key observation is that we can use a CPS translation that employs answer-type polymorphism, where CPS-translated computations have type ∀α. (A → α) → α.  This type justifies, by a free theorem, the new equality rule in our target language and allows us to recover the term/type equivalences that CPS translation disrupts.  Finally, we conjecture that our translation extends to dependent case analysis on sums, despite the impossibility result, and provide a proof sketch.

Keywords: Project-Team Prosecco Seminar Inria de Paris