Axiomatising parametricity in Agda via rewrite rules, with a units of measure example

param.agda

{-# OPTIONS --prop --rewriting --confluence-check #-}

module param-rewrites where

open import Agda.Builtin.Unit

------------------------------------------------------------------------------
-- Equality as a proposition
data _≡_ {a} {A : Set a} : A → A → Prop where
  refl : ∀{a} → a ≡ a

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REWRITE _≡_ #-}

postulate
  subst : ∀ {ℓ1 ℓ2} {A : Set ℓ1}
          (a₁ : A) →
          (B : (a₂ : A) → a₁ ≡ a₂ → Set ℓ2)
          (b : B a₁ refl) →
          (a₂ : A)(e : a₁ ≡ a₂) →
          B a₂ e
  subst-refl : ∀ {ℓ1 ℓ2} (A : Set ℓ1)
          (a₁ : A)
          (B : (a₂ : A) → a₁ ≡ a₂ → Set ℓ2)
          (b : B a₁ refl) →
          subst a₁ B b a₁ refl ≡ b

{-# REWRITE subst-refl #-}

transport : ∀ {ℓ} {X Y : Set ℓ} → X ≡ Y → X → Y
transport{_}{X}{Y} e = subst X (\y _ → X → y) (λ x → x) Y e

trans : ∀ {ℓ}{X : Set ℓ}{x y z : X} → x ≡ y → y ≡ z → y ≡ z
trans refl refl = refl

symm : ∀ {ℓ}{X : Set ℓ}{x y : X} → x ≡ y → y ≡ x
symm refl = refl

------------------------------------------------------------------------------
-- Axiomatising parametricity
postulate
  𝕀 : Set
  src tgt : 𝕀

-- FIXME: ought to be a type of discrete sets: do not instantiate with 'Rel'
|Set| : Set₁
|Set| = Set

postulate
  Rel : ∀ (A B : |Set|)(R : A → B → Prop) → 𝕀 → Set

  Rel-src : ∀ (A B : |Set|)(R : A → B → Prop) → Rel A B R src ≡ A
  Rel-tgt : ∀ (A B : |Set|)(R : A → B → Prop) → Rel A B R tgt ≡ B

{-# REWRITE Rel-src Rel-tgt #-}

postulate
  rel : ∀ {A B : |Set|}{R : A → B → Prop}(a : A)(b : B)(r : R a b)(p : 𝕀) → Rel A B R p

  rel-src : ∀ (A B : |Set|)(R : A → B → Prop)(a : A)(b : B)(r : R a b) → rel {A} {B} {R} a b r src ≡ a
  rel-tgt : ∀ (A B : |Set|)(R : A → B → Prop)(a : A)(b : B)(r : R a b) → rel {A} {B} {R} a b r tgt ≡ b

{-# REWRITE rel-src rel-tgt #-}

postulate
  param : (A B : |Set|)(R : A → B → Prop)(f : (p : 𝕀) → Rel A B R p) → R (f src) (f tgt)

postulate
  elim : ∀ {a} {A B : |Set|}
         {R : A → B → Prop}
         (S : (p : 𝕀) → Rel A B R p → Set a)
         {f₁ : (a : A) → S src a}
         {f₂ : (b : B) → S tgt b}
         (fᵣ : (a : A)(b : B)(r : R a b)(p : 𝕀) → S p (rel a b r p))
         (p₁ : (a : A)(b : B)(r : R a b) → f₁ a ≡ fᵣ a b r src)
         (p₂ : (a : A)(b : B)(r : R a b) → f₂ b ≡ fᵣ a b r tgt)
         (p : 𝕀)(e : Rel A B R p) → S p e

  elim-src : ∀ {a} (A B : |Set|)(R : A → B → Prop)
         (S : (p : 𝕀) → Rel A B R p → Set a)
         (f₁ : (a : A) → S src a)
         (f₂ : (b : B) → S tgt b)
         (fᵣ : (a : A)(b : B)(r : R a b)(p : 𝕀) → S p (rel a b r p))
         (p₁ : (a : A)(b : B)(r : R a b) → f₁ a ≡ fᵣ a b r src)
         (p₂ : (a : A)(b : B)(r : R a b) → f₂ b ≡ fᵣ a b r tgt) →
         elim {a} {A} {B} {R} S {f₁} {f₂} fᵣ p₁ p₂ src ≡ f₁
  elim-tgt : ∀ {a} (A B : |Set|)(R : A → B → Prop)
         (S : (p : 𝕀) → Rel A B R p → Set a)
         (f₁ : (a : A) → S src a)
         (f₂ : (b : B) → S tgt b)
         (fᵣ : (a : A)(b : B)(r : R a b)(p : 𝕀) → S p (rel a b r p))
         (p₁ : (a : A)(b : B)(r : R a b) → f₁ a ≡ fᵣ a b r src)
         (p₂ : (a : A)(b : B)(r : R a b) → f₂ b ≡ fᵣ a b r tgt) →
         elim {a} {A} {B} {R} S {f₁} {f₂} fᵣ p₁ p₂ tgt ≡ f₂

  -- because propositions are always related, as long as they are both
  -- true
  elim-prop : ∀ {A B : |Set|}
         {R : A → B → Prop}
         (S : (p : 𝕀) → Rel A B R p → Prop)
         (f₁ : (a : A) → S src a)
         (f₂ : (b : B) → S tgt b)
         (p : 𝕀)(e : Rel A B R p) → S p e

{-# REWRITE elim-src elim-tgt #-}

-- Simply typed version of the relatedness eliminator
elim-simple : ∀ {a} {A B : |Set|}
       {R : A → B → Prop}
       {S : (p : 𝕀) → Set a}
       {f₁ : (a : A) → S src}
       {f₂ : (b : B) → S tgt}
       (fᵣ : (a : A)(b : B)(r : R a b)(p : 𝕀) → S p)
       (p₁ : (a : A)(b : B)(r : R a b) → f₁ a ≡ fᵣ a b r src)
       (p₂ : (a : A)(b : B)(r : R a b) → f₂ b ≡ fᵣ a b r tgt)
       (p : 𝕀) → Rel A B R p → S p
elim-simple {S = S} = elim (λ p _ → S p)


postulate
  -- FIXME: this ought to be an equality?
  identity-extension : ∀ {A : |Set|}(p : 𝕀) → A → Rel A A _≡_ p

  identity-extension-src : ∀ {A : |Set|} (a : A) → identity-extension src a ≡ a
  identity-extension-tgt : ∀ {A : |Set|} (a : A) → identity-extension tgt a ≡ a

{-# REWRITE identity-extension-src identity-extension-tgt #-}

id-param : ∀ {A : |Set|} → (f : 𝕀 → A) → f src ≡ f tgt
id-param f = param _ _ _≡_ λ p → identity-extension p (f p)

--------------------------------------------------------------------------------
-- Simple example
identity : (f : (X : Set) → X → X) →
           (Y : |Set|) →
           (y : Y) →
           f Y y ≡ y
identity f Y y =
  param Y ⊤ (λ y' _ → y' ≡ y) λ p → f (Rel Y ⊤ _ p) (rel y tt refl p)

----------------------------------------------------------------------
-- Units of measure example

record UOM : Set₁ where
  field
    U   : Set
    _·_ : U → U → U
    e1  : U

    -- group laws
    lunit : ∀ x → x ≡ (e1 · x)

    num  : U → Set
    _*n_ : ∀ {u₁ u₂} → num u₁ → num u₂ → num (u₁ · u₂)
    1n   : num e1
open UOM


postulate
    G    : |Set|
    _·G_  : G → G → G
    1G   : G

    law1 : ∀ x → x ≡ (1G ·G x)
    law : ∀ {u₁ u₂ x₁ x₂ y₁ y₂} → x₁ ≡ (u₁ ·G x₂) → y₁ ≡ (u₂ ·G y₂) → (x₁ ·G y₁) ≡ ((u₁ ·G u₂) ·G (x₂ ·G y₂))

plain-UOM : UOM
plain-UOM =
  record
    { U = ⊤; _·_ = λ _ _ → tt; e1 = tt; lunit = λ x → refl
    ; num = λ _ → G; _*n_ = _·G_; 1n = 1G }

-- The unit operations are scaling invariant
scaling-UOM : (p : 𝕀) → UOM
scaling-UOM p =
  let Num p u = Rel G G (λ x y → x ≡ (u ·G y)) p in
  record
    { U = G
    ; _·_ = _·G_
    ; e1 = 1G
    ; lunit = law1
    ; num = Num p
    ; _*n_ =
       elim-simple
         (λ x₁ x₂ rx →
           elim-simple
              (λ y₁ y₂ ry →
                  rel (x₁ ·G y₁) (x₂ ·G y₂) (law rx ry))
              (λ _ _ _ → refl)
              (λ _ _ _ → refl))
         (λ _ _ _ → refl)
         (λ _ _ _ → refl)
         p
    ; 1n = rel 1G 1G (law1 1G) p
    }

record True : Prop where
  constructor tt

-- Relating the unit-free to the unit-encumbered
erasure-UOM : (p : 𝕀) → UOM
erasure-UOM p =
  let Urel = Rel G ⊤ (λ x _ → True)
      unitmul = elim-simple
                 (λ u₁ _ _ →
                    elim-simple
                      (λ u₂ _ _ → rel (u₁ ·G u₂) tt tt)
                      (λ _ _ _ → refl)
                      (λ _ _ _ → refl))
                 (λ _ _ _ → refl)
                 (λ _ _ _ → refl)
      unit1 = rel 1G tt tt
  in
  record
    { U = Urel p
    ; _·_ = unitmul p
    ; e1 = unit1 p
    ; lunit = elim-prop (λ p x → x ≡ unitmul p (unit1 p) x)
               (λ a → law1 a)
               (λ a → refl)
               p
    ; num = λ _ → G
    ; _*n_ = _·G_
    ; 1n = 1G
    }

module _ (f : (M : UOM) → (u : M .U) → M .num u → M .num u) where

  --  a free scaling theorem
  scaling : ∀ g x →
            f (scaling-UOM src) g (g ·G x) ≡ (g ·G f (scaling-UOM src) g x)
  scaling g x =
     param G G (λ z z₁ → z ≡ (g ·G z₁)) λ p →
     f (scaling-UOM p) g (rel (g ·G x) x refl p)

  -- Units don't actually matter
  unit-irrelevance :
    ∀ g x →
    f (scaling-UOM src) g x ≡ f plain-UOM tt x
  unit-irrelevance g x =
    id-param λ p → f (erasure-UOM p) (rel g tt tt p) x