Impredicative encoding of functions. Using an impredicative encoding, the function type α→β can be alternatively represented as the continuation passing style ∀κ, (β→κ)→(α→κ). I give a Coq proof that, assuming parametricity (and functional extensionality), both types are indeed isomorphic.

gistfile1.coq

Definition compose {A B C:Type} (f:A->B) (g:B->C) : A->C := fun x => g (f x).
Arguments compose {A B C} f g x /.
Notation "g ∘ f" := (compose f g) (at level 3, left associativity).

Definition id {A:Type} : A -> A := fun x => x.
Arguments id {A} x /.


(** The impredicative encoding of functions. There is a bit of
    cheating as it is not actually an impredicative
    quantification. But it is fine for the purpose of this
    demonstration. *)
Definition Fun_i (A B:Type) : Type := forall R, (B->R)->A->R.

Definition encode (A B:Type) (f:A->B) : Fun_i A B :=
  fun R k a => k (f a)
.

Definition decode (A B:Type) (f:Fun_i A B) : A -> B :=
  f B (fun x => x)
.

Lemma the_function_space_is_a_retract_of_the_impredicative_encoding (A B:Type) :
  forall f, decode A B (encode A B f) = f.
Proof.
  intros f.
  reflexivity.
Qed.


(** In order to prove that the other composition is also the identity,
    βη does not suffice: we need parametricity. We assume that the
    type [Fun_i A B] is indeed parametric, i.e. that every function is
    related to itself by the relation [RFun_i A B]. The definition of
    [RFun_i A B] follows the structure of [Fun_i A B]. See Philip
    Wadler's Theorems for free! for further documentation. *)

(** Relations *)
Notation "A ⇔ B" := (A->B->Prop) (at level 70).

Definition RFun {A₁ A₂ B₁ B₂:Type} (RA:A₁⇔A₂) (RB:B₁⇔B₂) : (A₁->B₁)⇔(A₂->B₂) :=
  fun f g => forall x y, RA x y -> RB (f x) (g y)
.
Arguments RFun {A₁ A₂ B₁ B₂} RA RB f g /.
Notation "RA ⟶ RB" := (RFun RA RB) (at level 70, right associativity).

Definition RForall {B₁:Type->Type} {B₂:Type->Type}
   (RB:forall (A₁ A₂:Type) (R:A₁⇔A₂), B₁ A₁⇔B₂ A₂) : (forall x, B₁ x) ⇔ (forall x, B₂ x) :=
  fun f g => forall (A₁ A₂:Type) (RA:A₁⇔A₂), RB A₁ A₂ RA (f A₁) (g A₂)
.

Notation "∀ ( R : A₁ ⇔ A₂ ) , RB" := (RForall (fun A₁ A₂ R => RB)) (at level 90, R ident, A₁ ident, A₂ ident).

Definition RFun_i {A₁ A₂ B₁ B₂:Type} (RA:A₁⇔A₂) (RB:B₁⇔B₂) : Fun_i A₁ B₁ ⇔ Fun_i A₂ B₂ :=
  ∀ (R:U⇔V), (RB ⟶ R) ⟶ RA ⟶ R
.
Eval compute in @RFun_i.
(* … => forall (U V : Type) (R : U ⇔ V),
         forall (k₁ : B₁ -> U) (k₂ : B₂ -> V),
          (forall (s : B₁) (t : B₂), RB s t -> R (k₁ s) (k₂ t)) ->
          forall (x : A₁) (y : A₂), RA x y -> R (f U k₁ x) (g V k₂ y) *)

Axiom Fun_i_parametric : forall {A₁ A₂ B₁ B₂:Type} (RA:A₁⇔A₂) (RB:B₁⇔B₂),
  forall (f:Fun_i A₁ B₁) (g:Fun_i A₂ B₂), RFun_i RA RB f g.


(** The relations we will need are all graphs of functions. *)
Definition Graph {A B:Type} (f:A->B) : A⇔B := fun x y => f x = y.
Arguments Graph {A B} f x y /.

Lemma the_impredicative_encoding_is_a_retract_of_the_function_space (A B:Type) :
  forall f R k x, encode A B (decode A B f) R k x = f R k x.
Proof.
  intros f R k x.
  compute.
  (** specializes the parametricity lemma to graphs. *)
  generalize (fun (g:A->A) (h:B->B) (U V:Type) (i:U->V) =>
                Fun_i_parametric (Graph g) (Graph h) f f U V (Graph i)
             ); intros p; simpl in p.
  apply (p id id).
  + intros ** <-; reflexivity.
  + reflexivity.
Qed.


(** Up to functional extensionality, we hence have that [encode A B]
    and [decode A B] form an isomorphism. *)
Require Import Coq.Logic.FunctionalExtensionality.


Theorem impredicative_encoding_isomorphic (A B:Type) :
  (decode A B) ∘ (encode A B) = id /\ (encode A B) ∘ (decode A B) = id.
Proof.
  split.
  + extensionality f; simpl.
    apply the_function_space_is_a_retract_of_the_impredicative_encoding.
  + extensionality f; simpl.
    extensionality R; extensionality k; extensionality x.
    apply the_impredicative_encoding_is_a_retract_of_the_function_space.
Qed.

Print Assumptions impredicative_encoding_isomorphic.
(* Axioms:
     Fun_i_parametric
     functional_extensionality_dep *)