From d5393e72aa787acb71fff3137db304959fd1dd38 Mon Sep 17 00:00:00 2001 From: Eric Easley Date: Tue, 15 Nov 2016 19:23:19 -0800 Subject: [PATCH 1/5] Make `Union` visible in through an `Internal` module --- freer.cabal | 1 + src/Data/Open/Union.hs | 44 +++------------------------------ src/Data/Open/Union/Internal.hs | 44 +++++++++++++++++++++++++++++++++ 3 files changed, 48 insertions(+), 41 deletions(-) create mode 100644 src/Data/Open/Union/Internal.hs diff --git a/freer.cabal b/freer.cabal index 5979794..ffc3f3c 100644 --- a/freer.cabal +++ b/freer.cabal @@ -48,6 +48,7 @@ library , Control.Monad.Freer.Writer , Data.FTCQueue , Data.Open.Union + , Data.Open.Union.Internal build-depends: base >=4.7 && <5 hs-source-dirs: src diff --git a/src/Data/Open/Union.hs b/src/Data/Open/Union.hs index d84f424..5ffede0 100644 --- a/src/Data/Open/Union.hs +++ b/src/Data/Open/Union.hs @@ -31,22 +31,16 @@ starting point. -} module Data.Open.Union ( - Union, - decomp, - weaken, - Member(..), - Members + module Data.Open.Union, + Union ) where import GHC.Exts +import Data.Open.Union.Internal -------------------------------------------------------------------------------- -- Interface -- -------------------------------------------------------------------------------- -data Union (r :: [ * -> * ]) v where - UNow :: t v -> Union (t ': r) v - UNext :: Union r v -> Union (any ': r) v - {-# INLINE decomp #-} decomp :: Union (t ': r) v -> Either (Union r v) (t v) decomp (UNow x) = Right x @@ -68,35 +62,3 @@ type family Members m r :: Constraint where Members (t ': c) r = (Member t r, Members c r) Members '[] r = () --------------------------------------------------------------------------------- - -- Implementation -- --------------------------------------------------------------------------------- -data Nat = S Nat | Z -data P (n :: Nat) = P - --- injecting/projecting at a specified position P n -class Member' t r (n :: Nat) where - inj' :: P n -> t v -> Union r v - prj' :: P n -> Union r v -> Maybe (t v) - -instance (r ~ (t ': r')) => Member' t r 'Z where - inj' _ = UNow - prj' _ (UNow x) = Just x - prj' _ _ = Nothing - -instance (r ~ (t' ': r'), Member' t r' n) => Member' t r ('S n) where - inj' _ = UNext . inj' (P::P n) - prj' _ (UNow _) = Nothing - prj' _ (UNext x) = prj' (P::P n) x - --- Find an index of an element in a `list' --- The element must exist --- This closed type family disambiguates otherwise overlapping --- instances -type family FindElem (t :: * -> *) r :: Nat where - FindElem t (t ': r) = 'Z - FindElem t (any ': r) = 'S (FindElem t r) - -type family EQU (a :: k) (b :: k) :: Bool where - EQU a a = 'True - EQU a b = 'False diff --git a/src/Data/Open/Union/Internal.hs b/src/Data/Open/Union/Internal.hs new file mode 100644 index 0000000..4415e91 --- /dev/null +++ b/src/Data/Open/Union/Internal.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DataKinds, PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Open.Union.Internal where + +data Union (r :: [ * -> * ]) v where + UNow :: t v -> Union (t ': r) v + UNext :: Union r v -> Union (any ': r) v + +data Nat = S Nat | Z +data P (n :: Nat) = P + +-- injecting/projecting at a specified position P n +class Member' t r (n :: Nat) where + inj' :: P n -> t v -> Union r v + prj' :: P n -> Union r v -> Maybe (t v) + +instance (r ~ (t ': r')) => Member' t r 'Z where + inj' _ = UNow + prj' _ (UNow x) = Just x + prj' _ _ = Nothing + +instance (r ~ (t' ': r'), Member' t r' n) => Member' t r ('S n) where + inj' _ = UNext . inj' (P::P n) + prj' _ (UNow _) = Nothing + prj' _ (UNext x) = prj' (P::P n) x + +-- Find an index of an element in a `list' +-- The element must exist +-- This closed type family disambiguates otherwise overlapping +-- instances +type family FindElem (t :: * -> *) r :: Nat where + FindElem t (t ': r) = 'Z + FindElem t (any ': r) = 'S (FindElem t r) + +type family EQU (a :: k) (b :: k) :: Bool where + EQU a a = 'True + EQU a b = 'False + From 42604669292e093e41005792791f89a772fa518c Mon Sep 17 00:00:00 2001 From: Eric Easley Date: Tue, 15 Nov 2016 22:54:41 -0800 Subject: [PATCH 2/5] Add `extract` for safely extracting final element from union --- README.md | 9 ++++----- examples/src/Teletype.hs | 18 ++++++++---------- src/Control/Monad/Freer/Internal.hs | 6 +++--- src/Control/Monad/Freer/Trace.hs | 5 ++--- src/Data/Open/Union.hs | 6 +++++- src/Data/Open/Union/Internal.hs | 4 ++-- 6 files changed, 24 insertions(+), 24 deletions(-) diff --git a/README.md b/README.md index b9221c7..47e6423 100644 --- a/README.md +++ b/README.md @@ -57,11 +57,10 @@ exitSuccess' = send ExitSuccess -------------------------------------------------------------------------------- runTeletype :: Eff '[Teletype] w -> IO w runTeletype (Val x) = return x -runTeletype (E u q) = case decomp u of - Right (PutStrLn msg) -> putStrLn msg >> runTeletype (qApp q ()) - Right GetLine -> getLine >>= \s -> runTeletype (qApp q s) - Right ExitSuccess -> exitSuccess - Left _ -> error "This cannot happen" +runTeletype (E u q) = case extract u of + (PutStrLn msg) -> putStrLn msg >> runTeletype (qApp q ()) + GetLine -> getLine >>= \s -> runTeletype (qApp q s) + ExitSuccess -> exitSuccess -------------------------------------------------------------------------------- -- Pure Interpreter -- diff --git a/examples/src/Teletype.hs b/examples/src/Teletype.hs index 2c92891..432bbfa 100644 --- a/examples/src/Teletype.hs +++ b/examples/src/Teletype.hs @@ -30,11 +30,10 @@ exitSuccess' = send ExitSuccess -------------------------------------------------------------------------------- runTeletype :: Eff '[Teletype] w -> IO w runTeletype (Val x) = return x -runTeletype (E u q) = case decomp u of - Right (PutStrLn msg) -> putStrLn msg >> runTeletype (qApp q ()) - Right GetLine -> getLine >>= \s -> runTeletype (qApp q s) - Right ExitSuccess -> exitSuccess - Left _ -> error "This cannot happen" +runTeletype (E u q) = case extract u of + (PutStrLn msg) -> putStrLn msg >> runTeletype (qApp q ()) + GetLine -> getLine >>= \s -> runTeletype (qApp q s) + ExitSuccess -> exitSuccess -------------------------------------------------------------------------------- -- Pure Interpreter -- @@ -44,8 +43,7 @@ runTeletypePure inputs req = reverse (go inputs req []) where go :: [String] -> Eff '[Teletype] w -> [String] -> [String] go _ (Val _) acc = acc go [] _ acc = acc - go (x:xs) (E u q) acc = case decomp u of - Right (PutStrLn msg) -> go (x:xs) (qApp q ()) (msg:acc) - Right GetLine -> go xs (qApp q x) acc - Right ExitSuccess -> go xs (Val ()) acc - Left _ -> go xs (Val ()) acc + go (x:xs) (E u q) acc = case extract u of + (PutStrLn msg) -> go (x:xs) (qApp q ()) (msg:acc) + GetLine -> go xs (qApp q x) acc + ExitSuccess -> go xs (Val ()) acc diff --git a/src/Control/Monad/Freer/Internal.hs b/src/Control/Monad/Freer/Internal.hs index 51ab4e5..30f11ce 100644 --- a/src/Control/Monad/Freer/Internal.hs +++ b/src/Control/Monad/Freer/Internal.hs @@ -44,6 +44,7 @@ module Control.Monad.Freer.Internal ( decomp, tsingleton, + extract, qApp, qComp, @@ -137,9 +138,8 @@ run _ = error "Internal:run - This (E) should never happen" -- This is useful for plugging in traditional transformer stacks. runM :: Monad m => Eff '[m] w -> m w runM (Val x) = return x -runM (E u q) = case decomp u of - Right mb -> mb >>= runM . qApp q - Left _ -> error "Internal:runM - This (Left) should never happen" +runM (E u q) = case extract u of + mb -> mb >>= runM . qApp q -- the other case is unreachable since Union [] a cannot be -- constructed. Therefore, run is a total function if its argument diff --git a/src/Control/Monad/Freer/Trace.hs b/src/Control/Monad/Freer/Trace.hs index 56b4fdf..0a111be 100644 --- a/src/Control/Monad/Freer/Trace.hs +++ b/src/Control/Monad/Freer/Trace.hs @@ -38,6 +38,5 @@ trace = send . Trace -- | An IO handler for Trace effects runTrace :: Eff '[Trace] w -> IO w runTrace (Val x) = return x -runTrace (E u q) = case decomp u of - Right (Trace s) -> putStrLn s >> runTrace (qApp q ()) - Left _ -> error "runTrace:Left - This should never happen" +runTrace (E u q) = case extract u of + Trace s -> putStrLn s >> runTrace (qApp q ()) diff --git a/src/Data/Open/Union.hs b/src/Data/Open/Union.hs index 5ffede0..e4ec9ba 100644 --- a/src/Data/Open/Union.hs +++ b/src/Data/Open/Union.hs @@ -46,8 +46,12 @@ decomp :: Union (t ': r) v -> Either (Union r v) (t v) decomp (UNow x) = Right x decomp (UNext v) = Left v +{-# INLINE extract #-} +extract :: Union '[t] v -> t v +extract (UNow x) = x + {-# INLINE weaken #-} -weaken :: Union r w -> Union (any ': r) w +weaken :: Union (t ': r) w -> Union (any ': t ': r) w weaken = UNext class (Member' t r (FindElem t r)) => Member t r where diff --git a/src/Data/Open/Union/Internal.hs b/src/Data/Open/Union/Internal.hs index 4415e91..7d80fcf 100644 --- a/src/Data/Open/Union/Internal.hs +++ b/src/Data/Open/Union/Internal.hs @@ -10,7 +10,7 @@ module Data.Open.Union.Internal where data Union (r :: [ * -> * ]) v where UNow :: t v -> Union (t ': r) v - UNext :: Union r v -> Union (any ': r) v + UNext :: Union (t ': r) v -> Union (any ': t ': r) v data Nat = S Nat | Z data P (n :: Nat) = P @@ -25,7 +25,7 @@ instance (r ~ (t ': r')) => Member' t r 'Z where prj' _ (UNow x) = Just x prj' _ _ = Nothing -instance (r ~ (t' ': r'), Member' t r' n) => Member' t r ('S n) where +instance (r ~ (t' ': r' : rs'), Member' t (r' : rs') n) => Member' t r ('S n) where inj' _ = UNext . inj' (P::P n) prj' _ (UNow _) = Nothing prj' _ (UNext x) = prj' (P::P n) x From 4e1d228ba7e6310d82903e127659822c30a8866f Mon Sep 17 00:00:00 2001 From: Eric Easley Date: Wed, 16 Nov 2016 08:53:37 -0800 Subject: [PATCH 3/5] Don't rely on internals in example --- examples/src/Main.hs | 12 ++++++++---- examples/src/Teletype.hs | 34 +++++++++++++++++++--------------- src/Control/Monad/Freer.hs | 4 ++++ 3 files changed, 31 insertions(+), 19 deletions(-) diff --git a/examples/src/Main.hs b/examples/src/Main.hs index 80ddb45..4b90f09 100644 --- a/examples/src/Main.hs +++ b/examples/src/Main.hs @@ -1,18 +1,22 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} module Main where import Control.Monad.Freer import Teletype -runner :: Eff '[Teletype] () +runner :: (Member Teletype r) => Eff r () runner = do x <- getLine' + _ <- getLine' + putStrLn' x + z <- getLine' + putStrLn' z + putStrLn' x putStrLn' x - y <- getLine' - putStrLn' y main :: IO () main = do - let xs = runTeletypePure ["cat", "fish"] runner + let xs = runTeletypePure ["cat", "fish", "dog", "bird"] runner print xs runTeletype runner diff --git a/examples/src/Teletype.hs b/examples/src/Teletype.hs index 432bbfa..abb361d 100644 --- a/examples/src/Teletype.hs +++ b/examples/src/Teletype.hs @@ -5,7 +5,6 @@ module Teletype where import Control.Monad.Freer -import Control.Monad.Freer.Internal import System.Exit hiding (ExitSuccess) -------------------------------------------------------------------------------- @@ -28,22 +27,27 @@ exitSuccess' = send ExitSuccess -------------------------------------------------------------------------------- -- Effectful Interpreter -- -------------------------------------------------------------------------------- -runTeletype :: Eff '[Teletype] w -> IO w -runTeletype (Val x) = return x -runTeletype (E u q) = case extract u of - (PutStrLn msg) -> putStrLn msg >> runTeletype (qApp q ()) - GetLine -> getLine >>= \s -> runTeletype (qApp q s) - ExitSuccess -> exitSuccess +runTeletype :: Eff '[Teletype, IO] w -> IO w +runTeletype req = runM (handleRelay pure go req) + where + go :: Teletype v -> Arr '[IO] v w -> Eff '[IO] w + go (PutStrLn msg) q = send (putStrLn msg) >>= q + go GetLine q = send getLine >>= q + go ExitSuccess q = send exitSuccess >>= q -------------------------------------------------------------------------------- -- Pure Interpreter -- -------------------------------------------------------------------------------- runTeletypePure :: [String] -> Eff '[Teletype] w -> [String] -runTeletypePure inputs req = reverse (go inputs req []) - where go :: [String] -> Eff '[Teletype] w -> [String] -> [String] - go _ (Val _) acc = acc - go [] _ acc = acc - go (x:xs) (E u q) acc = case extract u of - (PutStrLn msg) -> go (x:xs) (qApp q ()) (msg:acc) - GetLine -> go xs (qApp q x) acc - ExitSuccess -> go xs (Val ()) acc +runTeletypePure inputs req = + reverse . snd $ run (handleRelayS (inputs, []) (\s _ -> pure s) go req) + where + go + :: ([String], [String]) + -> Teletype v + -> (([String], [String]) -> Arr '[] v ([String], [String])) + -> Eff '[] ([String], [String]) + go (is, os) (PutStrLn msg) q = q (is, msg : os) () + go (i:is, os) GetLine q = q (is, os) i + go ([], _) GetLine _ = error "Not enough lines" + go (_, os) ExitSuccess _ = pure ([], os) diff --git a/src/Control/Monad/Freer.hs b/src/Control/Monad/Freer.hs index 2f74d44..8c5d889 100644 --- a/src/Control/Monad/Freer.hs +++ b/src/Control/Monad/Freer.hs @@ -13,7 +13,11 @@ module Control.Monad.Freer ( Members, Eff, run, + runM, + handleRelay, + handleRelayS, send, + Arr, NonDetEff(..), makeChoiceA, From 0e8a6da11a75d1471768f918cd45f506ed485a61 Mon Sep 17 00:00:00 2001 From: Eric Easley Date: Wed, 16 Nov 2016 09:22:42 -0800 Subject: [PATCH 4/5] Make `Union` a `Functor` --- src/Data/Open/Union.hs | 28 ++++++---------------------- src/Data/Open/Union/Internal.hs | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 39 insertions(+), 22 deletions(-) diff --git a/src/Data/Open/Union.hs b/src/Data/Open/Union.hs index e4ec9ba..e2b1f95 100644 --- a/src/Data/Open/Union.hs +++ b/src/Data/Open/Union.hs @@ -32,7 +32,12 @@ starting point. module Data.Open.Union ( module Data.Open.Union, - Union + Union, + Member(..), + decomp, + weaken, + extract, + Functor(..) ) where import GHC.Exts @@ -41,27 +46,6 @@ import Data.Open.Union.Internal -------------------------------------------------------------------------------- -- Interface -- -------------------------------------------------------------------------------- -{-# INLINE decomp #-} -decomp :: Union (t ': r) v -> Either (Union r v) (t v) -decomp (UNow x) = Right x -decomp (UNext v) = Left v - -{-# INLINE extract #-} -extract :: Union '[t] v -> t v -extract (UNow x) = x - -{-# INLINE weaken #-} -weaken :: Union (t ': r) w -> Union (any ': t ': r) w -weaken = UNext - -class (Member' t r (FindElem t r)) => Member t r where - inj :: t v -> Union r v - prj :: Union r v -> Maybe (t v) - -instance (Member' t r (FindElem t r)) => Member t r where - inj = inj' (P :: P (FindElem t r)) - prj = prj' (P :: P (FindElem t r)) - type family Members m r :: Constraint where Members (t ': c) r = (Member t r, Members c r) Members '[] r = () diff --git a/src/Data/Open/Union/Internal.hs b/src/Data/Open/Union/Internal.hs index 7d80fcf..8c1c718 100644 --- a/src/Data/Open/Union/Internal.hs +++ b/src/Data/Open/Union/Internal.hs @@ -42,3 +42,36 @@ type family EQU (a :: k) (b :: k) :: Bool where EQU a a = 'True EQU a b = 'False +-------------------------------------------------------------------------------- + -- Interface -- +-------------------------------------------------------------------------------- + +{-# INLINE decomp #-} +decomp :: Union (t ': r) v -> Either (Union r v) (t v) +decomp (UNow x) = Right x +decomp (UNext v) = Left v + +{-# INLINE weaken #-} +weaken :: Union (t ': r) w -> Union (any ': t ': r) w +weaken = UNext + +{-# INLINE extract #-} +extract :: Union '[t] v -> t v +extract (UNow x) = x + + +class (Member' t r (FindElem t r)) => Member t r where + inj :: t v -> Union r v + prj :: Union r v -> Maybe (t v) + +instance (Member' t r (FindElem t r)) => Member t r where + inj = inj' (P :: P (FindElem t r)) + prj = prj' (P :: P (FindElem t r)) + +instance (Functor f) => Functor (Union '[f]) where + fmap f = inj . fmap f . extract +instance (Functor f1, Functor (Union (f2 ': fs))) => + Functor (Union (f1 ': f2 ': fs)) where + fmap f = either (weaken . fmap f) (inj . fmap f) . decomp + + From 23960755256892ef7dfbb06befe59bc2fe464aaa Mon Sep 17 00:00:00 2001 From: Eric Easley Date: Wed, 16 Nov 2016 09:44:45 -0800 Subject: [PATCH 5/5] Add `runNat` convenience function --- src/Control/Monad/Freer.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/Control/Monad/Freer.hs b/src/Control/Monad/Freer.hs index 8c5d889..2763ff5 100644 --- a/src/Control/Monad/Freer.hs +++ b/src/Control/Monad/Freer.hs @@ -1,3 +1,6 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE RankNTypes #-} {-| Module : Control.Monad.Freer Description : Freer - an extensible effects library @@ -14,6 +17,7 @@ module Control.Monad.Freer ( Eff, run, runM, + runNat, handleRelay, handleRelayS, send, @@ -25,3 +29,9 @@ module Control.Monad.Freer ( ) where import Control.Monad.Freer.Internal + +runNat + :: forall m r e w. + (Member m r) + => (forall a. e a -> m a) -> Eff (e ': r) w -> Eff r w +runNat f = handleRelay pure (\v -> (send (f v) >>=))