b8bd38b · typeable/ether

git.iko.soy/typeable/ether

on master help sign in

Constraint abbreviations

b8bd38bIndex Int11 years ago

ether.cabal+2

compare with master

unifiedsplit

@@ -26,6 +26,8 @@ library

27 exposed-modules: Control.Ether.Tagged

28 Control.Ether.Wrapped

29+ Control.Ether.Abbr

30+ Control.Ether.Implicit.Abbr

29 Control.Ether.TH

31 Control.Ether.TH

30 Control.Monad.Trans.Ether.Reader

32 Control.Monad.Trans.Ether.Reader

31 Control.Monad.Trans.Ether.Writer

33 Control.Monad.Trans.Ether.Writer

src/Control/Ether/Abbr.hsnew file+60

@@ -0,0 +1,60 @@

1+{-# LANGUAGE EmptyDataDecls #-}

2+{-# LANGUAGE TypeOperators #-}

3+{-# LANGUAGE ConstraintKinds #-}

4+{-# LANGUAGE DataKinds #-}

5+{-# LANGUAGE TypeFamilies #-}

7+-- | Abbreviations for constraints.

9+module Control.Ether.Abbr

10+ ( type (-->)

11+ , type (<--)

12+ , type (<->)

13+ , type (-!-)

14+ , Ether

15+ , ReifyAbbr

16+ ) where

17+

18+import GHC.Exts (Constraint)

19+

20+import Control.Monad.Ether

21+

22+-- | Turns an abbreviation into an actual constraint.

23+type family ReifyAbbr (abbr :: *) (m :: * -> *) :: Constraint

24+

25+-- | Denotes 'MonadReader'. The mnemonic is that you read values of type @r@

26+-- from the reader environment tagged by @tag@, thus the arrows points

27+-- from @tag@ to @r@.

28+data tag --> r

29+type instance ReifyAbbr (tag --> r) m = MonadReader tag r m

30+

31+-- | Denotes 'MonadWriter'. The mnemonic is that you write values of @w@

32+-- to the writer accumulator tagged by @tag@, thus the arrows points

33+-- from @w@ to @tag@.

34+data tag <-- w

35+type instance ReifyAbbr (tag <-- w) m = MonadWriter tag w m

36+

37+-- | Denotes 'MonadState'. The mnemonic is that you can both read from and

38+-- write into the state, thus the arrow points in both directions.

39+data tag <-> s

40+type instance ReifyAbbr (tag <-> s) m = MonadState tag s m

41+

42+-- | Denotes 'MonadExcept'.

43+data tag -!- e

44+type instance ReifyAbbr (tag -!- e) m = MonadExcept tag e m

45+

46+-- | Reify a list of constraint abbreviations.

47+--

48+-- > f :: Ether '[Foo --> r, Bar <-- w, Baz <-> s, Quux -!- e] m => m a

49+--

50+-- expands into

51+--

52+-- > f :: ( MonadReader Foo r m

53+-- > , MonadWriter Bar w m

54+-- > , MonadState Baz s m

55+-- > , MonadExcept Quux e m

56+-- > ) => m a

57+

58+type family Ether (abbrs :: [*]) m :: Constraint where

59+ Ether '[] m = ()

60+ Ether (abbr ': abbrs) m = (ReifyAbbr abbr m, Ether abbrs m)

src/Control/Ether/Implicit/Abbr.hsnew file+25

@@ -0,0 +1,25 @@

1+{-# LANGUAGE TypeFamilies #-}

3+-- | See "Control.Ether.Abbr".

5+module Control.Ether.Implicit.Abbr (R, W, S, E) where

7+import Control.Ether.Abbr (ReifyAbbr)

8+import Control.Monad.Ether.Implicit

10+-- | Denotes 'MonadReader'.

11+data R r

12+type instance ReifyAbbr (R r) m = MonadReader r m

13+

14+-- | Denotes 'MonadWriter'.

15+data W w

16+type instance ReifyAbbr (W w) m = MonadWriter w m

17+

18+-- | Denotes 'MonadState'.

19+data S s

20+type instance ReifyAbbr (S s) m = MonadState s m

21+

22+-- | Denotes 'MonadExcept'.

23+data E e

24+type instance ReifyAbbr (E e) m = MonadExcept e m

25+

test/Regression.hs+20−33

@@ -4,6 +4,8 @@

4{-# LANGUAGE TemplateHaskell #-}

5{-# LANGUAGE ConstraintKinds #-}

6{-# LANGUAGE ScopedTypeVariables #-}

7+{-# LANGUAGE DataKinds #-}

8+{-# LANGUAGE TypeOperators #-}

7{-# LANGUAGE LambdaCase #-}

9{-# LANGUAGE LambdaCase #-}

8module Main where

10module Main where

@@ -12,12 +14,13 @@ import Control.Monad

12import Control.Ether.Tagged

14import Control.Ether.Tagged

13import Control.Ether.TH

15import Control.Ether.TH

14import Control.Ether.Wrapped

16import Control.Ether.Wrapped

15−import Control.Monad.Ether.Reader

17+

16−import Control.Monad.Ether.State

18+import Control.Monad.Ether

17−import Control.Monad.Ether.Writer

19+import Control.Ether.Abbr

18−import qualified Control.Monad.Ether.Implicit.Reader as I

20+

19−import qualified Control.Monad.Ether.Implicit.State as I

21+import qualified Control.Monad.Ether.Implicit as I

20−import qualified Control.Monad.Ether.Implicit.Except as I

22+import qualified Control.Ether.Implicit.Abbr as I

23+

21import qualified Control.Monad.Reader as T

24import qualified Control.Monad.Reader as T

22import qualified Control.Monad.Writer as T

25import qualified Control.Monad.Writer as T

23import qualified Control.Monad.State as T

26import qualified Control.Monad.State as T

@@ -59,7 +62,7 @@ layeredLocalRight k f a1 a2 = property (direct == run indirect)

59 (direct, indirect) = layeredLocalCore' k f a1 a2

62 (direct, indirect) = layeredLocalCore' k f a1 a2

61layeredLocalCore

64layeredLocalCore

62− :: (MonadReader R1 r1 m, MonadReader R2 r2 m)

65+ :: Ether '[R1 --> r1, R2 --> r2] m

63 => (r2 -> r2) -> (r1 -> r2 -> a) -> m a

66 => (r2 -> r2) -> (r1 -> r2 -> a) -> m a

64layeredLocalCore f g = do

67layeredLocalCore f g = do

65 n <- ask r1

68 n <- ask r1

@@ -67,7 +70,7 @@ layeredLocalCore f g = do

67 return (g n m)

70 return (g n m)

69layeredLocalCore'

72layeredLocalCore'

70− :: (MonadReader R1 Int m, MonadReader R2 Integer m)

73+ :: Ether '[R1 --> Int, R2 --> Integer] m

71 => Fun (Int, Integer) Integer

74 => Fun (Int, Integer) Integer

72 -> Fun Integer Integer

75 -> Fun Integer Integer

73 -> Int -> Integer -> (Integer, m Integer)

76 -> Int -> Integer -> (Integer, m Integer)

@@ -76,27 +79,20 @@ layeredLocalCore' k f a1 a2 = (direct, indirect)

76 direct = apply k (fromIntegral a1, apply f a2)

79 direct = apply k (fromIntegral a1, apply f a2)

77 indirect = layeredLocalCore (apply f) (\n m -> apply k (fromIntegral n, m))

80 indirect = layeredLocalCore (apply f) (\n m -> apply k (fromIntegral n, m))

79−implicitCore :: (I.MonadReader Int m, I.MonadReader Bool m) => m String

82+implicitCore :: Ether '[I.R Int, I.R Bool] m => m String

80implicitCore = I.local (succ :: Int -> Int) $ do

83implicitCore = I.local (succ :: Int -> Int) $ do

81 n :: Int <- I.ask

84 n :: Int <- I.ask

82 b <- I.local not I.ask

85 b <- I.local not I.ask

83 return (if b then "" else show n)

86 return (if b then "" else show n)

85−wrapCore

86− :: ( T.MonadReader Int m

88+wrapCore :: (T.MonadReader Int m, T.MonadState Int m) => m Int

87− , T.MonadState Int m

88− ) => m Int

89wrapCore = do

90 b <- T.get

91 a <- T.ask

92 T.put (a + b)

93 return (a * b)

95−wrapCore'

95+wrapCore' :: Ether '[S1 --> Int, S1 <-> Int, R1 --> Int] m => m Int

96− :: ( MonadReader S1 Int m

97− , MonadState S1 Int m

98− , MonadReader R1 Int m

99− ) => m Int

100wrapCore' = do

96wrapCore' = do

101 a <- ethered s1 wrapCore

97 a <- ethered s1 wrapCore

102 c <- ask r1

98 c <- ask r1

@@ -121,16 +117,14 @@ uniqueTagsCore = flip (runReaderT r1) (1 :: Int)

121 print b

117 print b

122 print c

118 print c

123

119

124−stateCore :: ( MonadState S1 Int m

125− , MonadReader R1 Int m

126− , UniqueTags m ) => m ()

120+stateCore :: (Ether '[S1 <-> Int, R1 --> Int] m, UniqueTags m) => m ()

127−stateCore = do

121+stateCore = ensureUniqueTags $ do

128 a <- ask r1

122 a <- ask r1

129 n <- get s1

123 n <- get s1

130 put s1 (n * a)

124 put s1 (n * a)

131 modify s1 (subtract 1)

125 modify s1 (subtract 1)

132

126

133−recurseCore :: (Num a, Ord a) => (I.MonadReader a m, I.MonadState Int m) => m a

127+recurseCore :: (Num a, Ord a) => Ether '[I.R a, I.S Int]m => m a

134recurseCore = do

128recurseCore = do

135 a <- I.ask

129 a <- I.ask

136 if (a <= 0)

130 if (a <= 0)

@@ -156,8 +150,7 @@ data NegativeLog a = NegativeLog a

156

150

157exceptCore

151exceptCore

158 :: ( Floating a, Ord a

152 :: ( Floating a, Ord a

159− , I.MonadExcept DivideByZero m

160− , I.MonadExcept (NegativeLog a) m

153+ , Ether '[I.E DivideByZero, I.E (NegativeLog a)] m

161 ) => a -> a -> m a

154 ) => a -> a -> m a

162exceptCore a b = do

155exceptCore a b = do

163 T.when (b == 0) (I.throw DivideByZero)

156 T.when (b == 0) (I.throw DivideByZero)

@@ -193,10 +186,7 @@ wrapState_f = liftM show T.get

193wrapState_g :: T.MonadState Bool m => m String

186wrapState_g :: T.MonadState Bool m => m String

194wrapState_g = liftM show T.get

187wrapState_g = liftM show T.get

195

188

196−wrapState_useboth

189+wrapState_useboth :: Ether '[Foo <-> Int, Bar <-> Bool] m => m String

197− :: ( MonadState Foo Int m

198− , MonadState Bar Bool m

199− ) => m String

200wrapState_useboth = do

190wrapState_useboth = do

201 a <- ethered foo wrapState_f

191 a <- ethered foo wrapState_f

202 b <- ethered bar wrapState_g

192 b <- ethered bar wrapState_g

@@ -216,10 +206,7 @@ wrapStateBad1_useboth = do

216wrapStateBad1 :: Int -> String

206wrapStateBad1 :: Int -> String

217wrapStateBad1 = evalState foo wrapStateBad1_useboth

207wrapStateBad1 = evalState foo wrapStateBad1_useboth

218

208

219−wrapStateBad2

220− :: ( T.MonadState Int m

221− , MonadState Foo Int m

209+wrapStateBad2 :: (T.MonadState Int m , MonadState Foo Int m) => m Int

222− ) => m Int

223wrapStateBad2 = do

210wrapStateBad2 = do

224 modify foo (*100)

211 modify foo (*100)

225 T.get

212 T.get