# Lightweight Free Theorems

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