Last active
October 2, 2024 14:30
-
-
Save kory33/36305ff220b7bb78b74393a5357d0389 to your computer and use it in GitHub Desktop.
`Applicative` typeclass through `product`
This file contains hidden or 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
| //--- | |
| // laws defined in cats typeclasses | |
| // typeclasses: https://github.com/typelevel/cats/tree/29dd05a0282f51fda2e0f7d936250d6c0275bcf2/core/src/main/scala/cats | |
| // laws: https://github.com/typelevel/cats/tree/29dd05a0282f51fda2e0f7d936250d6c0275bcf2/laws/src/main/scala/cats/laws | |
| Functor => FunctorLaws#covariantIdentity := | |
| fa.map(identity) | |
| <-> fa | |
| Functor => FunctorLaws#covariantComposition := | |
| fa.map(f).map(g) | |
| <-> fa.map(f.andThen(g)) | |
| Apply => ApplyLaws#applyComposition := | |
| fbc.ap(fab.ap(fa)) | |
| <-> fbc.map(bc => (ab: A => B) => bc . ab).ap(fab).ap(fa) | |
| Apply => ApplyLaws#map2ProductConsistency := | |
| map2(fa, fb)(f) | |
| <-> product(fa, fb).map { case (a, b) => f(a, b) } | |
| Applicative => ApplicativeLaws#apProductConsistent := | |
| fab.ap(fa) | |
| <-> product(fab, fa).map { case (ab, a) => ab(a) } | |
| Applicative => ApplicativeLaws#applicativeMap := | |
| fa.map(f) <-> pure(f).ap(fa) | |
| //--- | |
| // additional assumptions on top of laws | |
| ApplicativeAssumption#productByAp := | |
| product(fa, fb) <-> fa.map(a => b => (a, b)).ap(fb) | |
| //--- | |
| // lemmata | |
| Aplicative => ApplicativeLemma#mapPure = | |
| pure(a).map(f) <-> pure(f(a)) | |
| Proof. | |
| pure(a).map(f) | |
| <-> { ApplicativeLaws#applicativeMap } | |
| pure(f).ap(pure(a)) | |
| <-> { ApplicativeLaws#applicativeHomomorphism } | |
| pure(f(a)) | |
| Applicative => ApplicativeLemma#apMapCommute = | |
| fab.ap(fb).map(bc) <-> fab.map(ab => bc . ab).ap(fb) | |
| Proof. | |
| fab.ap(fb).map(bc) | |
| <-> { ApplicativeLaws#applicativeMap } | |
| pure(bc).ap(fab.ap(fb)) | |
| <-> { ApplyLaws#applyComposition } | |
| pure(bc).map((bc1: B => C) => (ab: A => B) => bc1 . ab).ap(fab).ap(fa) | |
| <-> { ApplicativeLemma#mapPure } | |
| pure((ab: A => B) => bc . ab).ap(fab).ap(fa) | |
| <-> { ApplicativeLaws#applicativeMap } | |
| fab.map(ab => bc . ab).ap(fb) | |
| Applicative => ApplicativeLemma#apOfMap = | |
| fbc.ap(fa.map(ab)) <-> fbc.map(bc => bc . ab).ap(fa) | |
| Proof. | |
| fbc.ap(fa.map(ab)) | |
| <-> { ApplicativeLaws#applicativeMap } | |
| fbc.ap(pure(ab).ap(fa)) | |
| <-> { ApplyLaws#applyComposition } | |
| fbc.map((bc: B => C) => (ab: A => B) => bc . ab).ap(pure(ab)).ap(fa) | |
| <-> { ApplicativeLaws#applicativeInterchange } | |
| pure((abac: (A => B) => (A => C)) => abac(ab)).ap(fbc.map((bc: B => C) => (ab1: A => B) => bc . ab1)).ap(fa) | |
| <-> { ApplicativeLaws#applicativeMap } | |
| fbc.map((bc: B => C) => (ab1: A => B) => bc . ab1).map((abac: (A => B) => (A => C)) => abac(ab)).ap(fa) | |
| <-> { FunctorLaws#covariantComposition } | |
| fbc.map(bc => bc . ab).ap(fa) | |
| Applicative => ApplicativeLemma#productMapRCommute = | |
| product(fa, fb.map(bc)) | |
| <-> product(fa, fb).map { case (a, b) => (a, bc(b)) } | |
| Proof. | |
| product(fa, fb.map(bc)) | |
| <-> { ApplicativeAssumption#productByAp } | |
| fa.map(a => c => (a, c)).ap(fb.map(bc)) | |
| <-> { ApplicativeLemma#apOfMap } | |
| fa.map(a => c => (a, c)).map((cac: C => (A, C)) => cac . bc).ap(fb) | |
| <-> { FunctorLaws#covariantComposition } | |
| fa.map(a => ((cac: C => (A, C)) => cac . bc)(c => (a, c))).ap(fb) | |
| <-> fa.map(a => b => (a, bc(b))).ap(fb) | |
| <-> { ApplicativeLemma#apMapCommute } | |
| fa.map(a => b => (a, b)).ap(fb).map { case (a, b) => (a, bc(b)) } | |
| <-> { ApplicativeAssumption#productByAp } | |
| product(fa, fb).map { case (a, b) => (a, bc(b)) } | |
| Applicative => ApplicativeLemma#productMapLCommute = | |
| product(fa.map(ac), fb) | |
| <-> product(fa, fb).map { case (a, b) => (ac(a), b) } | |
| Proof. | |
| product(fa.map(ac), fb) | |
| <-> { ApplicativeAssumption#productByAp } | |
| fa.map(ac).map(c => b => (c, b)).ap(fb) | |
| <-> { FunctorLaws#covariantComposition } | |
| fa.map(a => b => (ac(a), b)).ap(fb) | |
| <-> { ApplicativeAssumption#productByAp } | |
| pure(a => b => (ac(a), b)).ap(fa).ap(fb) | |
| <-> { ApplicativeLaws#applicativeMap } | |
| fa.map(a => b => (ac(a), b)).ap(fb) | |
| <-> fa.map(a => { case (a, b) => (ac(a), b) } . (b => (a, b))).ap(fb) | |
| <-> { ApplicativeLemma#apMapCommute } | |
| fa.map(a => b => (a, b)).ap(fb).map { case (a, b) => (ac(a), b) } | |
| <-> { ApplicativeAssumption#productByAp } | |
| product(fa, fb).map { case (a, b) => (ac(a), b) } | |
| Applicative => ApplicativeLemma#productRProduct = | |
| fbc.ap(fab.ap(fa)) | |
| <-> product(fbc, product(fab, fa)).map { case (bc, (ab, a)) => bc(ab(a)) } | |
| Proof. | |
| fbc.ap(fab.ap(fa)) | |
| <-> { ApplicativeLaws#apProductConsistent } | |
| product(fbc, fab.ap(fa)).map { case (bc, b) => bc(b) } | |
| <-> { ApplicativeLaws#apProductConsistent } | |
| product(fbc, product(fab, fa).map { case (ab, a) => ab(a) }).map { case (bc, b) => bc(b) } | |
| <-> { ApplicativeLemma#productMapRCommute } | |
| product(fbc, product(fab, fa)).map { case (bc, (ab, a)) => (bc, ab(a)) }.map { case (bc, b) => bc(b) } | |
| <-> { FunctorLaws#covariantComposition } | |
| product(fbc, product(fab, fa)).map { case (bc, (ab, a)) => bc(ab(a)) } | |
| Applicative => ApplicativeLemma#productLProduct = | |
| fbc.map(bc => (ab: A => B) => bc . ab).ap(fab).ap(fa) | |
| <-> product(product(fbc, fab), fa).map { case ((bc, ab), a) => bc(ab(a)) } | |
| Proof. | |
| fbc.map(bc => (ab: A => B) => bc . ab).ap(fab).ap(fa) | |
| <-> { ApplicativeLaws#apProductConsistent } | |
| product(fbc.map(bc => (ab: A => B) => bc . ab), fab).map { case (abac, ab) => abac(ab) }.ap(fa) | |
| <-> { ApplicativeLaws#apProductConsistent } | |
| product(product(fbc.map(bc => (ab: A => B) => bc . ab), fab).map { case (abac, ab) => abac(ab) }, fa).map { case (ac, a) => ac(a) } | |
| <-> { ApplicativeLemma#productMapLCommute } | |
| product(product(fbc, fab).map { case (bc, ab) => ((ab1: A => B) => bc . ab1, ab) }.map { case (abac, ab) => abac(ab) }, fa).map { case (ac, a) => ac(a) } | |
| <-> { FunctorLaws#covariantComposition } | |
| product(product(fbc, fab).map { case (bc, ab) => bc . ab }, fa).map { case (ac, a) => ac(a) } | |
| <-> { ApplicativeLemma#productMapLCommute } | |
| product(product(fbc, fab), fa).map { case ((bc, ab), a) => (bc . ab, a) }.map { case (ac, a) => ac(a) } | |
| <-> { FunctorLaws#covariantComposition } | |
| product(product(fbc, fab), fa).map { case ((bc, ab), a) => bc(ab(a)) } | |
| //--- | |
| // equivalence statement | |
| Applicative => ApplyLaws#applyComposition | |
| = fbc.ap(fab.ap(fa)) <-> fbc.map(bc => (ab: A => B) => bc . ab).ap(fab).ap(fa) | |
| ⇔ { ApplicativeLemma#productLProduct, ApplicativeLemma#productRProduct } | |
| product(fbc, product(fab, fa)).map { case (bc, (ab, a)) => bc(ab(a)) } | |
| <-> product(product(fbc, fab), fa).map { case ((bc, ab), a) => bc(ab(a)) } | |
| ⇔ { | |
| ⇒ product(fa, product(fb, fc)).map { case (a, (b, c)) => (a, b, c) } | |
| <-> { FunctorLaws#covariantComposition } | |
| product(fa, product(fb, fc)).map { (a, (b, c)) => ({ case (b1, c1) => (a, b1, c1) }, (b, c))}.map { case (bcadc, (b, c)) => (bcadc, (c1 => (b, c1), c)) }.map { case (bcabc, (cbc, c)) => bcabc(cbc(c)) } | |
| <-> { ApplicativeLemma#productMapLCommute } | |
| product(fa.map(a => { case (b, c) => (a, b, c) }), product(fb, fc)).map { case (bcadc, (b, c)) => (bcadc, (c1 => (b, c1), c)) }.map { case (bcabc, (cbc, c)) => bcabc(cbc(c)) } | |
| <-> { ApplicativeLemma#productMapRCommute } | |
| product(fa.map(a => { case (b, c) => (a, b, c) }), product(fb, fc).map { case (b, c) => (c1 => (b, c1), c) }).map { case (bcabc, (cbc, c)) => bcabc(cbc(c)) } | |
| <-> { ApplicativeLemma#productMapLCommute } | |
| product(fa.map(a => { case (b, c) => (a, b, c) }), product(fb.map(b => c => (b, c)), fc)).map { case (bcabc, (cbc, c)) => bcabc(cbc(c)) } | |
| <-> { assumption } | |
| product(product(fa.map(a => { case (b, c) => (a, b, c) }), fb.map(b => c => (b, c))), fc).map { case ((bcabc, cbc), c) => bcabc(cbc(c)) } | |
| <-> { ApplicativeLemma#productMapLCommute } | |
| product(product(fa, fb.map(b => c => (b, c))).map { case (a, cbc) => ({ case (b, c) => (a, b, c) }, cbc) }, fc).map { case ((bcabc, cbc), c) => bcabc(cbc(c)) } | |
| <-> { ApplicativeLemma#productMapLCommute } | |
| product(product(fa, fb.map(b => c => (b, c))), fc).map { case ((a, cbc), c) => (({ case (b, c1) => (a, b, c1) }, cbc), c) }.map { case ((bcabc, cbc), c) => bcabc(cbc(c)) } | |
| <-> { ApplicativeLemma#productMapRCommute } | |
| product(product(fa, fb).map { case (a, b) => (a, c => (b, c)) }, fc).map { case ((a, cbc), c) => (({ case (b, c1) => (a, b, c1) }, cbc), c) }.map { case ((bcabc, cbc), c) => bcabc(cbc(c)) } | |
| <-> { ApplicativeLemma#productMapRCommute } | |
| product(product(fa, fb), fc).map { case ((a, b), c) => ((a, c1 => (b, c1)), c) }.map { case ((a, cbc), c) => (({ case (b, c1) => (a, b, c1) }, cbc), c) }.map { case ((bcabc, cbc), c) => bcabc(cbc(c)) } | |
| <-> { FunctorLaws#covariantComposition } | |
| product(product(fa, fb), fc).map { case ((a, b), c) => (a, b, c) } | |
| ⇐ product(fbc, product(fab, fa)).map { case (bc, (ab, a)) => bc(ab(a)) } | |
| <-> { FunctorLaws#covariantComposition } | |
| product(fbc, product(fab, fa)).map { case (bc, (ab, a)) => (bc, ab, a) }.map { case (bc, ab, a) => bc(ab(a)) } | |
| <-> { assumption } | |
| product(product(fbc, fab), fa).map { case ((bc, ab), a) => (bc, ab, a) }.map { case (bc, ab, a) => bc(ab(a)) } | |
| <-> { FunctorLaws#covariantComposition } | |
| product(product(fbc, fab), fa).map { case ((bc, ab), a) => bc(ab(a)) } | |
| } | |
| product(fa, product(fb, fc)).map { case (a, (b, c)) => (a, b, c) } | |
| <-> product(product(fa, fb), fc).map { case ((a, b), c) => (a, b, c) } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment