-
-
Save vpatryshev/9af0fb6223877229e688 to your computer and use it in GitHub Desktop.
a few operations with functors
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
package object types { | |
import scala.language.reflectiveCalls | |
import scala.language.higherKinds | |
// quantifiers aka (co)ends | |
type Forall[+F[_]] = { def apply[X]: F[X] } | |
type Exists[+F[_]] = F[_] | |
// basic categorical notions | |
type ~>[-F[_], +G[_]] = Forall[λ[ X => (F[X]=>G[X]) ]] | |
type Id[+X] = X | |
type Comp [F[ _], G[ _], X] = F[G[X]] | |
type CompPP[F[+_], G[+_], +X] = F[G[X]] | |
type CompPM[F[+_], G[-_], -X] = F[G[X]] | |
type CompMP[F[-_], G[+_], -X] = F[G[X]] | |
type CompMM[F[-_], G[-_], +X] = F[G[X]] | |
// Kan extensions | |
type Ran[-G[_], +H[_], +A] = Forall[λ[ B => ((A=>G[B])=>H[B]) ]] | |
type Lan[-G[_], +H[_], +A] = Exists[λ[ B => (G[B]=>A, H[B]) ]] | |
// TODO: Kan lifts, http://ncatlab.org/nlab/show/Kan+lift | |
// conversions to functor | |
type Yoneda[+F[_], +A] = Ran[Id, F, A] | |
type Coyoneda[+F[_], +A] = Lan[Id, F, A] | |
// monads via Kan exts | |
type Codensity[F[_], +A] = Ran[F, F, A] | |
type Density [F[_], +A] = Lan[F, F, A] | |
// basic (co)limit objects | |
type Initial = Forall[Id] // = `Nothing` | |
type Terminal = Exists[Id] // sorry, not `Unit` but `Any` (terminal in cat of subtypes) | |
// (co)inductive types, general | |
type FreeMonad [+F[_], +A] = Forall[λ[ X => ((A=>X, F[X]=>X)=>X) ]] | |
type CofreeComonad[+F[_], +A] = Exists[λ[ X => (X=>A, X=>F[X], X) ]] | |
// (co)inductive types, basic | |
// type InitialAlg[+F[_]] = FreeMonad[F, Initial] | |
// type TerminalCoalg[+F[_]] = CofreeComonad[F, Terminal] | |
type InitialAlg [+F[_]] = Forall[λ[ X => ((F[X]=>X)=>X) ]] | |
type TerminalCoalg[+F[_]] = Exists[λ[ X => (X=>F[X], X) ]] | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment