Created
September 27, 2018 01:02
-
-
Save ocharles/252bc296b659aa32e915e02d02537064 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# language ConstraintKinds #-} | |
{-# language FlexibleContexts #-} | |
{-# language FlexibleInstances #-} | |
{-# language GADTs #-} | |
{-# language MultiParamTypeClasses #-} | |
{-# language GeneralizedNewtypeDeriving #-} | |
{-# language RankNTypes #-} | |
{-# language QuantifiedConstraints #-} | |
{-# language TypeApplications #-} | |
{-# language TypeOperators #-} | |
{-# language UndecidableInstances #-} | |
module Cat where | |
import Prelude hiding ((.), id) | |
import Control.Category | |
import Control.Monad.IO.Class | |
import Control.Monad.Trans.Reader | |
-- LIBRARY | |
{- | |
Traditionally, we use free monads by defining a functor of operations, and then | |
using this to generate a monad: | |
data TeletypeF a = GetLine ( String -> a ) | PutLine a | |
type Teletype = Free TeletypeF | |
Russell O'Connor showed us that there is another free monad, the "van Laarhoven" | |
free monad: | |
data TeletypeOps m = TeletypeOps { getChar :: m Char; putChar :: Char -> m () } | |
type Teletype = VLMonad TeletypeOps | |
where | |
newtype VLMonad ops a = VLMonad { runVLMonad :: forall m. Monad m => ops m -> m a | |
This can be compared to explicit dictionary passing with mtl, where we would have | |
class MonadTeletype where | |
getChar :: m Char | |
putChar :: Char -> m () | |
In discussions around this [1], Tom Ellis points out that | |
forall m. MonadTeletype m => m a essentially *is* a free monad in its own right. | |
This work briefly explores this idea a little further by looking at natural | |
transformations of these mtl-y free monads. | |
[1]: https://www.reddit.com/r/haskell/comments/1xk8rr/after_lenses_come_free_monads_the_van_laarhoven/ | |
-} | |
newtype Free c a = Free { unFree :: forall m. c m => m a } | |
-- Somewhat amazing that this works. The same idea can be extended to | |
-- Applicative, Monad, etc. | |
instance ( forall m. c m => Functor m ) => Functor ( Free c ) where | |
fmap f ( Free m ) = | |
Free ( fmap f m ) | |
x <$ Free m = | |
Free (x <$ m) | |
-- | Natural transformations of "mtl free monads". | |
newtype c :~> c' = | |
Handle | |
{ ($$) :: forall a. ( forall m. c m => m a ) -> ( forall n. c' n => n a ) } | |
infixr 0 $$ | |
-- | "Classy" natural transformations can be composed and have an identity. | |
instance Category (:~>) where | |
id = | |
Handle ( \m -> m ) | |
Handle f . Handle g = | |
Handle ( \m -> f ( g m ) ) | |
-- Extensible effects time! EFF acts like "member" in most extensible effect | |
-- frameworks - it adds the constraint that @m@ supports the effect @c@. In | |
-- our case, the effect signature is simply an MTL class. | |
class EFF c m where | |
-- "Sending" an effect into the free monad is a monad homomorphism from | |
-- the free monad generated by c into m. | |
send :: Free c a -> m a | |
-- One way to implement extensible effects is to use a reader monad of | |
-- natural transformations from source effects into the constraints | |
-- required by their implementation (e.g., mapping everything to MonadIO). | |
-- | |
-- It's easy to extend this to do type directed resolution in a record | |
-- of handlers, for example. Here, I'm just stating that only one | |
-- effect can be handled. | |
instance ( Monad m, y ( ReaderT ( x :~> y ) m ), c ~ x ) => EFF c ( ReaderT ( x :~> y ) m ) where | |
send ( Free m ) = | |
ask >>= \handle -> handle $$ m | |
dispatchEffects :: handlers -> ReaderT handlers m a -> m a | |
dispatchEffects = | |
flip runReaderT | |
-- EXAMPLE | |
-- Define a monadic effect. | |
class MonadFoo m where | |
foo :: m () | |
-- Define a "reinterpreter" - this reinterprets MonadFoo into MonadLog. | |
newtype FooT m a = FooT { unFooT :: m a } | |
deriving ( Functor, Applicative, Monad, MonadIO ) | |
instance MonadLog m => MonadFoo ( FooT m ) where | |
foo = FooT (logMsg "Foo") | |
-- And so we'll also need MonadLog. | |
class Monad m => MonadLog m where | |
logMsg :: String -> m () | |
-- A reinterpreter down to MonadIO. | |
newtype LoggingT m a = LoggingT { runLoggingT :: m a } | |
deriving ( Functor, Applicative, Monad, MonadIO ) | |
instance MonadIO m => MonadLog (LoggingT m) where | |
logMsg = liftIO . putStrLn | |
-- FooT and LoggingT eliminators are classy natural transformations. | |
fooToLog :: MonadFoo :~> MonadLog | |
fooToLog = Handle unFooT | |
logToIO :: MonadLog :~> MonadIO | |
logToIO = Handle runLoggingT | |
-- We can compose them to handle MonadFoo directly in MonadIO: | |
fooToIO :: MonadFoo :~> MonadIO | |
fooToIO = logToIO . fooToLog | |
-- A test program in MonadFoo... | |
testProgram :: EFF MonadFoo m => m () | |
testProgram = send @MonadFoo ( Free foo ) | |
-- Can be ran in IO by composing fooToLog and logToIO | |
main :: IO () | |
main = | |
dispatchEffects fooToIO testProgram |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment