Skip to content

Instantly share code, notes, and snippets.

@bobatkey

bobatkey/param.agda

Last active June 23, 2020 16:20
Show Gist options
  • Save bobatkey/7861009f7d28d568eec8f8c32dd07b28 to your computer and use it in GitHub Desktop.
Save bobatkey/7861009f7d28d568eec8f8c32dd07b28 to your computer and use it in GitHub Desktop.
Download ZIP
Axiomatising parametricity in Agda via rewrite rules, with a units of measure example
Raw
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment