Closed joneshf closed 6 years ago
Given this comment, maybe it should be Ran/Covariant/Type
? And also add Ran/Contravariant/Type
as:
(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ ∀(b : Type) → (f b → a) → g b
I think since it's a standalone concept and would just cause code duplication I'll merge as is. I believe Contravariant
and Covariant
idea just applies to things that have those distinguishable characteristics.
Oh, sorry for being unclear. The two are different.
Ran/Covariant/Type
∀(f : Type → Type) → ∀(g : Type → Type) → ∀(a : Type) → Type
λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ ∀(b : Type)
→ (a → f b)
→ g b
Ran/Contravariant/Type
∀(f : Type → Type) → ∀(g : Type → Type) → ∀(a : Type) → Type
λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ ∀(b : Type)
→ (f b → a)
→ g b
N.B. (a → f b)
vs. (f b → a)
.
The derived types end up being similarly defined, but over their variance:
Yoneda/Covariant/Type
∀(f : Type → Type) → ∀(a : Type) → Type
./../../Ran/Covariant/Type ./../../Id/Type
Yoneda/Contravariant/Type
∀(f : Type → Type) → ∀(a : Type) → Type
./../../Ran/Contravariant/Type ./../../Id/Type
It makes an impact in expressions like lift
and lower
Ran/Covariant/lift
∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀(a : Type)
→ ./../../Comonad/Type f
→ ./../../Functor/Type g
→ g a
→ ./Type f g a
λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ λ(comonad : ./../../Comonad/Type f)
→ λ(functor : ./../../Functor/Type g)
→ λ(x : g a)
→ λ(b : Type)
→ λ(k : a → f b)
→ functor.map a b (λ(y : a) → comonad.extract b (k y)) x
Ran/Contravariant/lift
∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀(a : Type)
→ ./../../Applicative/Type f
→ ./../../Contravariant/Type g
→ g a
→ ./Type f g a
λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ λ(applicative : ./../../Applicative/Type f)
→ λ(contravariant : ./../../Contravariant/Type g)
→ λ(x : g a)
→ λ(b : Type)
→ λ(k : f b → a)
→ contravariant.map a b (λ(y : b) → k (applicative.pure b y)) x
Ran/Covariant/lower
∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀(a : Type)
→ ./../../Applicative/Type f
→ ./Type f g a
→ g a
λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ λ(applicative : ./../../Applicative/Type f)
→ λ(ran : ./Type f g a)
→ ran a (applicative.pure a)
Ran/Contravariant/lower
∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀(a : Type)
→ ./../../Comonad/Type f
→ ./Type f g a
→ g a
λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ λ(comonad : ./../../Comonad/Type f)
→ λ(ran : ./Type f g a)
→ ran a (comonad.extract a)
I.e. Where one version requires Applicative f
, the other version requires Comonad f
. Similarly for Functor f
and Contravariant f
.
Ends up with a version of Codensity
, Yoneda
, etc for both covariant and contravariant types.
I'm down to submit a PR, if that seems useful.
Re: #30
First go an implementing
Ran f g a
. There's more that could be moved from Codensity/Yoneda, but requires some additional concepts. E.g.Applicative (Ran f g)
if we have a an isomorphism betweenf
andg
(or at leastforall (a : Type) -> f a -> g a
andforall (a : Type) -> g a -> f a
).Ran/lower
if we haveforall (a : Type) -> f a -> a
(I think).I didn't want to add these just things for the sake of redefining everything in terms of Ran, but can if they're wanted.
In any case, let me know if this is what we're thinking and if anything needs to change!