[GHC] #12477: Allow left sectioning and tuple sectioning of types

[GHC]

#12477: Allow left sectioning and tuple sectioning of types
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  Iceland_jack
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by Iceland_jack:

@@ -82,0 +82,9 @@
+
+ **Edit**: Yoneda becomes
+
+ {{{#!hs
+ type f ~> g = forall xxx. f xxx -> g xxx
+
+ --   Yoneda f a = ((->) a) ~> f
+ type Yoneda f a = (a ->) ~> f
+ }}}

New description:

 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:
 >
 > — [http://comonad.com/reader/2012/unnatural-transformations-and-
 quantifiers/ The Comonad.Reader] on Unnatural Transformations and
 Quantifiers

 === Visible type application ===
 Makes visible type application seem nicer:

 {{{#!hs
 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 ===
 {{{#!hs
 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
 {{{#!hs
 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

 {{{#!hs
 type f ~> g = forall xxx. f xxx -> g xxx

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

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12477#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler