Last active
August 21, 2020 21:57
-
-
Save Kazark/297598ded07cdae2b093ffd73461d136 to your computer and use it in GitHub Desktop.
Lawfulness of applicative implementations than compile for homogenous pair
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Two where | |
open import Level using (Level) | |
open import Function using (_∘_; id; _$_) | |
import Relation.Binary.PropositionalEquality as Eq | |
open Eq using (_≡_; refl; cong) | |
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎; step-≡; step-≡˘) | |
data Two (A : Set) : Set where | |
TwoOf : A → A → Two A | |
pure : ∀{a : Set} → a → Two a | |
pure x = TwoOf x x | |
-- ONE (lawful) | |
infixl 5 _<*>¹_ | |
_<*>¹_ : ∀{a : Set}{b : Set} → Two (a → b) → Two a → Two b | |
_<*>¹_ (TwoOf f g) (TwoOf x y) = TwoOf (f x) (g y) | |
identity¹ : ∀{a : Set} → (v : Two a) → pure id <*>¹ v ≡ v | |
identity¹ (TwoOf _ _) = refl | |
composition¹ : ∀{a b c : Set} → (u : Two (b → c)) → (v : Two (a → b)) → (w : Two a) | |
→ pure (\f g x → f (g x)) <*>¹ u <*>¹ v <*>¹ w ≡ u <*>¹ (v <*>¹ w) | |
composition¹ (TwoOf _ _) (TwoOf _ _) (TwoOf _ _) = refl | |
homomorphism¹ : ∀{a b : Set} → (f : a → b) → (x : a) | |
→ pure f <*>¹ pure x ≡ pure (f x) | |
homomorphism¹ _ _ = refl | |
interchange¹ : ∀{a b : Set} → (u : Two (a → b)) → (y : a) | |
→ u <*>¹ pure y ≡ pure (_$ y) <*>¹ u | |
interchange¹ (TwoOf _ _) _ = refl | |
-- TWO (unlawful?) | |
infixl 5 _<*>²_ | |
_<*>²_ : ∀{a : Set}{b : Set} → Two (a → b) → Two a → Two b | |
_<*>²_ (TwoOf f g) (TwoOf x y) = TwoOf (g x) (f y) | |
identity² : ∀{a : Set} → (v : Two a) → pure id <*>² v ≡ v | |
identity² (TwoOf _ _) = refl | |
composition² : ∀{a b c : Set} → (u : Two (b → c)) → (v : Two (a → b)) → (w : Two a) | |
→ pure (\f g x → f (g x)) <*>² u <*>² v <*>² w ≡ u <*>² (v <*>² w) | |
composition² (TwoOf _ _) (TwoOf _ _) (TwoOf _ _) = {!!} -- looks unlawful | |
homomorphism² : ∀{a b : Set} → (f : a → b) → (x : a) | |
→ pure f <*>² pure x ≡ pure (f x) | |
homomorphism² _ _ = refl | |
interchange² : ∀{a b : Set} → (u : Two (a → b)) → (y : a) | |
→ u <*>² pure y ≡ pure (_$ y) <*>² u | |
interchange² (TwoOf _ _) _ = {!!} -- looks unlawful | |
-- THREE (unlawful?) | |
infixl 5 _<*>³_ | |
_<*>³_ : ∀{a : Set}{b : Set} → Two (a → b) → Two a → Two b | |
_<*>³_ (TwoOf f _) (TwoOf x y) = TwoOf (f x) (f y) | |
identity³ : ∀{a : Set} → (v : Two a) → pure id <*>³ v ≡ v | |
identity³ (TwoOf _ _) = refl | |
-- FOUR (unlawful?) | |
infixl 5 _<*>⁴_ | |
_<*>⁴_ : ∀{a : Set}{b : Set} → Two (a → b) → Two a → Two b | |
_<*>⁴_ (TwoOf _ g) (TwoOf x y) = TwoOf (g x) (g y) | |
identity⁴ : ∀{a : Set} → (v : Two a) → pure id <*>⁴ v ≡ v | |
identity⁴ (TwoOf _ _) = refl | |
-- ETC (unlawful?) | |
{- There seem to be 12 other ways to implement this that would typecheck. | |
-- For each of the variations above, you could: | |
-- 1. Only make use of x (4 more) | |
-- 2. Only make use of y (4 more) | |
-- 3. Invert the final two subexpressions (4 more) | |
-} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment