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 thatCodensity (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