traversable.md

Traversableに激似の抽象化たちを整理してみた

		tはどんな関手	とる	返す
Traversable t	traverse	$\mathrm{Hask} \to \mathrm{Hask}$	Star f a b	Star f (t a) (t b)
PTraversable t	ptraverse	$\mathrm{Hask} \to \mathrm{Hask}$	p a b	p (t a) (t b)
Bitraversable t	bitraverse	$\mathrm{Hask}^2 \to \mathrm{Hask}$	Star2 f a₁ a₂ b₁ b₂	Star f (t a₁ a₂) (t b₁ b₂)
Rank2.Traversable t	Rank2.traverse	$\mathrm{Hask}^k \to \mathrm{Hask}$	IxStar f a b	Star f (t a) (t b)
	traverseBia	$\mathrm{Hask} \to \mathrm{Hask}$	Fork p a b₁ b₂	Fork p (t a) (t b₁) (t b₂)

class Profunctor p => Cartesian p where
    prounit :: p () ()
    promult :: p a b -> p a' b' -> p (a,a') (b,b')
    
    provoid :: p Void Void
    prosum  :: p a b -> p a' b' -> p (Either a a') (Either b b')

newtype Star f a b = Star (a -> f b)

instance Functor f => Profunctor (Star f)
instance Applicative f => Cartesian (Star f)

-- A morphism in the category Hask^2
type Hask2 a₁ a₂ b₁ b₂ = (a₁ -> b₁, a₂ -> b₂)

-- Profunctor on Hask^2
newtype Star2 f a₁ a₂ b₁ b₂ = Star2 (Hask2 a₁ a₂ (f b₁) (f b₂))
dimapStar2 :: Functor f => Hask2 a₁ a₂ b₁ b₂ -> Hask2 c₁ c₂ d₁ d₂ -> Star2 f b₁ b₂ c₁ c₂ -> Star2 f a₁ a₂ d₁ d₂

-- If `f` is an Applicative, `Star2 f` is a kind of `Cartesian` which is for `Hask^2`

-- A morphism in the category Hask^k, the category of types indexed by k.
type (~>) :: (k -> Type) -> (k -> Type) -> Type
type f ~> g = forall x. f x -> g x

-- Profunctor on Hask^k
type IxProfunctor :: ((k -> Type) -> (k -> Type) -> Type) -> Constraints
class IxProfunctor p where
	ixdimap :: (f' ~> f) -> (g ~> g') -> p f g -> p f' g'

class IxCartesian p where
    ixprounit :: p U1 U1
    ixpromult :: p a b -> p a' b' -> p (a :*: a') (b :*: b')
    
    ixprovoid :: p V1 V1
    ixprosum  :: p a b -> p a' b' -> p (a :+: a') (b :+: b')

type IxStar :: (Type -> Type) -> (k -> Type) -> (k -> Type) -> Type
newtype IxStar f a b = IxStar (forall x. a x -> f (b x))

instance Functor f => IxProfunctor (IxStar f) where ...
instance Applicative f => IxCartesian (IxStar f) where ...

Fork is a profunctor $\mathrm{Hask}^{\mathrm{op}} \times \mathrm{Hask}^2 \to \mathrm{Hask}$.

newtype Fork p a b₁ b₂ = Fork (a -> p b₁ b₂)