uAgda-1.1.0.0: tutorial/02.1-Relevance.ua

-- Relevance and erasure
-------------------------

-- In uAgda, there are two flavours of quantification:
-- relevant and irrelevant. (We borrow the notion from Pfenning (2001)).

-- One can roughly thing as irrelevant things as things whose
-- computational content is inaccessible ("proofs"), while relevant
-- ones are regular terms whose computational content is relevant.
-- Irrelevant product is denoted with =>. Irrelevancy of abstraction
-- and applications is inferred.

-- Irrelevancy is enforced by making sure irrelevant variables are
-- never directly returned. They can only be used as arguments to
-- irrelevant applications or on the LHS of =>.

-- For example the following term does not type-check because 'A' is
-- used in the result directly, while it is irrelevant: 

{-
Wrong = \(A : *) -> A 
      : * => *,
-}

-- An example where irrelevance can be used for more precise typing is
-- the following. We can use a more precise type of the Leibniz
-- equality that says that the actual type used is irrelevant for the
-- predicate:

Eq = \ A a b -> (P : A => *) -> P a -> P b
     : (A : *) -> (a b : A) => *1,

-- Another example is the following: the inductive principle for
-- natural numbers is independent on the actual representation of the
-- naturals, so they are irrelevant.  This can be expressed as
-- follows...


Nat = 
      -- We assume an (abstract) representation N of naturals, as well as
      -- constructors for successor and zero.
      \(N : *) (s : N -> N) (z : N) ->

      -- Then define the induction principle:
      \(n : N) -> (P : N => *) -> P z -> ((m : N) => P m -> P (s m)) -> P n,


-- We know that all the programs we have written using naturals
-- satisfying the above induction principle can be represented by
-- Naturals where the irrelevant parts are erased. We can access this
-- erasure within uAgda by using the % operator. The second argument
-- is the depth of irrelevancy to erase. 

Nat-representation = Nat % 0,

-- The normal form of the above term reveals that the result is the
-- usual Church encoding for naturals.


*