#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_homomorp... 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