[GHC] #12363: Type application for infix

[GHC]

#12363: Type application for infix
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  lowest            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
  (Parser)                           |             Keywords:
      Resolution:                    |  TypeApplications
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 > The member function `lift` embeds a computation in monad ''m'' into a
 monad ''t m''. Furthermore, we expect a monad transformer to ''add''
 features, without changing the nature of an existing omputation. We
 introduce ''Monad Transformer Laws'' to capture the properties of `lift`:
 >
 >
 > {{{
 >   lift · unit_m
 > = unit_tm
 >
 >   lift (m `bind_m` k)
 > = lift m `bind_tm` (lift · k)
 > }}}
 >
 > The above laws say that lifting a null computation results in a null
 computation, and that lifting a sequence of computations is equivalent to
 first lifting them individually, and then combining them in the lifted
 monad.
 >
 > — [http://haskell.cs.yale.edu/wp-content/uploads/2011/02/POPL96-Modular-
 interpreters.pdf Monad Transformers and Modular Interpreters]

 This effectively uses a different formulation of `MonadTrans` with a
 `Monad` constraint on ''t m'' (see
 [https://www.reddit.com/r/haskell/comments/50rxci/edward_kmett_monad_homomorphisms_google_tech_talk/
 this])

 {{{#!hs
 class (Monad m, Monad (t m)) => MonadT t m where
   lift :: m a -> (t m) a
 }}}

 It preserves `pure` if these functions are equal

 {{{#!hs
 pure1, pure2 :: forall t m a. MonadT t m => a -> (t m) a
 pure1 = lift . pure @m
 pure2 = pure @(t m)
 }}}

 and with infix type application we can express the preservation of
 ''bind'' with the following two equations:

 {{{#!hs
 bind1, bind2 :: forall t m a b. MonadT t m => (a -> m b) -> (m a -> (t m)
 b)
 bind1 k m = lift (m >>= @m k)
 bind2 k m = lift m >>= @(t m) (lift . k)
 }}}

 without awkwardly infixiaticate it

 {{{#!hs
 bind1 k m = lift ((>>=) @m m k)
 bind2 k m = (>>=) @(t m) (lift m) (lift . k)
 }}}

 ----

 We can of course be even more explicit

 {{{#!hs
 bind1, bind2 :: forall t m a b. MonadT t m => (a -> m b) -> (m a -> (t m)
 b)
 bind1 k m = lift @t @m @b (m >>= @m @a @b k)
 bind2 k m = lift @t @m @a m >>= @(t m) @a @b (lift @t @m @b . k)
 }}}

 whatevs

 {{{#!hs
 lift_ :: forall tm a t m. ((t m ~ tm), MonadT t m) => m a -> t m a
 lift_ = lift

 bind1, bind2 :: forall t m a b. Monad_ t m => (a -> m b) -> (m a -> (t m)
 b)
 bind1 k m = lift_ @(t m) @b (m >>= @m @a @b k)

 bind2 k m = lift_ @(t m) @a m >>= @(t m) @a @b (lift_ @(t m) @b . k)
 }}}

 ----

 Similarly we can write down the laws for other monad morphisms:

 {{{#!hs
 foo1, foo2 :: forall m a. MonadIO m => a -> m a
 foo1 = pure @m
 foo2 = liftIO . pure @IO

 bind1, bind2 :: forall m a b. MonadIO m => (a -> IO b) -> (IO a -> m b)
 bind1 k m = liftIO ((>>=) @IO m k)
 bind2 k m = (>>=) @m (liftIO m) (liftIO . k)
 }}}

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