LightweightFreeTheorems

The Lightweight Free Theorems library (Attach:LFT.agda) allows to construct so called "free theorems" with ease.

Background

As Reynolds 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 (http://www-ps.iai.uni-bonn.de/ft/) 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.

Usage

To create a free theorem for a type such as:

 Filter =   (A : Set)       →  ( A   →   Bool)    →    List   A    →    List   A

rewrite using Π combinator:

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

And then "quote" every symbol:

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

Use Agda's "normalize-term" feature to expand the relations.

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 types

Relations for data types are created in a similar way. To produce 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 where
   true : Bool
   false : Bool

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

Parameters

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

More

Make sure to check out the examples provided in the attachment (Attach:LFT.agda). Theory is detailed in the paper: http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=118913