# 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