csci8980-f21/extra/Modules.lagda.md

title	layout	permalink
Modules: Modules and List Examples	page	/Modules/

** Turn this into a Setoid example. Copy equivalence relation and setoid from the standard library. **

module plfa.Modules where

This chapter introduces modules as a way of structuring proofs, and proves some general results which will be useful later.

Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Function using (_∘_)
open import Level using (Level)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.List using (List; []; _∷_; _++_; map; foldr; downFrom)
open import Data.List.All using (All; []; _∷_)
open import Data.List.Any using (Any; here; there)
open import plfa.Isomorphism using (_≃_; extensionality)

Modules

Let's say we want to prove some standard results about collections of elements of a given type at a given universe level with a given equivalence relation for equality. One way to do so is to begin every signature with a suitable sequence of implicit parameters. Here are some definitions, where we represent collections as lists. (We would call collections sets, save that the name Set already plays a special role in Agda.)

Coll′ : ∀ {ℓ : Level} → Set ℓ → Set ℓ
Coll′ A  =  List A

_∈′_ : ∀ {ℓ : Level} {A : Set ℓ} {_≈_ : A → A → Set ℓ} → A → Coll′ A → Set ℓ
_∈′_ {_≈_ = _≈_} x xs  =  All (x ≈_) xs

_⊆′_ : ∀ {ℓ : Level} {A : Set ℓ} {_≈_ : A → A → Set ℓ} → Coll′ A → Coll′ A → Set ℓ
_⊆′_ {_≈_ = _≈_} xs ys  =  ∀ {w} → _∈′_  {_≈_ = _≈_} w xs → _∈′_ {_≈_ = _≈_} w ys

This rapidly gets tired. Passing around the equivalence relation _≈_ takes a lot of space, hinders the use of infix notation, and obscures the essence of the definitions.

Instead, we can define a module parameterised by the desired concepts, which are then available throughout.

module Collection {ℓ : Level} (A : Set ℓ) (_≈_ : A → A → Set ℓ) where

  Coll : ∀ {ℓ : Level} → Set ℓ → Set ℓ
  Coll A  =  List A

  _∈_ : A → Coll A → Set ℓ
  x ∈ xs  =  Any (x ≈_) xs

  _⊆_ : Coll A → Coll A → Set ℓ
  xs ⊆ ys  =  ∀ {w} → w ∈ xs → w ∈ ys

Use of a module

open Collection (ℕ) (_≡_)

pattern [_] x  =  x ∷ []
pattern [_,_] x y  =  x ∷ y ∷ []
pattern [_,_,_] x y z  =  x ∷ y ∷ z ∷ []

ex : [ 1 , 3 ] ⊆ [ 1 , 2 , 3 ]
ex (here refl)          =  here refl
ex (there (here refl))  =  there (there (here refl))
ex (there (there ()))

Abstract types

Say I want to define a type of stacks, with operations push and pop. I can define stacks in terms of lists, but hide the definitions from the rest of the program.

abstract

  Stack : Set → Set
  Stack A = List A

  empty : ∀ {A} → Stack A
  empty = []

  push : ∀ {A} → A → Stack A → Stack A
  push x xs  =  x ∷ xs

  pop : ∀ {A} → Stack A → Maybe (A × Stack A)
  pop []        =  nothing
  pop (x ∷ xs)  =  just ⟨ x , xs ⟩

  lemma-pop-push : ∀ {A} {x : A} {xs} → pop (push x xs) ≡ just ⟨ x , xs ⟩
  lemma-pop-push = refl

  lemma-pop-empty : ∀ {A} → pop {A} empty ≡ nothing
  lemma-pop-empty = refl

Standard Library

Definitions similar to those in this chapter can be found in the standard library.

-- EDIT

The standard library version of IsMonoid differs from the one given here, in that it is also parameterised on an equivalence relation.

Unicode

This chapter uses the following unicode.

EDIT
∷  U+2237  PROPORTION  (\::)
⊗  U+2297  CIRCLED TIMES  (\otimes)
∈  U+2208  ELEMENT OF  (\in)
∉  U+2209  NOT AN ELEMENT OF  (\inn)