-- Data
---------

-- In the Calculus of Constructions, it is possible to encode data via
-- Church-style encodings. However, it is then impossible to do
-- inductive reasoning on these. This led to the addition of inductive
-- constructions (CiC). Agda features inductive families as a native
-- construct.

-- Even though uAgda does not feature a native construction for data,
-- it is possible to encode data using parametricity, erasure and a
-- little bit of special sauce. The trick is that 

-- 1. The erasure of the induction principle for a given inductive
-- family is equal to its Church representation, and

-- 2. The relational interpretation of the representation yields back
-- the inductive principle.

-- More theoretical background can be found in Phil Wadler's "The
-- Girard-Reynolds isomorphism".


-- In uAgda, we proceed as follows. First define the appropriate
-- induction principle and the proof that the constructors respect
-- induction. (Note that these definitions are parameterised over an
-- arbitrary module "q" containing an *abstract* version of the stuff
-- we want to define (here with fields Nat, suc and zer).

param Q = \ q -> (

Nat = \n -> (P : q#Nat -> *) -> ((n : q#Nat) -> P n -> P (q#suc n)) -> (P q#zer) -> P n,
zer = \P s z -> z,
suc = \m n P s z -> s m (n P s z),
\ _ -> *)

:: ((Nat : *1) ; (zer : Nat) ; (suc : Nat -> Nat) ; *1),

-- The keyword "param" and the double colon are special syntax to
-- construct a concrete representation (here "Q") that is
-- computationally equal to the erasure of the above, but whose
-- relational interpretation is the one given.

-- (The last component of the tuple is just noise, as usual).


-- From there we can do simple computations:
one = Q#suc Q#zer : Q#Nat,
two = Q#suc one,



-- And we can also do inductive reasoning (but indexed by a less
-- relevant version of the type/values):
Nat-elim = \n -> n!
         : (n : Q#Nat) -> (P : Q<#Nat -> *) -> ((n : Q<#Nat) -> P n -> P (Q<#suc n)) -> (P Q<#zer) -> P n<,


-- In particular, we can also inductive computation.  In that case,
-- because we work in a predicative type system, we need to apply the
-- induction on a copy of the natural lifted to a higher universe.
-- That's fine, because we also have an operator for that: postfix ^.

lift = \n -> n^
     : Q#Nat -> Q#Nat^,

plus 
 = \m n -> n^! (\_ -> Q#Nat) (\_ r -> Q#suc r) m 
 : Q#Nat -> Q#Nat -> Q#Nat,


four = plus two two,

*