# Tutorial: Setoids
A _setoid_ is a type equipped with an equivalence relation. Setoids come up when
you need types with a better behaved equality relation, or when you want the
equality relation to carry additional information. After completing this
tutorial you will:
1. Know the user interface to the `setoid` package.
2. Know two different applications in which it can be used:
+ constructing types with an equality relation that's better behaved than
Idris's built-in `Equal` type.
+ types with an equality relation that carries additional information
If you want to see the source-code behind this tutorial, check the
[source-code](sources/Tutorial.md) out.
## Equivalence relations
A _relation_ over a type `ty` in Idris is any two-argument type-valued function:
```
namespace Control.Relation
Rel : Type -> Type
Rel ty = ty -> ty -> Type
```
This definition and its associated interfaces ship with idris's standard
library. Given a relation `rel : Rel ty` and `x,y : ty`, we can form
```x `rel` y : Type```: the type of ways in which `x` and `y` can be related.
For example, two lists _overlap_ when they have a common element:
record Overlap {0 a : Type} (xs,ys : List a) where
constructor Overlapping
common : a
lhsPos : common `Elem` xs
rhsPos : common `Elem` ys
Lists can overlap in exactly one position:
Ex1 : Overlap [1,2,3] [6,7,2,8]
Ex1 = Overlapping
{ common = 2
, lhsPos = There Here
, rhsPos = There (There Here)
}
But they can overlap in several ways:
Ex2a ,
Ex2b ,
Ex2c : Overlap [1,2,3] [2,3,2]
Ex2a = Overlapping
{ common = 3
, lhsPos = There (There Here)
, rhsPos = There Here
}
Ex2b = Overlapping
{ common = 2
, lhsPos = There Here
, rhsPos = Here
}
Ex2c = Overlapping
{ common = 2
, lhsPos = There Here
, rhsPos = There (There Here)
}
We can think of a relation `rel : Rel ty` as the type of edges in a directed
graph between vertices in `ty`:
* edges have a direction: the type `rel x y` is different to `rel y x`
* multiple different edges between the same vertices `e1, e2 : rel x y`
* self-loops between the same vertex are allowed `loop : rel x x`.
An _equivalence relation_ is a relation that's:
* _reflexive_: we guarantee a specific way in which every element is related to
itself;
* _symmetric_: we can reverse an edge between two edges; and
* _transitive_: we can compose paths of related elements into a single edge.
record Equivalence (A : Type) where
constructor MkEquivalence
0 relation: Rel A
reflexive : (x : A) -> relation x x
symmetric : (x, y : A) -> relation x y -> relation y x
transitive: (x, y, z : A) -> relation x y -> relation y z
-> relation x z
We equip the built-in relation `Equal` with the structure of an equivalence
relation, using the constructor `Refl` and the stdlib functions `sym`, and
`trans`:
EqualityEquivalence : Equivalence a
EqualityEquivalence = MkEquivalence
{ relation = (===)
, reflexive = \x => Refl
, symmetric = \x,y,x\_eq\_y => sym x\_eq\_y
, transitive = \x,y,z,x\_eq\_y,y\_eq\_z => trans x\_eq\_y y\_eq\_z
}
We'll use the following relation on pairs of natural numbers as a running
example. We can represent an integer as the difference between a pair of natural
numbers:
infix 8 .-.
record INT where
constructor (.-.)
pos, neg : Nat
record SameDiff (x, y : INT) where
constructor Check
same : (x.pos + y.neg === y.pos + x.neg)
The `SameDiff x y` relation is equivalent to mathematical equation that states
that the difference between the positive and negative parts is identical:
$$x_{pos} - x_{neg} = y_{pos} - y_{neg}$$
But, unlike the last equation which requires us to define integers and
subtraction, its equivalent `(.same)` is expressed using only addition, and
so addition on `Nat` is enough.
The relation `SameDiff` is an equivalence relation. The proofs are
straightforward, and a good opportunity to practice Idris's equational
reasoning combinators from `Syntax.PreorderReasoning`:
SameDiffEquivalence : Equivalence INT
SameDiffEquivalence = MkEquivalence
{ relation = SameDiff
, reflexive = \x => Check $ Calc $
|~ x.pos + x.neg
~~ x.pos + x.neg ...(Refl)
This equational proof represents the single-step equational proof:
"Calculate:
1. $x_{pos} + x_{neg}$
2. $= x_{pos} + x_{neg}$ (by reflexivity)"
The mnemonic behind the ASCII-art is that the first step in the proof
starts with a logical-judgement symbol $\vdash$, each step continues with an
equality sign $=$, and justified by a thought bubble `(...)`.
, symmetric = \x,y,x\_eq\_y => Check $ Calc $
|~ y.pos + x.neg
~~ x.pos + y.neg ..<(x\_eq\_y.same)
In this proof, we were given the proof `x_eq_y.same : x.pos + y.neg = y.pos + x.neg`
and so we appealed to the symmetric equation. The mnemonic here is that the
last bubble in the thought bubble `(...)` is replace with a left-pointing arrow,
reversing the reasoning step.
, transitive = \x,y,z,x\_eq\_y,y\_eq\_z => Check $ plusRightCancel \_ \_ y.pos
$ Calc $
|~ x.pos + z.neg + y.pos
~~ x.pos + (y.pos + z.neg) ...(solve 3 Monoid.Commutative.Free.Free
{a = Nat.Additive} $
(X 0 .+. X 1) .+. X 2
=-= X 0 .+. (X 2 .+. X 1))
~~ x.pos + (z.pos + y.neg) ...(cong (x.pos +) $ y\_eq\_z.same)
~~ (x.pos + y.neg) + z.pos ...(solve 3 Monoid.Commutative.Free.Free
{a = Nat.Additive} $
X 0 .+. (X 1 .+. X 2)
=-= (X 0 .+. X 2) .+. X 1)
~~ (y.pos + x.neg) + z.pos ...(cong (+ z.pos) ?h2)
~~ z.pos + x.neg + y.pos ...(solve 3 Monoid.Commutative.Free.Free
{a = Nat.Additive} $
(X 0 .+. X 1) .+. X 2
=-= (X 2 .+. X 1) .+. X 0)
}
This proof is a lot more involved:
1. We appeal to the cancellation property of addition:
$a + c = b + c \Rightarrow a = b$
This construction relies crucially on the cancellation property. Later, we
will learn about its general form, called the INT-construction.
2. We rearrange the term, bringing the appropriate part of `y` into contact with
the appropriate part of `z` and `x` to transform the term.
Here we use the idris library [`Frex`](http://www.github.com/frex-project/idris-frex)
that can perform such routine
rearrangements for common algebraic structures. In this case, we use the
commutative monoid simplifier from `Frex`.
If you want to read more about `Frex`, check the
[paper](https://www.denotational.co.uk/drafts/allais-brady-corbyn-kammar-yallop-frex-dependently-typed-algebraic-simplification.pdf) out.
Idris's `Control.Relation` defines interfaces for properties like reflexivity
and transitivity. While the
setoid package doesn't use them, we'll use them in a few examples.
The `Overlap` relation from Examples 1 and 2 is symmetric:
Symmetric (List a) Overlap where
symmetric xs\_overlaps\_ys = Overlapping
{ common = xs\_overlaps\_ys.common
, lhsPos = xs\_overlaps\_ys.rhsPos
, rhsPos = xs\_overlaps\_ys.lhsPos
}
However, `Overlap` is neither reflexive nor transitive:
* The empty list doesn't overlap with itself:
Ex3 : Not (Overlap [] [])
Ex3 nil\_overlaps\_nil = case nil\_overlaps\_nil.lhsPos of
\_ impossible
* Two lists may overlap with a middle list, but on different elements. For example:
Ex4 : ( Overlap [1] [1,2]
, Overlap [1,2] [2]
, Not (Overlap [1] [2]))
Ex4 =
( Overlapping 1 Here Here
, Overlapping 2 (There Here) Here
, \ one\_overlaps\_two => case one\_overlaps\_two.lhsPos of
There \_ impossible
)
The outer lists agree on `1` and `2`, respectively, but they can't overlap on
on the first element of either, which exhausts all possibilities of overlap.
-- TODO: clean this up
(.+.) : (x, y : INT) -> INT
x .+. y = (x.pos + y.pos) .-. (x.neg + y.neg)
(.\*.) : (x, y : INT) -> INT
x .\*. y = (x.pos \* y.pos + x.neg \* y.neg) .-. (x.pos \* y.neg + x.neg \* y.pos)
O, I : INT
O = 0 .-. 0
I = 1 .-. 0
plusIntZeroLftNeutral : (x : INT) -> O .+. x `SameDiff` x
plusIntZeroLftNeutral x = Check Refl
plusIntZeroRgtNeutral : (x : INT) -> x .+. O `SameDiff` x
plusIntZeroRgtNeutral x = Check (solve 2 Monoid.Commutative.Free.Free
{a = Nat.Additive} $
(X 0 .+. O1) .+. X 1
=-= X 0 .+. (X 1 .+. O1))
plusInrAssociative : (x,y,z : INT) -> x .+. (y .+. z) `SameDiff` (x .+. y) .+. z
plusInrAssociative x y z = Check $ (solve 6 Monoid.Commutative.Free.Free
{a = Nat.Additive} $
(X 0 .+. (X 1 .+. X 2)) .+. ((X 3 .+. X 4) .+. X 5)
=-= (X 0 .+. X 1 .+. X 2) .+. (X 3 .+. (X 4 .+. X 5)))
data INT' : Type where
IPos : Nat -> INT'
INegS : Nat -> INT'
Cast INT' Integer where
cast (IPos k) = cast k
cast (INegS k) = - cast (S k)
Cast INT' INT where
cast (IPos k) = k .-. 0
cast (INegS k) = 0 .-. (S k)
normalise : INT -> INT
normalise i@(0 .-. neg ) = i
normalise i@((S k) .-. 0 ) = i
normalise i@((S k) .-. (S j)) = normalise (k .-. j)
normaliseEitherZero : (x : INT) -> Either ((normalise x).pos = Z) ((normalise x).neg = Z)
normaliseEitherZero i@(0 .-. neg ) = Left Refl
normaliseEitherZero i@((S k) .-. 0 ) = Right Refl
normaliseEitherZero i@((S k) .-. (S j)) = normaliseEitherZero (k .-. j)
Cast INT INT' where
cast x = let (pos .-. neg) = normalise x in
case normaliseEitherZero x of
(Left y) => case neg of
0 => IPos 0
(S k) => INegS k
s pos
-- x `SameDiff` y -> normalise x = normalise y
(:\*:), (:+:) : (x,y : INT') -> INT'
x :+: y = cast (cast x .+. cast y)
x :\*: y = cast (cast x .\*. cast y)