% Girard-Reynolds isomorphism
% based on Wadler's paper

% Kevin Watkins
% April 2005



% Wadler's "F2"

tp : type.              % Types
tm : tp -> type.        % Terms of a given type

=> : tp -> tp -> tp.    % Function arrow
                                                %infix right 8 =>.
! : (tp -> tp) -> tp.   % Forall

\ : (tm A -> tm B) -> tm (A => B).
@ : tm (A => B) -> tm A -> tm B.                %infix left 7 @.
gen : ({X:tp} tm (B X)) -> tm (![X] B X).
inst : tm (![X] B X) -> {A:tp} tm (B A).        %infix left 7 inst.

% Another way to think about F2 is as the pure type system
%   tp : kd
%   (tp, tp, tp)
%   (kd, tp, tp)



% Wadler's "P2"
% This is not actually a system treated in Girard's thesis, as
% far as I can tell.

o : type.               % Propositions
pf : o -> type.         % Proofs of a given proposition
% In LF there's no need for an explicit syntax of predicates;
% they're just LF functions from terms to propositions.
% This has the effect of internalizing beta- and eta-equivalences
% over predicates into LF's own notion of equality.
pr : tp -> type
        = [A] tm A -> o.

--> : o -> o -> o.      % Implies
                                                %infix right 3 -->.
tp! : (tp -> o) -> o.   % Forall (types)
tm! : (tm C -> o) -> o. % Forall (terms of a given type)
pr! : (pr C -> o) -> o. % Forall (predicates over a given type)

lam : (pf A -> pf B) -> pf (A --> B).
app : pf (A --> B) -> pf A -> pf B.             %infix left 1 app.
tpgen : ({X:tp} pf (B X)) -> pf (tp![X] B X).
tpinst : pf (tp![X] B X) -> {A:tp} pf (B A).    %infix left 1 tpinst.
tmgen : ({x:tm C} pf (B x)) -> pf (tm![x] B x).
tminst : pf (tm![x] B x) -> {t:tm C} pf (B t).  %infix left 1 tminst.
prgen : ({X:pr C} pf (B X)) -> pf (pr![X] B X).
prinst : pf (pr![X] B X) -> {A:pr C} pf (B A).  %infix left 1 prinst.

% Irritatingly, Wadler's paper is not precise about the congruences
% for beta equivalence.  I adopt the most restrictive interpretation.

% Since we have quantification over predicates, these could also be
% modeled as equalities within the logic itself.

beta : {C} pf (C ((\[x] T x) @ U)) -> pf (C (T U)).
instbeta : {C} pf (C ((gen[x] T x) inst A)) -> pf (C (T A)).

% Combinators for conversions
%abbrev
at : ({C:pr A} pf (C T) -> pf (C U)) -> {C:pr A} pf (C T) -> pf (C U)
        = [cnv] cnv.                            %infix left 2 at.

%abbrev
conv : pf A -> (pf A -> pf B) -> pf B
        = [d] [e] e d.                          %infix left 1 conv.

%abbrev
rev : ({C:pr A} pf (C T) -> pf (C U))
   -> ({C:pr A} pf (C U) -> pf (C T))
        = [cnv] [C] [d] (lam[x] x) conv cnv at ([h] C h --> C T)
                                   app d.

% The conversions on proofs are tedious, so I'm not representing them.

% P2 seems to be related to the PTS
%   tp : kd
%   (tp, tp, tp)
%   (kd, tp, tp)
%   o : ltp (logical types)
%   (o, o, o)
%   (ltp, o, o)
%   (tp, ltp, ltp)
%   (tp, o, o)
%   (kd, o, o)

% The system U does come up in Girard's thesis, where it's proved
% inconsistent.  I think the relevant fragment of U in PTS would be
%   tp : kd
%   (tp, tp, tp)
%   (kd, tp, tp)
%   o : tp
%   (o, o, o)
%   (tp, o, o)



% Simulations of nullary and binary predicates

1 : tp
        = ![X] X => X.
unit : tm 1
        = gen[X] \[x] x.
%abbrev
nullary : o -> pr 1
        = [C] [x] C.

% The beta-conversion for nullary predicates listed in Wadler's paper
% is internalized by LF's notion of equality.

* : tp -> tp -> tp
        = [A] [B] ![X] (A => B => X) => X.      %infix left 10 *.
pair : tm A -> tm B -> tm (A * B)
        = [t] [u] gen[X] \[k] k @ t @ u.
fst : tm (A * B) -> tm A
        = [s] s inst A @ (\[x] \[y] x).
snd : tm (A * B) -> tm B
        = [s] s inst B @ (\[x] \[y] y).
%abbrev
binary : (tm A -> tm B -> o) -> pr (A * B)
        = [C] [z] C (fst z) (snd z).

%abbrev
fstbeta : {C} pf (C (fst (pair T U))) -> pf (C T)
        = [C] [d] d conv instbeta at ([h] C (h @ (\[x] \[y] x)))
                    conv beta at ([h] C h)
                    conv beta at ([h] C (h @ U))
                    conv beta at ([h] C h).
%abbrev
sndbeta : {C} pf (C (snd (pair T U))) -> pf (C U)
        = [C] [d] d conv instbeta at ([h] C (h @ (\[x] \[y] y)))
                    conv beta at ([h] C h)
                    conv beta at ([h] C (h @ U))
                    conv beta at ([h] C h).

%abbrev
binarybeta : {C} pf (C (binary Pred (pair T U))) -> pf (C (Pred T U))
        = [C] [d] d conv fstbeta at ([h] C (Pred h (snd (pair T U))))
                    conv sndbeta at ([h] C (Pred T h)).



% Definitions of other logical connectives

true : o
        = pr![X] X unit --> X unit.
false : o
        = pr![X] X unit.
&& : o -> o -> o
        = [A] [B] pr![X] (A --> B --> X unit) --> X unit.
                                                %infix left 5 &&.
|| : o -> o -> o
        = [A] [B] pr![X] (A --> X unit) --> (B --> X unit) --> X unit.
                                                %infix left 4 ||.
<-> : o -> o -> o
        = [A] [B] (A --> B) && (B --> A).       %infix none 3 <->.

% Relations on predicates

<= : pr A -> pr A -> o
        = [A] [B] tm![x] A x --> B x.           %infix none 6 <=.
pr== : pr A -> pr A -> o
        = [A] [B] A <= B && B <= A.             %infix none 6 pr==.

% Leibniz equality

== : tm A -> tm A -> o
        = [t] [u] pr![X] X t --> X u.           %infix none 6 ==.

refl : pf (T == T)
        = prgen[X] lam[x] x.
sym : pf (T == U) -> pf (U == T)
        = [d] d prinst ([x] x == T) app refl.
trans : pf (T == U) -> pf (U == V) -> pf (T == V)
        = [d] [e] prgen[X] lam[x] e prinst X app (d prinst X app x).
==beta : pf ((\[x] T x) @ U == T U)
        = prgen[X] lam[x] x conv beta at ([h] X h).

% Generally, in LF it's better to use meta-congruences than this sort
% of extensionality axiom, but I'm too lazy to modify Wadler's treatment.

ext : pf (tm![f] tm![g] (tm![x] f @ x == g @ x) --> f == g).
tpext : pf (tm![f] tm![g] (tp![X] f inst X == g inst X) --> f == g).



% The "Girard projection"

% Judgments
o# : o -> tp -> type.
pr# : pr A -> tp -> type.
pf# : pf A -> tm A# -> type.

% The projection of propositions
--># : o# (A --> B) (A# => B#)
        <- o# A A#
        <- o# B B#.
tp!# : o# (tp![X] A X) A#
        <- {X} o# (A X) A#.
tm!# : o# (tm![x] A x) A#
        <- {x} o# (A x) A#.
pr!# : o# (pr![X] A X) (![X#] A# X#)
        <- ({X} {X#} pr# X X# -> o# (A X) (A# X#)).

% The projection of predicates
% This is slightly awkward (it doesn't mode check)
pred# : o# (A T) A#
        <- pr# A A#.

% The projection of proofs
lam# : pf# (lam[x] U x) (\[x#] U# x#)
        <- ({x} {x#} pf# x x# -> pf# (U x) (U# x#)).
app# : pf# (S app T) (S# @ T#)
        <- pf# S S#
        <- pf# T T#.
tpgen# : pf# (tpgen[X] U X) U#
        <- ({X} pf# (U X) U#).
tpinst# : pf# (S tpinst T) S#
        <- pf# S S#.
tmgen# : pf# (tmgen[x] U x) U#
        <- ({x} pf# (U x) U#).
tminst# : pf# (S tminst T) S#
        <- pf# S S#.
prgen# : pf# (prgen[X] U X) (gen[X#] U# X#)
        <- ({X} {X#} pr# X X# -> pf# (U X) (U# X#)).
prinst# : pf# (U prinst X) (U# inst X#)
        <- pf# U U#
        <- ({x} o# (X x) X#).

% Wadler's paper leaves out projections for the extensionality axioms.
% However, they are probably trivial, because every term equality
% (T == U) projects to the unit type, as Twelf can demonstrate:

%solve _ : o# (T == U) 1.



% The "Reynolds embedding"
% This turns into a bit of a nightmare for Twelf's term reconstruction
% engine unless you annotate heavily.

% Judgments
tp$ : {X:tp} pr X -> type.
tm$ : tm A -> pf A$ -> type.

% The embedding of types
=>$ : tp$ (A => B) ([z] tm![x] A$ x --> B$ (z @ x))
        <- tp$ A A$
        <- tp$ B B$.
!$ : tp$ (![X] B X) ([z] tp![X] pr![X$] B$ X X$ (z inst X))
        <- ({X} {X$} tp$ X X$ -> tp$ (B X) (B$ X X$)).

% The embedding of terms
\$ : tm$ (\[x] U x) (tmgen[x] lam[x$] U$ x x$ conv rev beta at ([h] B$ h)
                : pf (B$ ((\[x] U x) @ x)))
        <- ({x} {x$} tm$ x (x$ : pf (A$ x))
                -> tm$ (U x) (U$ x x$ : pf (B$ (U x)))).
@$ : tm$ (S @ T) (S$ tminst T app T$)
        <- tm$ S (S$ : pf (tm![x] A$ x --> B$ (S @ x)))
        <- tm$ T (T$ : pf (A$ T)).
gen$ : tm$ (gen[X] U X) (tpgen[X] prgen[X$] U$ X X$ conv rev instbeta at ([h] B$ X X$ h)
                : pf (B$ X X$ ((gen[X] U X) inst X)))
        <- ({X} {X$} tp$ X X$
                -> tm$ (U X) (U$ X X$ : pf (B$ X X$ (U X)))).
inst$ : tm$ (S inst A) (S$ tpinst A prinst A$)
        <- tm$ S (S$ : pf (tp![X] pr![X$:pr X] B$ X X$))
        <- tp$ A A$.

% Note that I haven't sanity checked Twelf's reconstructions for
% either translation.  They might be excessively general, requiring
% further annotations.