Setoids in Agda

Setoid is a record type in Agda, and it appears everywhere from Relation.Binary.EqReasoning to Algebra. But, why do we need such a type ? After reading “setoids in type theory”, I thought that setoids are used for mathematical constructions like subset, quotients in the intensional type theory and the Calculus of Inductive Construction. Since some of functional data structure could be represented as such constructions, it also may be useful for functional programming, at least for understanding it.

Setoid is defined as a record type as follows,

record Setoid : Set1 where
infix 4 _≈_
field

carrier : Set
_≈_ : Rel carrier
isEquivalence : IsEquivalence _≈_

where isEquivalence is a record type packing the proof of equivalence relation defined as follows,

record IsEquivalence {a : Set} (_≈_ : Rel a) : Set where
field

refl : Reflexive _≈_
sym : Symmetric _≈_
trans : Transitive _≈_

Usually, we call such a setoid is a “total” setoid since it’s defined on all elements of type “carrier“. We will explan what is the meaning of each field.

  1. carrier : Set : the underlaying type what we want to operate on,
  2. _≈_ : Rel : the relation what we think the equality between elements of “carrier”,
  3. isEquivalence : IsEquivalence _≈_: the proof terms which show that _≈_ is a equivalence relation.

Thus, there is a induced setoid from Leibniz equality (see Relation.Binary.Core) for evey types, that is, we have a setoid for every type A, by computationally equality (“for all x in A, x ≡ x”). You could find such induced setoid from Relation.Binary.PropositionalEquality.≡-setoid defined on all types.

However, we could define other equivalence relation. For example, we want to identify lists with the same length, and we could define it as follows,

data _∼_ {a : Set}(xs : List a) : (List a) → Set where

len-eq : {ys : List a} → (pf : length xs ≡ length ys) → xs ∼ ys

It’s obvious to see that it’s a equivalence relation, and we could give proof terms about it.

∼-refl : ∀ {a} → {xs : List a} → xs ∼ xs
∼-refl = len-eq ≡-refl

∼-sym : ∀ {a} → {xs ys : List a} → xs ∼ ys → ys ∼ xs
∼-sym (len-eq refl) = len-eq (≡-sym refl)

∼-trans : ∀ {a} → {xs ys zs : List a} → xs ∼ ys → ys ∼ zs → xs ∼ zs
∼-trans (len-eq xs∼ys) (len-eq ys∼zs) = len-eq (≡-trans xs∼ys ys∼zs)

It’s trivial since they use the fact from Leibnz equality. Finally, we could pack them together simply by define it as a Setoid by hand, but we notice that it is just as same as defining a quotient on ≡-setoid (List a). Hence, we define a function Quotient to do this,

Quotient : (S : Set)(_∼_ : Rel S)(ER : IsEquivalence _∼_) → Setoid
Quotient S _∼_ ER = record

{ carrier = S
; _≈_ = _∼_
; isEquivalence = ER
}

Thus, the following is \mathbf{List(A) / \sim }.

ListLen : (a : Set) → Setoid
ListLen a = Quotient (List a) _∼_ ∼-isEQ

where

∼-isEQ : IsEquivalence (_∼_ {a})
∼-isEQ = record

{ refl = ∼-refl
; sym = ∼-sym
; trans = ∼-trans
}

We could show that ListLen is equivalent to \mathbb{N} by constructing a function from ListLen to \mathbb{N} and its inverse. Notice that, it’s exactly the function Data.List.length and Data.List.replicate. From these function, we could define “plus” from “concatenate” by such mapping from ListLen to \mathbb{N}. It means that we could define an operation on a more delicated structure, and get the operation on its quotient, via \pi : \mathbf{List(A)} \rightarrow (\mathbf{List(A)}/\sim{}) \cong \mathbb{N}.

Advertisements

5 thoughts on “Setoids in Agda

  1. Thanks for the explanation! I didn’t quite understand what Setoid was for.

    Questions:

    > We could show that ListLen is equivalent to N by constructing a function from ListLen to and its inverse.

    You mean from the carrier of ListLen to N, right?

    > It means that we could define an operation on a more delicated structure, and get the operation on its quotient, via…

    It’d be great to know how to do that!

    • You mean from the carrier of ListLen to N, right?

      No, I mean a map from a setoid to a setoid. So I must give it a proof that the length and replicate preserve the equality.

      It’d be great to know how to do that!

      It may look a bit strange such that I define _∼_ by Nat. However, we could avoid it as follows,

      data _∼_ {a : Set} : (List a) → (List a) → Set where
      []-eq : [] ∼ []
      ∷-eq : ∀ {xs ys x y} → (xs∼ys : xs ∼ ys) → (x ∷ xs) ∼ (y ∷ ys)

      The proof of this equivalence relation is also easy with pattern matching. Thus we could define plus' on Nat (Setoid) by composition with ++ and length. Then, define the extracted function (Map.ap plus') as plus. Hummm, I haven’t yet written about Map, and I think I will post it later.

  2. Pingback: Decidable setoid in Agda « XOO’s

  3. A few years have passed since this post. I am not able to find \==-refl and \==-setoid in the current agda libraries. Could you please provide a current pointer ?

    • Hi, I am not so sure about your question. You may start from Relation.Binary for a definition of equivalence relation.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s