[Agda] Lightweight free theorems

[Jean-Philippe Bernardy]

Hello,

In this message I present a library (in attachment) to construct "free
theorems" with ease.  Agda serves both as a host and target language.

As Reynolds [1] tells us, a type "T" can be interpreted as a relation
"[T]", and every inhabitant "t" of type "T" satisfies the relation.

   "if ⊢ t : T then (t,t) ∈ [T]"

For complicated types T, the corresponding relation [T] can be tedious
to write. A tool such as Voigtländer's [2] can be of help.
Unfortunately, that tool supports only Haskell, and has limited
support for data types. The library supports full Agda, at the cost of
more user involvement.

The promise is that given a type such as:

Filter =   (A : Set)      →  (  A   →   Bool)    →    List   A    →    List   A
or equivalently
Filter =    Π   Set   \ A  →  ( A   →   Bool)    →    List   A    →    List   A

The corresponding relation can be obtained by merely "quoting" each symbol:

[Filter] = [Π] [Set] \ [A] →  ([A] [→] [Bool])  [→]  [List] [A]  [→]  [List] [A]

The library provides the combinators [Π], [Set], and [→]. It is up to
the user to add support for each data type, but that is easily done as
we shall see next.


data Bool : Set where
  true : Bool
  false : Bool

To produce a the relational equivalent of an inductive definition such
a the above, quote each symbol, and apply the (translated) type to the
original constant (twice).

data [Bool] : [Set] Bool Bool where
  [true]  : [Bool] true true
  [false] : [Bool] false false


If an inductive definition has a parameter, it must be duplicated, and
an extra parameter (witnessing the relation) must be added:

data List (A : Set) : Set where
    nil : List A
    cons : A -> List A -> List A

data [List] {A1 A2 : Set} ([A] : [Set] A1 A2) : [Set] (List A1) (List A2) where
    [nil]  : [List] [A] nil nil
    [cons] : ([A]  [->]  [List] [A]  [->]  [List] [A]) cons cons


We can then use Agda's "normalize-term" feature to expand relations,
and obtain free theorems:

check : (∀ f -> [Filter] f f) == (
     -- for any function of the Filter type,
  (f : Filter)
     -- for any relation A1 ↔ A2,
  {A1 : Set} {A2 : Set} ([A] : A1 → A2 → Set)
     -- if p1, p2 take related values to equal booleans
  {p1 : A1 → Bool} {p2 : A2 → Bool} →
    (pR : ∀ {a1 a2} → [A] a1 a2 → [Bool] (p1 a1) (p2 a2))
    -- if xs1, xs2 are related by [A] indexwise,
  {xs1 : List A1} {xs2 : List A2} (xsR : [List] [A] xs1 xs2) →
    -- then the results are related by [A] indexwise
  [List] [A] (f A1 p1 xs1) (f A2 p2 xs2) )
check = refl

The code for the library, plus examples, is in attachment.  The theory
and further details are described in our draft paper [3].

Cheers,
-- JP

[1] John C. Reynolds, "Types, Abstraction and Parametric
Polymorphism." Information Processing, 1983
[2] http://www-ps.iai.uni-bonn.de/ft/
[3] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=118913
-------------- next part --------------
A non-text attachment was scrubbed...
Name: LFT.agda
Type: application/octet-stream
Size: 3732 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100507/90608c8e/LFT-0001.obj