Allow left sectioning and tuple sectioning of types

Simple syntactic change that would be fine to have, allow writing the type (•) r as (r •). Just getting a discussion going

Usage

Used briefly in

This gives rise to the monad S -> (-, S) the state monad. According to the facts above, we should have that Codensity (s ->) (excuse the sectioning) is the same as state, and if we look, we see:

— The Comonad.Reader on Unnatural Transformations and Quantifiers

Visible type application

Makes visible type application seem nicer:

fmap @_ @_ @((:-) _) :: (b :- b') -> (a :- b) -> (a :- b')
fmap @_ @_ @((->) _) :: (b -> b') -> (a -> b) -> (a -> b')
-- vs
fmap @_ @_ @(_ :-) :: (b :- b') -> (a :- b) -> (a :- b')
fmap @_ @_ @(_ ->) :: (b -> b') -> (a -> b) -> (a -> b')

Examples

instance Functor   ((->) r) 
instance Functor   ((,) a)
instance Copointed ((,,) a b)
instance Copointed ((,,) a b c)

instance Magnify ((->) b) ((->) a) b a where
type instance Key ((:->:) a) = a
instance HasTrie e => Lookup  ((:->:) e) where
instance Memo    a => Functor ((~>) a)   where

instance Functor ((&) a) where
  type Dom ((&) a) = (:-)
  type Cod ((&) a) = (:-)

instance Functor ((:-) a) where
  type Dom ((:-) a) = (:-)
  type Cod ((:-) a) = (->)
  fmap = (.)

instance Functor ((:~:) a) where
  type Dom ((:~:) a) = (:~:)
  type Cod ((:~:) a) = (->)
  fmap = (.)

instance Adjunction ((,)a) ((->)a) (->) (->) where

becomes

instance Functor   (r ->) 
instance Functor   (a,)
instance Copointed (a, b,)
instance Copointed (a, b, c,)

instance Magnify (b ->) (a ->) b a where
type instance Key (a :->:) = a
instance HasTrie e => Lookup  (e :->:) where
instance Memo    a => Functor (a ~>)   where

instance Functor (a &) where
  type Dom (a &) = (:-)
  type Cod (a &) = (:-)

instance Functor (a :-) where
  type Dom (a :-) = (:-)
  type Cod (a :-) = (->)
  fmap = (.)

instance Functor (a :~:) where
  type Dom (a :~:) = (:~:)
  type Cod (a :~:) = (->)
  fmap = (.)
instance Adjunction (a ,) (a ->) (->) (->) where

• *Edit**: Yoneda becomes

type f ~> g = forall xxx. f xxx -> g xxx

--   Yoneda f a = ((->) a) ~> f
type Yoneda f a = (a ->) ~> f