Church-Encoded Pairs are not Categorical Products

Recently, John Altidor a PhD student from the University of Massachusetts has been visting UIowa. His research as of right now is concerned with subtyping. While his work can be applied to a wide range of programming languages he and his advisor have been applying their work to Java. Lately, he and I have been talking a lot about his work on subtyping. As I said, he has been applying his work to Java, and one thing I find interesting is thinking about how much of OO can be done in a dependent type theory. His work sparked me to read a few papers on subtyping. One such paper is “An extension of system F with subtyping” by L. Cardelli et al. In this paper the authors claim something I was not aware of. They state that church-encoded pairs in system F do not correspond to actual categorical constructs. Now this is not saying that they are unsound, but it is saying that they are not products. It is important to note that this claim is with respect to \(\beta\eta\)-equality. I am not sure, but it may be possible to show that church-encoded pairs can be identified with products using some other notation of equality. The authors claim this is well-known and do not give the details. Curiosity has lead me to filling in the details myself.

I plan to present the details of this claim in a three part post. First, I will set the stage by defining system F with \(\beta\eta\)-equality and church-encoded pairs. In the second post I will present all the categorical notions we will need on the journey. Finally, in the third post I will present the main results. The entirety of this series will be presented and formalized in Coq. I assume the reader is familier with Coq and the locally nameless binding representation. However, for the uninitiated I give plenty of references.

System F was invented independently by both J. Girard and J. Reynolds. It is the extension of the simply typed \(\lambda\)-calculus with second order universal quantification. For a more in depth look at system F see the amazing book “Proofs and Types.” I start by defining the syntax. The syntax for types and terms are defined by the following inductive definitions. Note that I will not be able to give every detail of the formalization, however in the final post I will provide a link to the entire formalization.

Inductive typ : Set := 
  | typ_base 
  | typ_fvar   (n:nat)
  | typ_bvar   (n:nat)
  | typ_forall (A:typ)
  | typ_arrow  (A1:typ) (A2:typ).

Inductive trm : Set :=
  | trm_bvar  (n:nat)
  | trm_fvar  (n:nat)
  | trm_lam   (A:typ) (b:trm)
  | trm_Lam   (b:trm)
  | trm_app   (a:trm) (b:trm)
  | trm_tapp  (a:trm) (T:typ)
  | trm_c.

There are a few things that must be said before moving on. I am using the locally nameless representation for binders. See this for more information on that. System F has the types, typ_bvar _ bound variables, typ_fvar _ free variables, typ_base a base type, typ_forall _ the universal type, and typ_arrow _ _ implication (or the function type). Now terms are made up of bound variables trm_bvar _, free variables trm_fvar _, \(\lambda\)-abstractions trm_lam _ _, type abstractions trm_Lam _, applications trm_app _ _, type applications trm_tapp _ _, and a constant trm_c.

The syntax for terms and types allow for the definition of non-well-formed types and terms. An example of a non-well-formed type is typ_bvar 0. This type contains an unbound bound variable. Another example is typ_arrow (typ_bvar 0) (typ_fvar 0) which also contains an unbound bound variable. A similar game can be played using terms. A type or a term is well-formed iff all bound variables are bound. Well-formed types and terms are characterized by the following two predicates.

Inductive lc_T : typ -> Prop :=
  | lcT_base : lc_T typ_base

  | lcT_fvar : forall n, lc_T (typ_fvar n)

  | lcT_arrow : forall a b,
    lc_T a ->
    lc_T b ->
    lc_T (typ_arrow a b)

  | lcT_forall : forall t L,
    (forall x, ~(In x L) -> lc_T (open_T 0 (typ_fvar x) t)) ->
    lc_T (typ_forall t).

Inductive lc : trm -> Prop :=
  | lc_fvar : forall n, lc (trm_fvar n)

  | lc_lam : forall L t A, 
    lc_T A ->
    (forall x, ~(In x L) -> lc (open_t 0 (trm_fvar x) t)) ->
    lc (trm_lam A t)

  | lc_Lam : forall t,
    lc t ->
    lc (trm_Lam t)

  | lc_app : forall t1 t2,
    lc t1 ->
    lc t2 ->
    lc (trm_app t1 t2)

  | lc_tapp : forall T t,
    lc_T T ->
    lc t ->
    lc (trm_tapp t T)

  | lc_c : lc trm_c.

A type T or a term t is called locally closed iff lc_T T and lc_t t are true. Both of these definitions depend on two functions called open_T (n:nat) (t:typ) (t':typ) : typ and open_t (n:nat) (t:trm) (t':trm) : trm. The former replaces all bound variables typ_bvar n with the type t in t'. The latter does the same with respect to terms. There is also a third function we will see open_tT (n:nat) (t:typ) (t':trm) : trm which replaces all bound type variables typ_bvar n with the type t in the term t'.

The definition of full \(\beta\eta\)-reduction is next. This is the standard definition so I do not comment on it. The reflexive and transitive closure of this relation is denoted by t1 ~*> t2.

Inductive step_t : trm -> trm -> Prop :=
  | ST_lam : forall A q q' L,
    lc_T A ->
    (forall y, 
      ~ In y L -> 
      exists q'', open_t 0 (trm_fvar y) q ~> q'' /\ q' = close_t 0 y q'') -> 
    (trm_lam A q) ~> (trm_lam A q')

  | ST_Lam : forall t t',
    t ~> t' ->
    (trm_Lam t) ~> (trm_Lam t')

  | ST_beta : forall T t1 t2,
    lc (trm_lam T t1) -> 
    lc t2 ->
    (trm_app (trm_lam T t1) t2) ~> (open_t 0 t2 t1)

  | ST_eta : forall t T,
    lc t ->
    (trm_lam T (trm_app t (trm_bvar 0))) ~> t

  | ST_type : forall t T,
    lc t ->
    lc_T T ->
    (trm_tapp (trm_Lam t) T) ~> (open_tT 0 T t)

  | ST_app1 : forall t1 t1' t2,
    lc t2 ->
    t1 ~> t1' ->
    trm_app t1 t2 ~> trm_app t1' t2

  | ST_app2 : forall t1 t2 t2',
    lc t1 ->
    t2 ~> t2' ->
    trm_app t1 t2 ~> trm_app t1 t2'

  | ST_tapp : forall t t' T, 
    lc_T T ->
    t ~> t' ->
    trm_tapp t T ~> trm_tapp t' T
where "t1 '~>' t2" := (step_t t1 t2).

The standard definition of typing for church-style system F goes something like the following; where context is defined to be List (nat*typ). In fact all names are nats. The proposition Ok G where G:context states that contexts are well-formed, which means that all variables in the domain of G are distinct.

Inductive type_check (G:context) : trm -> typ -> Prop :=
  | T_Var : forall T x,
    Ok G -> In (x,T) G ->
    type_check G (trm_fvar x) T

  | T_Lam : forall L t T1 T2,
    (forall (x:nat),
      ~ (In x L) ->
      type_check ((x,T1) :: G) (open_t 0 (trm_fvar x) t) T2) ->
    type_check G (trm_lam T1 t) (typ_arrow T1 T2)

  | T_TLam : forall L t T,
    (forall (x:nat),
      ~ (In x L) ->
      type_check G (open_tT 0 (typ_fvar x) t) (open_T 0 (typ_fvar x) T)) ->
    type_check G (trm_Lam t) (typ_forall T)

  | T_App : forall T1 T2 t1 t2,
    type_check G t1 (typ_arrow T1 T2) ->
    type_check G t2 T1 ->
    type_check G (trm_app t1 t2) T2

  | T_AppT : forall t T T' A,
    lc_T T' ->
    type_check G t (typ_forall T) ->
    (open_T 0 T' T) = A ->
    type_check G (trm_tapp t T') A

  | T_C :
    Ok G ->
    type_check G trm_c typ_base
where "G :> t ; T" := (type_check G t T).

Finally, I define \(\beta\eta\)-equality. This definition is rather long and tedious. If the reader would like a clearer picture see page 8 of Cardelli's paper cited above. There Cardelli gives the definition for \(\beta\eta\)-equality for system F with subtyping which the following definition is based.

Inductive trm_eq (G:context) : trm -> trm -> typ -> Prop :=
  | Eq_var :  forall n T, 
    G :> (trm_fvar n) ; T -> 
    G :> (trm_fvar n) <~> (trm_fvar n) ; T

  | Eq_lam : forall L t1 t2 T1 T2,
    (forall (x:nat),
     ~ (In x L) ->
     ((x,T1) :: G) :> (open_t 0 (trm_fvar x) t1) <~> (open_t 0 (trm_fvar x) t2) ; T2) ->
    G :> (trm_lam T1 t1) <~> (trm_lam T1 t2) ; (typ_arrow T1 T2)

  | Eq_tlam : forall L t1 t2 T,
    (forall (n:nat),
      ~ In n L ->
      G :> (open_tT 0 (typ_fvar n) t1) <~> (open_tT 0 (typ_fvar n) t2) ; (open_T 0 (typ_fvar n) T)) ->
    G :> (trm_Lam t1) <~> (trm_Lam t2) ; (typ_forall T)

  | Eq_app : forall a a' b b' A B,
    G :> a <~> a' ; typ_arrow A B ->
    G :> b <~> b' ; A ->
    G :> (trm_app a b) <~> (trm_app a' b') ; B
  | Eq_tapp : forall a a' A B C,
    lc_T B ->
    G :> a <~> a' ; typ_forall A ->
    C = (open_T 0 B A) ->
    G :> (trm_tapp a B) <~> (trm_tapp a' B) ; C

  | Eq_beta : forall L a a' b b' c A B,
    (forall (x:nat),
      ~ (In x L) ->
      ((x,A) :: G) :> (open_t 0 (trm_fvar x) b) <~> (open_t 0 (trm_fvar x) b') ; B) ->
    G :> a <~> a' ; A ->
    c = (open_t 0 a' b') -> 
    G :> (trm_app (trm_lam A b) a) <~>  c ; B 

  | Eq_tbeta : forall L a b c A B C,
    lc_T B ->
    (forall (n:nat),
      ~ In n L ->
      G :> (open_tT 0 (typ_fvar n) a) <~> (open_tT 0 (typ_fvar n) b) ; (open_T 0 (typ_fvar n) A)) ->
    c = open_tT 0 B b -> 
    C = open_T 0 B A ->
    G :> (trm_tapp (trm_Lam a) B) <~>  c ; C

  | Eq_eta : forall b b' A B,
    G :> b <~> b' ; typ_arrow A B ->
    G :> (trm_lam A (trm_app b (trm_bvar 0))) <~> b' ; typ_arrow A B
  | Eq_teta : forall b b' A,
    G :> b <~> b' ; typ_forall A ->
    G :> (trm_Lam (trm_tapp b (typ_fvar 0))) <~> b' ; typ_forall A

  | Eq_sym : forall t1 t2 T, 
    G :> t2 <~> t1 ; T -> 
    G :> t1 <~> t2 ; T 

  | Eq_trans : forall t1 t2 t3 T,  
    G :> t1 <~> t3 ; T ->  
    G :> t3 <~> t2 ; T -> G :> t1 <~> t2 ; T 
where "G :> t1 <~> t2 ; T" := (trm_eq G t1 t2 T).

This concludes the definition of system F with \(\beta\eta\)-equality. The next step is to define the church encoding of pairs. Following the definition I state several correctness properties certifying that we have the correct definitions.

At this point I define the church-encoding of pairs. The following defines the constructor for pairs.

Definition pair_cons := 
  trm_Lam (trm_Lam (trm_lam (typ_bvar 1) 
  (trm_lam (typ_bvar 0) 
    (trm_Lam (trm_lam (typ_arrow (typ_bvar 2) (typ_arrow (typ_bvar 1) (typ_bvar 0))) 
      ((trm_app (trm_app (trm_bvar 0) (trm_bvar 2)) (trm_bvar 1)))))))).

This is a little hard to read so lets take a look at this in mathematical notation.
\Lambda X.\Lambda Y.\lambda x:X.\lambda y:Y.\Lambda Z.\lambda z:X \rightarrow (Y \rightarrow Z).(z\,x)\,y.
Here the variables \(x\) and \(y\) are the data we are packaging up in the pair. The variable \(z\) is used to project out the data of the pair. Next we define the type of pair_cons.

Definition pair_cons_type := 
 typ_forall (typ_forall (typ_arrow (typ_bvar 1) (typ_arrow (typ_bvar 0) 
   (typ_forall (typ_arrow 
     (typ_arrow (typ_bvar 2) (typ_arrow (typ_bvar 1) (typ_bvar 0))) (typ_bvar 0)))))).

In mathematical notation this looks like the following:

\forall X.\forall Y.X \rightarrow (Y \rightarrow \forall Z.((X \rightarrow (Y \rightarrow Z)) \rightarrow Z)).

The previous definitions are how define church-encoded pairs in system F. Next are the definitions of two convince functions which will allow us to easily construct pairs. The following is the definition of a pair given two terms a:A and b:B.

Definition pair (A B:typ) (a b:trm) := trm_app (trm_app (trm_tapp (trm_tapp pair_cons A) B) a) b.

The following is the type of pair.

Definition pair_type (A B:typ) := 
  typ_forall (typ_arrow (typ_arrow A (typ_arrow B (typ_bvar 0))) (typ_bvar 0)).

We need to be sure these are the correct definitions so first I show that pair_cons has the type pair_cons_type and that pair has the type pair_type. I omit proofs for brevity.

Lemma pair_cons_typing : nil :> pair_cons ; pair_cons_type.

Lemma pair_typing : forall A B a b, 
  lc_T A ->
  lc_T B ->
  nil :> a ; A ->
  nil :> b ; B ->
  nil :> pair A B a b ; pair_type A B.

Using our pair definition we can construct pairs, but we still need ways of getting the data back out of the pairs. Next I define the first and second projections of our pairs. First, O need two very simple functions. They are used for deciding which projection we want. The first function, arg_one, is used to get the first projection, while the second, arg_two, is used to get the second.

Definition arg_one A B := trm_lam A (trm_lam B (trm_bvar 1)).
Definition arg_two A B := trm_lam A (trm_lam B (trm_bvar 0)).

Now using arg_one and arg_two I can define the first and second projections as follows:

Definition fst (A:typ) (B:typ) (p:trm) := trm_app (trm_tapp p A) (arg_one A B).
Definition snd (A:typ) (B:typ) (p:trm) := trm_app (trm_tapp p B) (arg_two A B).

Again I must be sure these are the correct definitions. I first show that fst and snd have the expected type.

Lemma fst_typing : forall A B p,
  lc_T A ->
  lc_T B ->
  nil :> p ; pair_type A B ->
  nil :> fst A B p ; A.

Lemma snd_typing : forall A B p,
  lc_T A ->
  lc_T B ->
  nil :> p ; pair_type A B ->
  nil :> snd A B p ; B.

Recall that I defined \(\beta\eta\)-equality. All equational reasoning I will do will be using \(\beta\eta\)-equality. Using this I show that applying fst to a pair is equivalent to the first project of the pair.

Lemma fst_eq : forall A B a b,
  nil :> a ; A ->
  nil :> b ; B ->
  nil :> (pair A B a b) ; pair_type A B ->
  nil :> fst A B (pair A B a b) <~> a ; A.

Finally, I do the same for snd.

Lemma snd_eq : forall A B a b,
  nil :> a ; A ->
  nil :> b ; B ->
  nil :> (pair A B a b) ; pair_type A B ->
  nil :> snd A B (pair A B a b) <~> b ; B.

We have set out on a journey to better understand the relationship between church-encoded pairs in system F and categorical products. So far we have defined system F with \(\beta\eta\)-equality and defined church-encoded pairs in system F. In the next post we will layout all the necessary category theory we will need for the main result. Stay tuned.

This entry was posted in category theory, Coq, Logic, metatheory, Semantics, Type Theory and tagged , , , , , . Bookmark the permalink.

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>