free 4.5 → 4.6
raw patch · 22 files changed
+2366/−393 lines, 22 files
Files
- CHANGELOG.markdown +10/−0
- HLint.hs +15/−0
- doc/proof/Control/Comonad/Cofree/instance-Applicative-Cofree.md +6/−0
- doc/proof/Control/Comonad/Cofree/instance-Monad-Cofree.md +6/−0
- doc/proof/Control/Comonad/Cofree/instance-MonadZip-Cofree.md +9/−0
- doc/proof/Control/Comonad/Trans/Cofree/instance-Applicative-CofreeT.md +612/−0
- doc/proof/Control/Comonad/Trans/Cofree/instance-Monad-CofreeT.md +200/−0
- doc/proof/Control/Comonad/Trans/Cofree/instance-MonadTrans-CofreeT.md +88/−0
- doc/proof/Control/Comonad/Trans/Cofree/instance-MonadZip-CofreeT.md +448/−0
- free.cabal +4/−2
- src/Control/Alternative/Free.hs +79/−44
- src/Control/Applicative/Free.hs +15/−1
- src/Control/Comonad/Cofree.hs +12/−0
- src/Control/Comonad/Trans/Cofree.hs +60/−3
- src/Control/Comonad/Trans/Coiter.hs +169/−3
- src/Control/Monad/Free.hs +8/−0
- src/Control/Monad/Free/Church.hs +41/−14
- src/Control/Monad/Free/TH.hs +195/−5
- src/Control/Monad/Trans/Free.hs +43/−2
- src/Control/Monad/Trans/Free/Church.hs +37/−0
- src/Control/Monad/Trans/Iter.hs +309/−14
- src/Control/MonadPlus/Free.hs +0/−305
CHANGELOG.markdown view
@@ -1,3 +1,13 @@+4.6+---+* Víctor López Juan and Fabian Ruch added many documentation improvements and a whole host of proofs of correctness.+* Improvements in the template haskell code generator.+* Added instances for `MonadWriter` and `MonadCont` where appropriate, thanks to Nickolay Kudasov.+* Added `cutoff`, `iterTM`, and `never`.+* Made modifications to some `Typeable` and `Data` instances to work correctly on both GHC 7.8.1rc1 and 7.8.1rc2.+* Removed `Control.MonadPlus.Free`. Use `FreeT f []` instead and the result will be law-abiding.+* Replaced `Control.Alternative.Free` with a new approach that is law-abiding for left-distributive Alternatives.+ 4.5 ----- * Added `Control.Monad.Free.TH` with `makeFree` to make it easier to write free monads.
+ HLint.hs view
@@ -0,0 +1,15 @@+import "hint" HLint.HLint++infixr 5 :<++-- This affects performance+ignore "Redundant lambda"++-- This is not valid for improve+ignore "Eta reduce"++-- DeriveDataTypable noise+ignore "Unused LANGUAGE pragma"++-- They are clearer in places+ignore "Avoid lambda"
+ doc/proof/Control/Comonad/Cofree/instance-Applicative-Cofree.md view
@@ -0,0 +1,6 @@+Instance of Applicative for Cofree+==================================++See [proof for the transformer version]+(../Trans/Cofree/instance-Applicative-CofreeT.md) and specialize it for the+Identity applicative functor.
+ doc/proof/Control/Comonad/Cofree/instance-Monad-Cofree.md view
@@ -0,0 +1,6 @@+Instance of Monad for Cofree+==================================++See [proof for the transformer version]+(../Trans/Cofree/instance-Monad-CofreeT.md) and specialize it for the+Identity Monad.
+ doc/proof/Control/Comonad/Cofree/instance-MonadZip-Cofree.md view
@@ -0,0 +1,9 @@+MonadZip instance for Cofree+============================++For every functor `f` with `Alternative` and `MonadZip` instances,+`Cofree f` is an instance of `MonadZip`.++The claim follows as a corollary from the [`MonadZip` instance theorem+for `CofreeT`](../Trans/Cofree/instance-MonadZip-CofreeT.md) when `m` is+set to be `Identity`, which obviously has an instance of `MonadZip`.
+ doc/proof/Control/Comonad/Trans/Cofree/instance-Applicative-CofreeT.md view
@@ -0,0 +1,612 @@+Applicative instance for CofreeT+================================++If the underlying functor f is an instance of Alternative, then CofreeT is also+an applicative functor.++Note that the only required properties of Alternative are associativity and+existence of an identity element, so one could also use functors that are+instances of Plus (semigroupoid package).++```haskell+instance (Alternative f, Applicative w) =>+ Applicative (CofreeT f w) where+ pure = CofreeT . pure . (:< empty)+ + (CofreeT wf) <*> aa@(CofreeT wa) = CofreeT $+ ( \(f :< t) -> + \(a) -> + let (b :< n) = bimap f (fmap f) a in + b :< (n <|> fmap (<*> aa) t)) <$> wf <*> wa+```+++## Identity++```haskell++ pure id <*> (C wa)++== {- definition of <*> -}++ C $+ ( \(f :< t) -> + \(a) -> + let (b :< n) = bimap f (fmap f) a in + b :< (n <|> fmap (<*> C wa) t)) <$> (pure $ id :< empty) <*> wa++== {- w is Applicative -}+ + C $+ \(a) -> + let (b :< n) = bimap id (fmap id) a in + b :< (n <|> fmap (<*> C wa) empty)) <$> wa++== {- functor preserves identity -}++ C $+ \(a) -> + let (b :< n) = bimap id id a in + b :< (n <|> fmap (<*> C wa) empty)) <$> wa++== {- bifunctors preserve identity -}++ C $+ \(a) -> + let (b :< n) = a in + b :< (n <|> fmap (<*> C wa) empty)) <$> wa++== {- empty is invariant under fmap -}+ + C $+ \(a) -> + let (b :< n) = a in + b :< (n <|> empty) <$> wa++== {- empty is identity, β-reduction -}++ C $ id <$> wa++== {- functor preserves identity -}++ C wa++```+++## Composition++First, we rewrite the definition of the (<*>) into something simpler:++```haskell++ (C wf) <*> (C wa)++== {- definition of <*> -}++ C $+ ( \(f :< t) -> + \(a) -> + let (b :< n) = bimap f (fmap f) a in + b :< (n <|> fmap (<*> C wa) t)) <$> wf <*> wa++== {- pattern match on CofreeF -}++ C $+ ( \(f :< t) -> + \(a :< m) -> + let (b :< n) = bimap f (fmap f) (a :< m) in + b :< (n <|> fmap (<*> C wa) t)) <$> wf <*> wa++== {- definition of bimap -}++ C $+ ( \(f :< t) -> + \(a :< m) -> + let (b :< n) = f a :< fmap (fmap f) m in + b :< (n <|> fmap (<*> C wa) t)) <$> wf <*> wa++== {- β-equivalence -}++ C $+ ( \(f :< t) -> + \(a :< m) -> + (f a) :< (fmap (fmap f) m <|> fmap (<*> C wa) t)) <$> wf <*> wa++== {- define star(C wa) ≡ ( \(f :< t) -> … (<*> C wa) … ) -}++ C $ star(C wa) <$> wf <*> wa++== {- fmap for w Applicative -}++ C (pure star(C wa) <*> wf <*> wa)++```++Now, we can prove the law of composition:++```haskell++ pure (.) <*> C u <*> C v <*> C w++== {- definition of <*> -}++ C (pure star(C u) <*> pure ((.) :< empty) <*> u ) <*> C v <*> C w ++== {- definition of <*> -}++ C (pure star(C v) <*> + (pure star(C u) <*> pure ((.) :< empty) <*> u ) <*> + v+ ) <*> + C w++== {- definition of <*> -}++ C (pure star(C w) <*>+ (pure star(C v) <*>+ (pure star(C u) <*> pure ((.) :< empty) <*> u ) <*>+ v) <*>+ w)+++== {- see lemma 1 -}++ C $ (\a :< m -> \b :< n -> c :< p ->+ (a (b c)) :< (fmap (fmap (a . b)) p <|>+ fmap (\x -> pure (.) <*> pure a <*> x <*> C w) n) <|>+ fmap (\x -> pure (.) <*> x <*> C v <*> C w) m))) ==+++++== {- coinduction on recursive definition (“produce 1, consume 1”) -}++ + C $ (\a :< m -> b :< n -> c :< p ->+ (a (b c) :< (fmap (fmap (a . b)) p) <|>+ (fmap (\x -> pure a <*> (x <*> C w)) n) <|>+ (fmap (\x -> x<*> (C v <*> C w)) m) ) +++== {- see lemma 2 -}++ C (pure star(C v <*> C w) <*>+ u <*>+ (pure star(C w) <*>+ v <*>+ w))+ +== {- definition of <*> -}++ C (pure star(C v <*> C w) <*> u <*> unC (C v <*> C w))++== {- definition of <*> -}++ C u <*> (C v <*> C w)+```++### Lemma 1++To make reasoning easier, we'll use a shortand notation.++```+U ≡ star(C v)+V ≡ star(C u)+W ≡ star(C w)+! ≡ (.) :< empty+p ≡ pure+<concatenation> ≡ function application +. ≡ (.)+```++By repeteadly applying the Applicative laws for the underlying functor, we+get:++```haskell+ +pW <*> (pV <*> (pU <*> p! <*> u) <*> v ) <*> w ==++pW <*> (pV <*> (p(U!) <*> u) <*> v ) <*> w ==++pW <*> (p. <*> pV <*> p(U!) <*> u <*> v ) <*> w ==++pW <*> ( p(.V)(U!) <*> u <*> v ) <*> w ==++p. <*> pW <*> ( p(.V)(U!) <*> u ) <*> v <*> w ==++p(.W) <*> (p(.V)(U!) <*> u) <*> v <*> w ==++p. <*> p(.W) <*> p(.V)(U!) <*> u <*> v <*> w ==++p.(.W)((.V)(U!)) <*> u <*> v <*> w ++```++Undoing the shorthand notation and simplifying:++```haskell++! == (.) :< empty+U! == \(a :< m) -> (. a) :< fmap (fmap (.)) m+V == \(f :< t) -> \(b :< n) -> (f b) :< (fmap (fmap f) n <|> + fmap (<*> C v) t)+++. V (U!) == \(a :< m) -> V ((. a) :< fmap (fmap (.)) m) ==+ == \(a :< m) -> \(b :< n) ->+ (a . b) :< (fmap (fmap (. a) n) <|>+ fmap (<*> C v) ( fmap (fmap (.)) m)++W == \(f :< t) -> \(c :< p) ->+ (f c) :< (fmap (fmap f) p <|> fmap (<*> C w) t)++.W == \g -> (\x -> W (g x))+++ .(.W)(.V(U!))++== \s -> (.W)((.V(U!)) s) ==++== \a :< m -> (.W) ((.V(U!)) a :< m) ==++== \a :< m -> (.W) (\(b :< n) ->+ (a . b) :< (fmap (fmap (. a) n) <|>+ fmap (<*> C v) ( fmap (fmap (.)) m))) ==++== \a :< m -> \b :< n ->+ W ( (a . b) :< (fmap (fmap (. a) n) <|>+ fmap (<*> C v) ( fmap (fmap (.)) m))) ==++== \a :< m -> \b :< n -> c :< p ->+ (a (b c)) :< (fmap (fmap (a . b)) p <|>+ fmap (<*> C w)+ ((fmap (fmap (. a) n) <|>+ fmap (<*> C v) (fmap (fmap (.)) m)))) ==++== \a :< m -> \b :< n -> c :< p ->+ (a (b c)) :< (fmap (fmap (a . b)) p <|>+ fmap (<*> C w) (fmap (fmap (. a)) n) <|>+ fmap (<*> C w) (fmap (<*> C v) ( fmap (fmap (.)) m))) ==++== \a :< m -> \b :< n -> c :< p ->+ (a (b c)) :< (fmap (fmap (a . b)) p <|>+ fmap (\x -> pure (.) <*> pure a <*> x <*> C w) n) <|>+ fmap (\x -> pure (.) <*> x <*> C v <*> C w) m))) +```++### Lemma 2++We use the following shorthands to make reasoning more readable.++```+W ≡ star(C w)+Y ≡ star(C v <*> C w)+p ≡ pure+<concatenation> ≡ function application +. ≡ (.)+$W ≡ ($ star(C w))+```++By repeteadly applying composition law for w, we get:++```haskell+ +pY <*> u <*> (pW <*> v <*> w) ==++p. <*> (pY <*> u) <*> (pW <*> v) <*> w ==++p. <*> p. <*> pY <*> u <*> (pW <*> v) <*> w ==++p. <*> (p. <*> p. <*> pY <*> u) <*> pW <*> v <*> w ==++p. <*> (p..Y <*> u) <*> pW <*> v <*> w ==++p. <*> p. <*> p..Y <*> u <*> pW <*> v <*> w ==++p..(..Y) <*> u <*> pW <*> v <*> w ==++p($W) <*> (p..(..Y) <*> u) <*> v <*> w ==++p.($W)(..(..Y)) <*> u <*> v <*> w+++(.) == \f -> \g -> \x -> f (g x)++($W) == \g -> g W++($W) . (..(..Y)) == \s -> (\g -> g W) ((..(..Y)) s)+ == \s -> (..(..Y)) s W++(. . (..Y)) == (\s -> . ((..Y) s))++∴ ($W) . (..(..Y)) == \s -> ((..Y) s) . W++(..Y) == (\y -> (.) (Y y))++∴ ($W) . (..(..Y)) == \s -> ((.) (Y s)) . W++ == \s -> \t -> ((.) (Y s)) (W t)+ + == \s -> \t -> (Y s) . (W t)++ == \s -> \t -> u -> (Y s (W t u))+```++Undoing shorthands and α-converting, we get:++```haskell+.($W)(..(..Y)) ==++\a :< m -> b :< n -> c :< p -> (Y (a :< m) (W (b :<n) (c :< p))) ==++\a :< m -> b :< n -> c :< p ->+ (Y (a :< m) (b c :< (fmap (fmap b) p) <|>+ (fmap (<*> C w) n))) ==++\a :< m -> b :< n -> c :< p ->+ (Y (a :< m) (b c :< (fmap (fmap b) p) <|>+ (fmap (<*> C w) n))) ==++\a :< m -> b :< n -> c :< p ->+ (a (b c) :< (fmap (fmap a) ((fmap (fmap b) p) <|>+ (fmap (<*> C w) n)))+ <|>+ (fmap (<*> (C v <*> C w)) m))+ +== {- fmap distributes over <|>, fmap respects composition -}+ +\a :< m -> b :< n -> c :< p ->+ (a (b c) :< (fmap (fmap (a . b)) p) <|>+ (fmap ((fmap a) . (<*> C w)) n) <|>+ (fmap (<*> (C v <*> C w)) m)) ++== ++\a :< m -> b :< n -> c :< p ->+ (a (b c) :< (fmap (fmap (a . b)) p) <|>+ (fmap (\x -> pure a <*> (x <*> C w)) n) <|>+ (fmap (\x -> x<*> (C v <*> C w)) m) ) +```++## Homomorphism++```haskell++ pure f <*> pure x++== {- definition of <*> -}++ C $+ ( \(f :< t) -> + \(a) -> + let (b :< n) = bimap f (fmap f) a in + b :< (n <|> fmap (<*> pure x) t)) <$>+ pure (f :< empty) <*> pure (x :< empty)++== {- homomorphism law for w, twice -}++ C $ pure $+ let (b :< n) = bimap f (fmap f) (x :< empty) in + b :< (n <|> fmap (<*> pure x) empty)) ++== {- bimap -}++ C $ pure $+ let (b :< n) = (f x :< (fmap f empty)) in + b :< (n <|> fmap (<*> pure x) empty)) ++== {- empty invariant under fmap -}+ + C $ pure $ (f x) :< (empty <|> empty) ++== {- definition -}++ pure (f x)++```++## Interchange++```haskell++ u <*> pure y++== {- definition of <*>, pure -}++ C $ + ( \(f :< t) ->+ \(a) -> + let (b :< n) = bimap f (fmap f) a in+ b :< (n <|> fmap (<*> (pure y)) t)) <$> u <*> (pure (y :< empty))++== {- interchange law for w -}++ C $+ pure ($ y :< empty) <*>+ (pure+ ( \(f :< t) ->+ \(a) -> + let (b :< n) = bimap f (fmap f) a in+ b :< (n <|> fmap (<*> (pure y)) t))) <*> u)++== {- composition -}++ C $+ pure (.) <*>+ pure ($ y :< empty) <*>+ pure+ ( \(f :< t) ->+ \(a) -> + let (b :< n) = bimap f (fmap f) a in+ b :< (n <|> fmap (<*> (pure y)) t))++ <*> u)++== {- homomorphism -}++ C $+ pure (($ y :< empty) .) <*>+ pure+ ( \(f :< t) ->+ \(a) -> + let (b :< n) = bimap f (fmap f) a in+ b :< (n <|> fmap (<*> (pure y)) t))++ <*> u)++== {- homomorphism -}++ C $+ pure (($ y :< empty) . + ( \(f :< t) ->+ \(a) -> + let (b :< n) = bimap f (fmap f) a in+ b :< (n <|> fmap (<*> (pure y)) t))+ <*> u)++== {- β-reduction -}++ C $+ pure (+ ( \(f :< t) ->+ let (b :< n) = bimap f (fmap f) (y :< empty) in+ b :< (n <|> fmap (<*> (pure y)) t))+ <*> u)++== {- bimap, β-reduction -}++ C $+ pure (+ ( \(f :< t) -> f y :< (empty <|> fmap (<*> (pure y)) t))+ <*> u)++== {- fmap -}++ C $ (\(f :< t) -> f y :< (fmap (<*> pure y) t)) <$> u ++== {- coinduction (consume 1, produce 1) -}+ + C $ (\(f :< t) -> f y :< (fmap ($ y) t)) <$> u+ +== {- def. $ -}++ C $ (\(f :< t) -> ($ y) f :< (fmap ($ y) t)) <$> u++== {- def. bimap -}++ C $ bimap ($ y) (fmap ($ y)) <$> u++== {- β,η-expansion -}++ C $ + ( + \(a) -> + let (b :< n) = bimap ($ y) (fmap ($ y)) a in+ b :< n) <$> u++== {- empty inviariant under fmap -}++ C $ + ( + \(a) -> + let (b :< n) = bimap ($ y) (fmap ($ y)) a in+ b :< (n <|> fmap (<*> u) empty)) <$> u++== {- fmap over pure -} ++ C $ + ( \(f :< t) ->+ \(a) -> + let (b :< n) = bimap f (fmap f) a in+ b :< (n <|> fmap (<*> u) t)) <$> (pure (($ y) :< empty)) <*> u++== {- definition -}++pure ($ y) <*> u+```++## Consistency with Monad definition++```haskell+instance (Alternative f, Monad w) => Monad (CofreeT f w) where+ return = CofreeT . return . (:< empty)+ (CofreeT cx) >>= f = CofreeT $ do+ (a :< m) <- cx+ (b :< n) <- runCofreeT $ f a+ return $ b :< (n <|> fmap (>>= f) m)+```++If w is also a monad, then ```(<*>) == ap```.+ +The proof uses coinduction for the case “produce one, consume one”.+ +_Remark:_ If ```g = (\f -> (CofreeT wa) >>= (\a -> return $ f a))```, then+ ```(`ap` a) == (>>= g)```.++```haskell++(C wf) `ap` (C wa)++== {- definition -}++(C wf) >>= (\f -> (C wa) >>= (\a -> f a))++== {- definition -}++ wf >>= \(f :< t) ->+ unC (C wa >>= (\a -> return $ f a)) >>= \(b :< n) ->+ return $ b :< (n <|> fmap (>>= g) t)++== {- coinductive step -}++ wf >>= \(f :< t) ->+ unC (C wa >>= (\a -> return $ f a)) >>= \(b :< n) ->+ return $ b :< (n <|> fmap (<*> C wa) t)+== {- definition of fmap for monads -}+++ wf >>= \(f :< t) ->+ unC (fmap f (C wa)) >>= \(b :< n) ->+ return $ b :< (n <|> fmap (<*> C wa) t)++== {- definition of fmap for C -}++ wf >>= \(f :< t) ->+ fmap (bimap f (fmap f)) wa >>= \(b :< n) ->+ return $ b :< (n <|> fmap (<*> C wa) t)+ +== {- definition of fmap for monads -}++ wf >>= \(f :< t) ->+ (wa >>= (\a -> return (bimap f (fmap f) a) >>= \(b :< n) ->+ return $ b :< (n <|> fmap (<*> C wa) t)++== {- associativity of monads -}++ wf >>= \(f :< t) ->+ wa >>= \a ->+ (return (bimap f (fmap f a))) >>= \(b :< n) -> + return $ b :< (n <|> fmap (<*> a) m)++== {- Left identity of monads -}++ wf >>= \(f :< t) ->+ wa >>= \(a ->+ let b :< n = bimap f (fmap f a)) in+ return $ b :< (n <|> fmap (<*> a) m))++== {- Equivalence of (>>=) and (<*>) for monad w. -}++ \(f :< t) ->+ \(a ->+ let b :< n = bimap f (fmap f a)) in+ return $ b :< (n <|> fmap (<*> a) m)))++== {- definition of (<*>) -}++(CofreeT wf) <*> (CofreeT wa)++```+ +
+ doc/proof/Control/Comonad/Trans/Cofree/instance-Monad-CofreeT.md view
@@ -0,0 +1,200 @@+Monad instance for CofreeT+==========================++If the underlying functor f is an instance of Alternative, then CofreeT is also+a Monad.++Note that the only required properties of Alternative are associativity and+identity element, so one could also use functors that are instances of Plus+(semigroupoid package).++```haskell+instance (Alternative f, Monad w) => Monad (CofreeT f w) where+ return = CofreeT . return . (:< empty)+ (CofreeT cx) >>= f = CofreeT $ do+ (a :< m) <- cx+ (b :< n) <- runCofreeT $ f a+ return $ b :< (n <|> fmap (>>= f) m)+```++This definition is equivalent to that of the Cofree module if 'w' is+identity. ++The tokens `CofreeT` and `runCofreeT` are abreviated as `C` and `unC`, +respectively, for readability.++## Left identity++```haskell+return x >>= f++== {- definition of return -}++C (return (x :< empty)) >>= f++== {- definition of bind -}++C $ (return (x :< empty)) >>= (\a :< m ->+ unC (f a) >>= (\b :< n ->+ return $ b :< (n <|> fmap (>>= f) m)++== {- Left identity for 'w' -}++ C $ unC (f x) >>= (\b :< n ->+ return $ b :< (n <|> fmap (>>= f) empty)++== {- fmap over empty -}++ C $ unC (f x) >>= (\b :< n ->+ return $ b :< (n <|> fmap (>>= f) empty)++== {- empty is identity for <|> -} == ++ C $ unC (f x) >>= (\b :< n ->+ return $ b :< n+ +== {- η-reduction, right identity for w -}++ C $ unC (f x)+==++f x+```++## Right identity ++```haskell++ (C wx) >>= return++== {- definition of return -}++ (C wx) >>= (\x -> C $ return $ (x :< empty))++== {- definition of bind -}++ C $ wx >>= (\a :< m -> unC (C $ return $ a :< empty)+ >>= (\b :< n -> return $ b :< (n <|> fmap (>>= return) m)++== {- coinduction (“produce 1, consume 1”) -}++ C $ wx >>= (\a :< m -> unC (C $ return $ a :< empty)+ >>= (\b :< n -> return $ b :< (n <|> fmap id m)++== {- fmap id == id -}++ C $ wx >>= (\a :< m ->+ unC (C $ return $ a :< empty) >>= (\b :< n ->+ return $ b :< (n <|> m)++== {- unC . C == id, left identity for w -}++ C $ wx >>= (\a :< m ->+ let b :< n = a :< empty in+ return $ b :< (n <|> m)++== {- β-equivalence -}++ C $ wx >>= (\a :< m -> return $ a :< (empty <|> m))++== {- empty is identity for <|> -}++ C $ wx >>= (\a :< m -> return $ a :< m))++== {- right identity for w -}++ C wx+```++## Associativity++```haskell+ (C wa >>= g) >>= h+ +== {- definition -}+ + C $ do+ unC (C wa >>= g) >>= \(c :< o) ->+ unC $ h c >>= \(d :< p) _>+ return $ d :< (p <|> fmap (>>= h) o)+ +== {- definition -}+ + C $ do+ (wa >>= \(a :< m) ->+ unC (g a) >>= \(b :< n) ->+ return $ b :< (m <|> fmap (>>= g) n)+ ) >>= \(c :< o) ->+ unC $ h c >>= \(d :< p) _>+ return $ d :< (p <|> fmap (>>= h) o)+ +== {- associativity of 'w' -}+ + C $ do+ wa >>= \(a :< m) ->+ unC (g a) >>= \(b :< n) ->+ return $ b :< (m <|> fmap (>>= g) m) >>= \(c :< o) ->+ unC $ h c >>= \(d :< p) _>+ return $ d :< (p <|> fmap (>>= h) o)+ +== {- left identity -}+ C $ do+ wa >>= \(a :< m) ->+ unC (g a) >>= \(b :< n) ->+ unC (h b) >>= \(d :< p) _>+ return $ d :< (p <|> fmap (>>= h) (n <|> fmap (>>= g) m))+ +== {- fmap distributes over (<|>), <|> is associative -}+ + C $ do+ wa >>= \(a :< m) ->+ unC (g a) >>= \(b :< n) ->+ unC (h b) >>= \(d :< p) + return $ d :< (p <|> (fmap (>>= h) n) <|> fmap (>>= h) (fmap (>>= g) m))+ +== {- ∀f ∀g . fmap (f . g) == fmap f . fmap g -}+ C $ do+ wa >>= \(a :< m) ->+ unC (g a) >>= \(b :< n) ->+ unC (h b) >>= \(d :< p) + return $ d :< (p <|> (fmap (>>= h) n) <|> fmap ((>>= h) . (>>= g)) m)+ +== {- coinduction -}+ + C $ do+ wa >>= \(a :< m) ->+ unC (g a) >>= \(b :< n) ->+ unC (h b) >>= \(d :< p) + return $ d :< (p <|> (fmap (>>= h) n) <|> fmap (>>= (\x -> g x >>= h)) m)+ +== {- associativity of <|> -}+ + c $ do+ wa >>= \(a :< m) ->+ unC (g a) >>= \(b :< n) ->+ unC (h b) >>= \(d :< p) + return $ d :< ((p <|> fmap (>>=h) n) <|> fmap (>>= (\x -> g x >>= h)) m+ +== {- associativity, right identity for monads -}+ c $ do+ (wa >>= \(a :< m) ->+ unC (g a) >>= \(b :< n) ->+ unC (h b) >>= \(d :< p) + return (d :< (p <|> (fmap >>= h) n))) >>= \(c :< o) ->+ return $ c :< (o <|> fmap (>>= (\x -> g x >>= h)) m+ +== {- definition of bind -}++ C $ do+ wa >>= \(a :< m) ->+ unC (g a >>= h) >>= \(c :< o) ->+ return $ c :< (o <|> fmap (>>= (\x -> g x >>= h)) m)+ +== {- definition of bind -}++ (C wa) >>= (\x -> g x >>= h)+```++## Consistency with Applicative definition++See [proof for applicative instance](instance-Applicative-CofreeT.md#consistency-with-monad-definition).
+ doc/proof/Control/Comonad/Trans/Cofree/instance-MonadTrans-CofreeT.md view
@@ -0,0 +1,88 @@+MonadTrans instance for CofreeT+===============================++If the ```Functor f``` is an instance of ```Plus``` (or of ```Alternative```)+then CofreeT is a monad transformer.++## Lift `return`++```haskell+lift (return x)++== {- definition lift -}++C $ (liftM (:< empty) (return x))++== {- definition liftM -}++C $ (return x) >>= (\a -> return $ a :< empty)++== {- monad left identity -}++C $ return $ x :< empty++== {- definition -}++return x+```++## Lift distributes over `bind`++```haskell+lift (m >>= f)++== {- definition lift -}++C $ (liftM (:< empty) (m >>= f))++== {- definition liftM -}++C $ (m >>= f) >>= (\a -> return $ a :< empty)++== {- α-equivalence -}++C $ m >>= f >>= (\b -> return $ b :< empty)++== {- η-equivalence -}++C $ m >>= \a ->+ f a >>= \b ->+ return $ b :< empty++== {- empty invariant under fmap, empty identity -}++C $ m >>= \a ->+ f a >>= \b ->+ return $ b :< (empty <|> fmap (>>= …) empty)++== {- left identity -}++C $ m >>= \a ->+ return (a :< empty) >>= \a :< n ->+ f a >>= \b ->+ return (b :< empty) >>= \b :< m ->+ return $ b :< (n <|> fmap (>>= …) m)+++== {- associativity of >>= -}++C $ (m >>= (\a -> return $ a :< empty)) >>= \a :< n ->+ ((f a) >>= (\b -> return $ b :< empty)) >>= \b :< m ->+ return $ b :< (n <|> fmap (>>= …) m)++== {- pattern matching on CofreeF -}++(C (m >>= (\a -> return $ a :< empty)) >>= (\x -> C ((f x) >>= (\b -> return b :< empty)))++== {- definition lift -}++(C (m >>= (\a -> return $ a :< empty)) >>= (\x -> lift (f x))++== {- definition lift -}++lift m >>= (lift . f)+```++++
+ doc/proof/Control/Comonad/Trans/Cofree/instance-MonadZip-CofreeT.md view
@@ -0,0 +1,448 @@+MonadZip instance for CofreeT+=============================++For every monad `m` with a `MonadZip` instance and functor `f` with+`Alternative` and `MonadZip` instances, `CofreeT f m` is an instance of+`MonadZip`.++```haskell+instance (Alternative f, MonadZip f, MonadZip m) => MonadZip (CofreeT f m) where+ mzip (CofreeT ma) (CofreeT mb) = CofreeT $ do+ (a :< fa, b :< fb) <- mzip ma mb+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)+```++This definition is equivalent to that of the `Cofree` module if `m` is+chosen to be the `Identity` monad.++The claim follows directly from the two lemmata below, which establish+the `MonadZip` laws for naturality and information preservation+respectively, and the [`Monad` instance theorem for+`CofreeT`](instance-Monad-CofreeT.md).++In the following, the tokens `CofreeT` and `runCofreeT` are abbreviated+as `C` and `unC` respectively.++## Naturality++```haskell+liftM (f *** g) (mzip ma mb) == mzip (liftM f ma) (liftM g mb)+```++### Proof.++```haskell+ liftM (f *** g) (mzip ma mb)++== {- Definition of `liftM` -}++ mzip ma mb >>= return . (f *** g)++== {- Definition of `mzip` -}++ C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)+ >>= return . (f *** g)++== {- Definition of `(>>=)` -}++ C $ do c :< m <- do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)+ d :< n <- unC $ return $ (f *** g) c+ return $ d :< (n <|> fmap (>>= return . f *** g) m)++== {- `Monad` law `m >>= (\x -> k x >>= h) == (m >>= k) >>= h` -}++ C $ do a :< fa <- unC ma+ c :< m <- do b :< fb <- unC mb+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)+ d :< n <- unC $ return $ (f *** g) c+ return $ d :< (n <|> fmap (>>= return . f *** g) m)++== {- `Monad` law `m >>= (\x -> k x >>= h) == (m >>= k) >>= h` -}++ C $ do a :< fa <- unC ma+ b :< fb <- unC mb+ c :< m <- return $ (a, b) :< (uncurry mzip <$> mzip fa fb)+ d :< n <- unC $ return $ (f *** g) c+ return $ d :< (n <|> fmap (>>= return . f *** g) m)++== {- `Monad` law `return a >>= k == k a` -}++ C $ do a :< fa <- unC ma+ b :< fb <- unC mb+ d :< n <- unC $ return $ (f *** g) (a, b)+ return $ d :< (n <|> fmap (>>= return . f *** g) (uncurry mzip <$> mzip fa fb))++== {- Definition of `return` -}++ C $ do a :< fa <- unC ma+ b :< fb <- unC mb+ d :< n <- unC $ C $ return $ (f *** g) (a, b) :< empty+ return $ d :< (n <|> fmap (>>= return . f *** g) (uncurry mzip <$> mzip fa fb))++== {- Unpack -}++ C $ do a :< fa <- unC ma+ b :< fb <- unC mb+ d :< n <- return $ (f *** g) (a, b) :< empty+ return $ d :< (n <|> fmap (>>= return . f *** g) (uncurry mzip <$> mzip fa fb))++== {- `Monad` law `return a >>= k == k a` -}++ C $ do a :< fa <- unC ma+ b :< fb <- unC mb+ return $ (f *** g) (a, b) :< (empty <|> fmap (>>= return . f *** g) (uncurry mzip <$> mzip fa fb))++== {- Identity of `<|>` -}++ C $ do a :< fa <- unC ma+ b :< fb <- unC mb+ return $ (f *** g) (a, b) :< fmap (>>= return . f *** g) (uncurry mzip <$> mzip fa fb)++== {- Definition of `liftM` -}++ C $ do a :< fa <- unC ma+ b :< fb <- unC mb+ return $ (f *** g) (a, b) :< fmap (liftM (f *** g)) (uncurry mzip <$> mzip fa fb)++== {- Definition of `<$>` -}++ C $ do a :< fa <- unC ma+ b :< fb <- unC mb+ return $ (f *** g) (a, b) :< fmap (liftM (f *** g)) (fmap (uncurry mzip) $ mzip fa fb)++== {- `Functor` composition -}++ C $ do a :< fa <- unC ma+ b :< fb <- unC mb+ return $ (f *** g) (a, b) :< fmap (liftM (f *** g) . uncurry mzip) $ mzip fa fb++== {- Coinduction hypothesis -}++ C $ do a :< fa <- unC ma+ b :< fb <- unC mb+ return $ (f *** g) (a, b) :< fmap (uncurry mzip . liftM f *** liftM g) $ mzip fa fb++== {- `Functor` composition -}++ C $ do c :< m <- unC ma+ k :< o <- unC mb+ return $ (f c, g k) :< fmap (uncurry mzip) $ fmap (liftM f *** liftM g) $ mzip m o++== {- `MonadZip` naturality -}++ C $ do c :< m <- unC ma+ k :< o <- unC mb+ return $ (f c, g k) :< fmap (uncurry mzip) $ mzip (fmap (liftM f) m) (fmap (liftM g) o))++== {- Definition of `<$>` -}++ C $ do c :< m <- unC ma+ k :< o <- unC mb+ return $ (f c, g k) :< (uncurry mzip <$> mzip (fmap (liftM f) m) (fmap (liftM g) o))++== {- Definition of `liftM` -}++ C $ do c :< m <- unC ma+ k :< o <- unC mb+ return $ (f c, g k) :< (uncurry mzip <$> mzip (fmap (>>= return . f) m) (fmap (>>= return . g) o))++== {- `Monad` law `return a >>= k == k a` -}++ C $ do c :< m <- unC ma+ a :< fa <- return $ f c :< fmap (>>= return . f) m+ k :< o <- unC mb+ b :< fb <- return $ g k :< fmap (>>= return . g) o+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)++== {- `Alternative` identity -}++ C $ do c :< m <- unC ma+ a :< fa <- return $ f c :< (empty <|> fmap (>>= return . f) m)+ k :< o <- unC mb+ b :< fb <- return $ g k :< (empty <|> fmap (>>= return . g) o)+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)++== {- `Monad` law `return a >>= k == k a` -}++ C $ do c :< m <- unC ma+ d :< n <- return $ f c :< empty+ a :< fa <- return $ d :< (n <|> fmap (>>= return . f) m)+ k :< o <- unC mb+ l :< p <- return $ g k :< empty+ b :< fb <- return $ l :< (p <|> fmap (>>= return . g) o)+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)++== {- Unpack -}++ C $ do c :< m <- unC ma+ d :< n <- unC $ C $ return $ f c :< empty+ a :< fa <- unC $ C $ return $ d :< (n <|> fmap (>>= return . f) m)+ k :< o <- unC mb+ l :< p <- unC $ C $ return $ g k :< empty+ b :< fb <- unC $ C $ return $ l :< (p <|> fmap (>>= return . g) o)+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)++== {- Definition of `return` -}++ C $ do c :< m <- unC ma+ d :< n <- unC $ return $ f c+ a :< fa <- unC $ C $ return $ d :< (n <|> fmap (>>= return . f) m)+ k :< o <- unC mb+ l :< p <- unC $ return $ g k+ b :< fb <- unC $ C $ return $ l :< (p <|> fmap (>>= return . g) o)+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)++== {- `Monad` law `m >>= (\x -> k x >>= h) == (m >>= k) >>= h` -}++ C $ do c :< m <- unC ma+ a :< fa <- unC $ C $ do d :< n <- unC $ return $ return $ f c+ return $ d :< (n <|> fmap (>>= return . f) m)+ k :< o <- unC mb+ b :< fb <- unC $ C $ do l :< p <- unC $ return $ return g k+ return $ l :< (p <|> fmap (>>= return . g) o)+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)++== {- `Monad` law `m >>= (\x -> k x >>= h) == (m >>= k) >>= h` -}++ C $ do a :< fa <- unC $ C $ do c :< m <- unC ma+ d :< n <- unC $ return $ f c+ return $ d :< (n <|> fmap (>>= return . f) m)+ b :< fb <- unC $ C $ do k :< o <- unC mb+ l :< p <- unC $ return $ g k+ return $ l :< (p <|> fmap (>>= return . g) o)+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)++== {- Definition of `(>>=)` -}++ C $ do a :< fa <- unC $ ma >>= return . f+ b :< fb <- unC $ mb >>= return . g+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)++== {- Definition of `liftM` -}++ C $ do a :< fa <- unC $ liftM f ma+ b :< fb <- unC $ liftM g mb+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)++== {- Definition of `mzip` -}++ mzip (liftM f ma) (liftM g mb)++.+```++## Information Preservation++```haskell+liftM (const ()) ma == liftM (const ()) mb --> munzip (mzip ma mb) == (ma, mb)+```++### Proof.++```haskell+ munzip (mzip ma mb)++== {- Definition of `munzip` -}++ (,)+ (liftM fst $ mzip ma mb)+ (liftM snd $ mzip ma mb)++== {- Definition of `mzip` -}++ (,)+ (liftM fst $ C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ (a, b) :< fmap (uncurry mzip) $ mzip fa fb)+ (liftM snd $ C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ (a, b) :< fmap (uncurry mzip) $ mzip fa fb)++== {- Definition of `liftM` -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ (a, b) :< fmap (uncurry mzip) $ mzip fa fb+ >>= return . fst)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ (a, b) :< fmap (uncurry mzip) $ mzip fa fb+ >>= return . snd)++== {- Definition of `(>>=)` -}++ (,)+ (C $ do c :< fc <- do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ (a, b) :< fmap (uncurry mzip) $ mzip fa fb+ d :< fd <- unC $ return $ fst c+ return $ d :< $ fd <|> fmap (>>= return . fst) fc)+ (C $ do c :< fc <- do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ (a, b) :< fmap (uncurry mzip) $ mzip fa fb+ d :< fd <- unC $ return $ snd c+ return $ d :< $ fd <|> fmap (>>= return . snd) fc)++== {- `Monad` law `m >>= (\x -> k x >>= h) == (m >>= k) >>= h` -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ c :< fc <- return $ (a, b) :< fmap (uncurry mzip) $ mzip fa fb+ d :< fd <- unC $ return $ fst c+ return $ d :< $ fd <|> fmap (>>= return . fst) fc)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ c :< fc <- return $ (a, b) :< fmap (uncurry mzip) $ mzip fa fb+ d :< fd <- unC $ return $ snd c+ return $ d :< $ fd <|> fmap (>>= return . snd) fc)++== {- `Monad` law `return a >>= k == k a` -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ d :< fd <- unC $ return $ fst (a, b)+ return $ d :< $ fd <|> fmap (>>= return . fst) $ fmap (uncurry mzip) $ mzip fa fb)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ d :< fd <- unC $ return $ snd (a, b)+ return $ d :< $ fd <|> fmap (>>= return . snd) $ fmap (uncurry mzip) $ mzip fa fb)++== {- Definition of `return` -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ d :< fd <- unC $ C $ return $ fst (a, b) :< empty+ return $ d :< $ fd <|> fmap (>>= return . fst) $ fmap (uncurry mzip) $ mzip fa fb)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ d :< fd <- unC $ C $ return $ snd (a, b) :< empty+ return $ d :< $ fd <|> fmap (>>= return . snd) $ fmap (uncurry mzip) $ mzip fa fb)++== {- Unpack -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ d :< fd <- return $ fst (a, b) :< empty+ return $ d :< $ fd <|> fmap (>>= return . fst) $ fmap (uncurry mzip) $ mzip fa fb)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ d :< fd <- return $ snd (a, b) :< empty+ return $ d :< $ fd <|> fmap (>>= return . snd) $ fmap (uncurry mzip) $ mzip fa fb)++== {- `Monad` law `return a >>= k == k a` -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ fst (a, b) :< $ empty <|> fmap (>>= return . fst) $ fmap (uncurry mzip) $ mzip fa fb)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ snd (a, b) :< $ empty <|> fmap (>>= return . snd) $ fmap (uncurry mzip) $ mzip fa fb)++== {- `Alternative` identity -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ fst (a, b) :< fmap (>>= return . fst) $ fmap (uncurry mzip) $ mzip fa fb)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ snd (a, b) :< fmap (>>= return . snd) $ fmap (uncurry mzip) $ mzip fa fb)++== {- Definition of `fst` -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ a :< fmap (>>= return . fst) $ fmap (uncurry mzip) $ mzip fa fb)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ b :< fmap (>>= return . snd) $ fmap (uncurry mzip) $ mzip fa fb)++== {- Definition of `liftM` -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ a :< fmap (liftM fst) $ fmap (uncurry mzip) $ mzip fa fb)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ b :< fmap (liftM snd) $ fmap (uncurry mzip) $ mzip fa fb)++== {- `Functor` composition -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ a :< fmap (liftM fst . uncurry mzip) $ mzip fa fb)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ b :< fmap (liftM snd . uncurry mzip) $ mzip fa fb)++== {- Definition of `unzip` -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ a :< fmap (fst . unzip . uncurry mzip) $ mzip fa fb)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ b :< fmap (snd . unzip . uncurry mzip) $ mzip fa fb)++== {- Coinduction hypothesis -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ a :< fmap fst $ mzip fa fb)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ b :< fmap snd $ mzip fa fb)++== {- `Monad` law `fmap f m == m >>= return . f` and definition of `liftM` -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ a :< liftM fst $ mzip fa fb)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ b :< liftM snd $ mzip fa fb)++== {- Definition of `unzip` -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ a :< fst $ unzip $ mzip fa fb)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ b :< snd $ unzip $ mzip fa fb)++== {- `MonadZip` information preservation -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ a :< fst (fa, fb))+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ b :< snd (fa, fb))++== {- Definition of `fst` and `snd` -}++ (,)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ a :< fa)+ (C $ do (a :< fa, b :< fb) <- mzip (unC ma) (unC mb)+ return $ b :< fb)++== {- Definition of `fst` and `snd` -}++ (,)+ (C $ mzip (unC ma) (unC mb) >>= return . fst)+ (C $ mzip (unC ma) (unC mb) >>= return . snd)++== {- Definition of `liftM` -}++ (,)+ (C $ liftM fst $ mzip (unC ma) (unC mb))+ (C $ liftM snd $ mzip (unC ma) (unC mb))++== {- Definition of `unzip` -}++ (,)+ (C $ fst $ unzip $ mzip (unC ma) (unC mb))+ (C $ snd $ unzip $ mzip (unC ma) (unC mb))++== {- `MonadZip` information preservation -}++ (,)+ (C $ fst $ (unC ma, unC mb))+ (C $ snd $ (unC ma, unC mb))++== {- Definition of `fst` and `snd` -}++ (,)+ (C $ unC ma)+ (C $ unC mb)++== {- Pack -}++ (ma, mb)++.+```
free.cabal view
@@ -1,6 +1,6 @@ name: free category: Control, Monads-version: 4.5+version: 4.6 license: BSD3 cabal-version: >= 1.10 license-file: LICENSE@@ -33,6 +33,9 @@ .vim.custom README.markdown CHANGELOG.markdown+ HLint.hs+ doc/proof/Control/Comonad/Cofree/*.md+ doc/proof/Control/Comonad/Trans/Cofree/*.md source-repository head type: git@@ -80,6 +83,5 @@ Control.Monad.Trans.Free Control.Monad.Trans.Free.Church Control.Monad.Trans.Iter- Control.MonadPlus.Free ghc-options: -Wall
src/Control/Alternative/Free.hs view
@@ -1,6 +1,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-} #if __GLASGOW_HASKELL__ >= 707 {-# LANGUAGE DeriveDataTypeable #-} #endif@@ -20,6 +21,7 @@ ---------------------------------------------------------------------------- module Control.Alternative.Free ( Alt(..)+ , AltF(..) , runAlt , liftAlt , hoistAlt@@ -33,73 +35,99 @@ import Data.Typeable #endif --- | The free 'Alternative' for a 'Functor' @f@.-data Alt f a where- Pure :: a -> Alt f a- Ap :: f a -> Alt f (a -> b) -> Alt f b- Alt :: [Alt f a] -> Alt f a+infixl 3 `Ap`++data AltF f a where+ Ap :: f a -> Alt f (a -> b) -> AltF f b+ Pure :: a -> AltF f a #if __GLASGOW_HASKELL__ >= 707- deriving (Typeable)+ deriving Typeable #endif --- | Given a natural transformation from @f@ to @g@, this gives a canonical monoidal natural transformation from @'Alt' f@ to @g@.-runAlt :: Alternative g => (forall x. f x -> g x) -> Alt f a -> g a-runAlt _ (Pure x) = pure x-runAlt u (Ap f x) = flip id <$> u f <*> runAlt u x-runAlt u (Alt as) = foldr (\a r -> runAlt u a <|> r) empty as+newtype Alt f a = Alt { alternatives :: [AltF f a] }+#if __GLASGOW_HASKELL__ >= 707+ deriving Typeable+#endif -instance Functor (Alt f) where- fmap f (Pure a) = Pure (f a)- fmap f (Ap x y) = Ap x ((f .) <$> y)- fmap f (Alt as) = Alt (fmap f <$> as)+instance Functor f => Functor (AltF f) where+ fmap f (Pure a) = Pure $ f a+ fmap f (Ap x g) = x `Ap` fmap (f .) g -instance Apply (Alt f) where- Pure f <.> y = fmap f y- Ap x y <.> z = Ap x (flip <$> y <.> z)- Alt as <.> z = Alt (map (<.> z) as) -- This assumes 'left distribution'+instance Functor f => Functor (Alt f) where+ fmap f (Alt xs) = Alt $ map (fmap f) xs -instance Applicative (Alt f) where+instance Functor f => Applicative (AltF f) where pure = Pure- Pure f <*> y = fmap f y- Ap x y <*> z = Ap x (flip <$> y <*> z)- Alt as <*> z = Alt (map (<*> z) as) -- This assumes 'left distribution'+ {-# INLINE pure #-}+ (Pure f) <*> y = fmap f y -- fmap+ y <*> (Pure a) = fmap ($ a) y -- interchange+ (Ap a f) <*> b = a `Ap` (flip <$> f <*> (Alt [b]))+ {-# INLINE (<*>) #-} -instance Alternative (Alt f) where+instance Functor f => Applicative (Alt f) where+ pure a = Alt [pure a]+ {-# INLINE pure #-}++ (Alt xs) <*> ys = Alt (xs >>= alternatives . (`ap'` ys))+ where+ ap' :: (Functor f) => AltF f (a -> b) -> Alt f a -> Alt f b++ Pure f `ap'` u = fmap f u+ (u `Ap` f) `ap'` v = Alt [u `Ap` (flip <$> f) <*> v]+ {-# INLINE (<*>) #-}++liftAltF :: (Functor f) => f a -> AltF f a+liftAltF x = x `Ap` pure id+{-# INLINE liftAltF #-}++-- | A version of 'lift' that can be used with just a 'Functor' for @f@.+liftAlt :: (Functor f) => f a -> Alt f a+liftAlt = Alt . (:[]) . liftAltF+{-# INLINE liftAlt #-}++-- | Given a natural transformation from @f@ to @g@, this gives a canonical monoidal natural transformation from @'Alt' f@ to @g@.+runAlt :: forall f g a. Alternative g => (forall x. f x -> g x) -> Alt f a -> g a+runAlt u xs0 = go xs0 where++ go :: Alt f b -> g b+ go (Alt xs) = foldr (\r a -> (go2 r) <|> a) empty xs++ go2 :: AltF f b -> g b+ go2 (Pure a) = pure a+ go2 (Ap x f) = flip id <$> u x <*> go f+{-# INLINABLE runAlt #-}++instance (Functor f) => Apply (Alt f) where+ (<.>) = (<*>)+ {-# INLINE (<.>) #-}++instance (Functor f) => Alternative (Alt f) where empty = Alt [] {-# INLINE empty #-}- Alt [] <|> r = r- l <|> Alt [] = l Alt as <|> Alt bs = Alt (as ++ bs)- l <|> r = Alt [l, r] {-# INLINE (<|>) #-} -instance Semigroup (Alt f a) where+instance (Functor f) => Semigroup (Alt f a) where (<>) = (<|>) {-# INLINE (<>) #-} -instance Monoid (Alt f a) where+instance (Functor f) => Monoid (Alt f a) where mempty = empty {-# INLINE mempty #-} mappend = (<|>) {-# INLINE mappend #-}- mconcat as = fromList (as >>= toList)- where- toList (Alt xs) = xs- toList x = [x]- fromList [x] = x- fromList xs = Alt xs+ mconcat as = Alt (as >>= alternatives) {-# INLINE mconcat #-} --- | A version of 'lift' that can be used with just a 'Functor' for @f@.-liftAlt :: f a -> Alt f a-liftAlt x = Ap x (Pure id)-{-# INLINE liftAlt #-}+hoistAltF :: (forall a. f a -> g a) -> AltF f b -> AltF g b+hoistAltF _ (Pure a) = Pure a+hoistAltF f (Ap x y) = Ap (f x) (hoistAlt f y)+{-# INLINE hoistAltF #-} -- | Given a natural transformation from @f@ to @g@ this gives a monoidal natural transformation from @Alt f@ to @Alt g@. hoistAlt :: (forall a. f a -> g a) -> Alt f b -> Alt g b-hoistAlt _ (Pure a) = Pure a-hoistAlt f (Ap x y) = Ap (f x) (hoistAlt f y)-hoistAlt f (Alt as) = Alt (map (hoistAlt f) as)+hoistAlt f (Alt as) = Alt (map (hoistAltF f) as)+{-# INLINE hoistAlt #-} #if defined(GHC_TYPEABLE) && __GLASGOW_HASKELL__ < 707 instance Typeable1 f => Typeable1 (Alt f) where@@ -107,12 +135,19 @@ f :: Alt f a -> f a f = undefined -altTyCon :: TyCon+instance Typeable1 f => Typeable1 (AltF f) where+ typeOf1 t = mkTyConApp altFTyCon [typeOf1 (f t)] where+ f :: AltF f a -> f a+ f = undefined++altTyCon, altFTyCon :: TyCon #if __GLASGOW_HASKELL__ < 704 altTyCon = mkTyCon "Control.Alternative.Free.Alt"+altFTyCon = mkTyCon "Control.Alternative.Free.AltF" #else altTyCon = mkTyCon3 "free" "Control.Alternative.Free" "Alt"+altFTyCon = mkTyCon3 "free" "Control.Alternative.Free" "AltF" #endif {-# NOINLINE altTyCon #-}-+{-# NOINLINE altFTyCon #-} #endif
src/Control/Applicative/Free.hs view
@@ -18,7 +18,15 @@ -- 'Applicative' functors for free ---------------------------------------------------------------------------- module Control.Applicative.Free- ( Ap(..)+ (+ -- | Compared to the free monad, they are less expressive. However, they are also more+ -- flexible to inspect and interpret, as the number of ways in which+ -- the values can be nested is more limited.+ --+ -- See <http://paolocapriotti.com/assets/applicative.pdf Free Applicative Functors>,+ -- by Paolo Capriotti and Ambrus Kaposi, for some applications.++ Ap(..) , runAp , liftAp , hoistAp@@ -41,6 +49,8 @@ #endif -- | Given a natural transformation from @f@ to @g@, this gives a canonical monoidal natural transformation from @'Ap' f@ to @g@.+--+-- prop> runAp t == retractApp . hoistApp t runAp :: Applicative g => (forall x. f x -> g x) -> Ap f a -> g a runAp _ (Pure x) = pure x runAp u (Ap f x) = flip id <$> u f <*> runAp u x@@ -68,6 +78,10 @@ hoistAp _ (Pure a) = Pure a hoistAp f (Ap x y) = Ap (f x) (hoistAp f y) +-- | Interprets the free applicative functor over f using the semantics for+-- `pure` and `<*>` given by the Applicative instance for f.+--+-- prop> retractApp == runAp id retractAp :: Applicative f => Ap f a -> f a retractAp (Pure a) = pure a retractAp (Ap x y) = x <**> retractAp y
src/Control/Comonad/Cofree.hs view
@@ -87,6 +87,16 @@ -- -- * @'Cofree' ((->) b)'@ describes a Moore machine with states labeled with values of type a, and transitions on edges of type b. --+-- Furthermore, if the functor @f@ forms a monoid (for example, by+-- being an instance of 'Alternative'), the resulting 'Comonad' is+-- also a 'Monad'. See+-- <http://www.cs.appstate.edu/~johannp/jfp06-revised.pdf Monadic Augment and Generalised Shortcut Fusion> by Neil Ghani et al., Section 4.3+-- for more details.+--+-- In particular, if @f a ≡ [a]@, the+-- resulting data structure is a <https://en.wikipedia.org/wiki/Rose_tree Rose tree>.+-- For a practical application, check +-- <https://personal.cis.strath.ac.uk/neil.ghani/papers/ghani-calco07 Higher Dimensional Trees, Algebraically> by Neil Ghani et al. data Cofree f a = a :< f (Cofree f a) #if __GLASGOW_HASKELL__ >= 707 deriving (Typeable)@@ -180,7 +190,9 @@ (v, w) <- readsPrec 5 t]) r instance (Eq (f (Cofree f a)), Eq a) => Eq (Cofree f a) where+#ifndef HLINT a :< as == b :< bs = a == b && as == bs+#endif instance (Ord (f (Cofree f a)), Ord a) => Ord (Cofree f a) where compare (a :< as) (b :< bs) = case compare a b of
src/Control/Comonad/Trans/Cofree.hs view
@@ -21,7 +21,7 @@ ---------------------------------------------------------------------------- module Control.Comonad.Trans.Cofree ( CofreeT(..)- , cofree, runCofree+ , Cofree, cofree, runCofree , CofreeF(..) , ComonadCofree(..) , headF@@ -41,6 +41,9 @@ import Data.Functor.Identity import Data.Semigroup import Data.Traversable+import Control.Monad (liftM)+import Control.Monad.Trans+import Control.Monad.Zip import Prelude hiding (id,(.)) #if defined(GHC_TYPEABLE) || __GLASGOW_HASKELL__ >= 707@@ -85,13 +88,36 @@ -- | This is a cofree comonad of some functor @f@, with a comonad @w@ threaded through it at each level. newtype CofreeT f w a = CofreeT { runCofreeT :: w (CofreeF f a (CofreeT f w a)) }+#if __GLASGOW_HASKELL__ >= 707+ deriving Typeable+#endif +-- | The cofree `Comonad` of a functor @f@. type Cofree f = CofreeT f Identity +{- |+Wrap another layer around a cofree comonad value.++@cofree@ is a right inverse of `runCofree`.++@+runCofree . cofree == id+@+-} cofree :: CofreeF f a (Cofree f a) -> Cofree f a cofree = CofreeT . Identity {-# INLINE cofree #-} ++{- |+Unpeel the first layer off a cofree comonad value.++@runCofree@ is a right inverse of `cofree`.++@+cofree . runCofree == id+@+-} runCofree :: Cofree f a -> CofreeF f a (Cofree f a) runCofree = runIdentity . runCofreeT {-# INLINE runCofree #-}@@ -129,12 +155,39 @@ instance Ord (w (CofreeF f a (CofreeT f w a))) => Ord (CofreeT f w a) where compare (CofreeT a) (CofreeT b) = compare a b +instance (Alternative f, Monad w) => Monad (CofreeT f w) where+ return = CofreeT . return . (:< empty)+ {-# INLINE return #-}+ CofreeT cx >>= f = CofreeT $ do+ a :< m <- cx+ b :< n <- runCofreeT $ f a+ return $ b :< (n <|> fmap (>>= f) m)+++instance (Alternative f, Applicative w) => Applicative (CofreeT f w) where+ pure = CofreeT . pure . (:< empty)+ {-# INLINE pure #-}+ wf <*> wa = CofreeT $ go <$> runCofreeT wf <*> runCofreeT wa where+ go (f :< t) a = case bimap f (fmap f) a of+ b :< n -> b :< (n <|> fmap (<*> wa) t)+ {-# INLINE (<*>) #-}++instance Alternative f => MonadTrans (CofreeT f) where+ lift = CofreeT . liftM (:< empty)++instance (Alternative f, MonadZip f, MonadZip m) => MonadZip (CofreeT f m) where+ mzip (CofreeT ma) (CofreeT mb) = CofreeT $ do+ (a :< fa, b :< fb) <- mzip ma mb+ return $ (a, b) :< (uncurry mzip <$> mzip fa fb)+ -- | Unfold a @CofreeT@ comonad transformer from a coalgebra and an initial comonad. coiterT :: (Functor f, Comonad w) => (w a -> f (w a)) -> w a -> CofreeT f w a-coiterT psi = CofreeT . (extend $ \w -> extract w :< fmap (coiterT psi) (psi w))+coiterT psi = CofreeT . extend (\w -> extract w :< fmap (coiterT psi) (psi w)) -#if defined(GHC_TYPEABLE) && __GLASGOW_HASKELL__ < 707+#if defined(GHC_TYPEABLE) +#if __GLASGOW_HASKELL__ < 707+ instance Typeable1 f => Typeable2 (CofreeF f) where typeOf2 t = mkTyConApp cofreeFTyCon [typeOf1 (f t)] where f :: CofreeF f a b -> f a@@ -157,6 +210,10 @@ #endif {-# NOINLINE cofreeTTyCon #-} {-# NOINLINE cofreeFTyCon #-}++#else+#define Typeable1 Typeable+#endif instance ( Typeable1 f, Typeable a, Typeable b
src/Control/Comonad/Trans/Coiter.hs view
@@ -21,6 +21,17 @@ ---------------------------------------------------------------------------- module Control.Comonad.Trans.Coiter (+ -- |+ -- Coiterative comonads represent non-terminating, productive computations.+ --+ -- They are the dual notion of iterative monads. While iterative computations+ -- produce no values or eventually terminate with one, coiterative+ -- computations constantly produce values and they never terminate.+ -- + -- It's simpler form, 'Coiter', is an infinite stream of data. 'CoiterT'+ -- extends this so that each step of the computation can be performed in+ -- a comonadic context.+ -- * The coiterative comonad transformer CoiterT(..) -- * The coiterative comonad@@ -29,12 +40,18 @@ , unfold -- * Cofree comonads , ComonadCofree(..)+ -- * Example+ -- $example ) where -import Control.Arrow+import Control.Arrow hiding (second) import Control.Comonad-import Control.Comonad.Trans.Class import Control.Comonad.Cofree.Class+import Control.Comonad.Env.Class+import Control.Comonad.Hoist.Class+import Control.Comonad.Store.Class+import Control.Comonad.Traced.Class+import Control.Comonad.Trans.Class import Control.Category import Data.Bifunctor import Data.Bifoldable@@ -50,14 +67,23 @@ -- | This is the coiterative comonad generated by a comonad newtype CoiterT w a = CoiterT { runCoiterT :: w (a, CoiterT w a) }+#if defined(GHC_TYPEABLE) && __GLASGOW_HASKELL__ >= 707+ deriving Typeable+#endif -- | The coiterative comonad type Coiter = CoiterT Identity +-- | Prepends a result to a coiterative computation.+--+-- prop> runCoiter . uncurry coiter == id coiter :: a -> Coiter a -> Coiter a coiter a as = CoiterT $ Identity (a,as) {-# INLINE coiter #-} +-- | Extracts the first result from a coiterative computation.+--+-- prop> uncurry coiter . runCoiter == id runCoiter :: Coiter a -> (a, Coiter a) runCoiter = runIdentity . runCoiterT {-# INLINE runCoiter #-}@@ -82,7 +108,32 @@ instance Comonad w => ComonadCofree Identity (CoiterT w) where unwrap = Identity . snd . extract . runCoiterT {-# INLINE unwrap #-}+ +instance ComonadEnv e w => ComonadEnv e (CoiterT w) where+ ask = ask . lower+ {-# INLINE ask #-}+ +instance ComonadHoist CoiterT where+ cohoist g = CoiterT . fmap (second (cohoist g)) . g . runCoiterT +instance ComonadTraced m w => ComonadTraced m (CoiterT w) where+ trace m = trace m . lower+ {-# INLINE trace #-}++instance ComonadStore s w => ComonadStore s (CoiterT w) where+ pos = pos . lower+ peek s = peek s . lower+ peeks f = peeks f . lower+ seek = seek+ seeks = seeks+ experiment f = experiment f . lower+ {-# INLINE pos #-}+ {-# INLINE peek #-}+ {-# INLINE peeks #-}+ {-# INLINE seek #-}+ {-# INLINE seeks #-}+ {-# INLINE experiment #-}+ instance Show (w (a, CoiterT w a)) => Show (CoiterT w a) where showsPrec d w = showParen (d > 10) $ showString "CoiterT " . showsPrec 11 w@@ -103,7 +154,8 @@ unfold :: Comonad w => (w a -> a) -> w a -> CoiterT w a unfold psi = CoiterT . extend (extract &&& unfold psi . extend psi) -#if defined(GHC_TYPEABLE) && __GLASGOW_HASKELL__ < 707+#if defined(GHC_TYPEABLE)+#if __GLASGOW_HASKELL__ < 707 instance Typeable1 w => Typeable1 (CoiterT w) where typeOf1 t = mkTyConApp coiterTTyCon [typeOf1 (w t)] where@@ -118,6 +170,10 @@ #endif {-# NOINLINE coiterTTyCon #-} +#else+#define Typeable1 Typeable+#endif+ instance ( Typeable1 w, Typeable a , Data (w (a, CoiterT w a))@@ -138,4 +194,114 @@ coiterTDataType :: DataType coiterTDataType = mkDataType "Control.Comonad.Trans.Coiter.CoiterT" [coiterTConstr] {-# NOINLINE coiterTDataType #-}+ #endif++-- BEGIN Coiter.lhs+{- $example+This is literate Haskell! To run the example, open the source and copy+this comment block into a new file with '.lhs' extension.++Many numerical approximation methods compute infinite sequences of results; each,+hopefully, more accurate than the previous one.++<https://en.wikipedia.org/wiki/Newton's_method Newton's method>+to find zeroes of a function is one such algorithm.+ +@ \{\-\# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances \#\-\} @++> {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}++> import Control.Comonad.Trans.Coiter+> import Control.Comonad.Env+> import Control.Applicative+> import Data.Foldable (toList, find)++> data Function = Function {+> -- Function to find zeroes of+> function :: Double -> Double,+> -- Derivative of the function+> derivative :: Double -> Double+> }+> +> data Result = Result {+> -- Estimated zero of the function+> value :: Double,+> -- Estimated distance to the actual zero+> xerror :: Double,+> -- How far is value from being an actual zero; that is,+> -- the difference between @0@ and @f value@+> ferror :: Double+> } deriving (Show)+> +> data Outlook = Outlook { result :: Result,+> -- Whether the result improves in future steps+> progress :: Bool } deriving (Show)++To make our lives easier, we will store the problem at hand using the Env+environment comonad.++> type Solution a = CoiterT (Env Function) a++Problems consist of a function and its derivative as the environment, and+an initial value.++> type Problem = Env Function Double++We can express an iterative algorithm using unfold over an initial environment.+ +> newton :: Problem -> Solution Double+> newton = unfold (\wd ->+> let f = asks function wd in+> let df = asks derivative wd in+> let x = extract wd in+> x - f x / df x)+> +> ++To estimate the error, we look forward one position in the stream. The next value+will be much more precise than the current one, so we can consider it as the+actual result.++We know that the exact value of a function at one of it's zeroes is 0. So,+@ferror@ can be computed exactly as @abs (f a - f 0) == abs (f a)@++> estimateError :: Solution Double -> Result+> estimateError s =+> let a:a':_ = toList s in+> let f = asks function s in+> Result { value = a,+> xerror = abs $ a - a',+> ferror = abs $ f a+> }++To get a sense of when the algorithm is making any progress, we can sample the+future and check if the result improves at all.+ +> estimateOutlook :: Int -> Solution Result -> Outlook+> estimateOutlook sampleSize solution =+> let sample = map ferror $ take sampleSize $ tail $ toList solution in+> let result = extract solution in+> Outlook { result = result,+> progress = ferror result > minimum sample } ++To compute the square root of @c@, we solve the equation @x*x - c = 0@. We will+stop whenever the accuracy of the result doesn't improve in the next 5 steps.++The starting value for our algorithm is @c@ itself. One could compute a better+estimate, but the algorithm converges fast enough that it's not really worth it.++> squareRoot :: Double -> Maybe Result+> squareRoot c = let problem = flip env c (Function { function = (\x -> x*x - c),+> derivative = (\x -> 2*x) })+> in +> fmap result $ find (not . progress) $ +> newton problem =>> estimateError =>> estimateOutlook 5++This program will output the result together with the error.++> main :: IO ()+> main = putStrLn $ show $ squareRoot 4++-}+-- END Coiter.lhs
src/Control/Monad/Free.hs view
@@ -27,6 +27,7 @@ , iter , iterM , hoistFree+ , toFreeT , _Pure, _Free ) where @@ -34,6 +35,7 @@ import Control.Monad (liftM, MonadPlus(..)) import Control.Monad.Fix import Control.Monad.Trans.Class+import qualified Control.Monad.Trans.Free as FreeT import Control.Monad.Free.Class import Control.Monad.Reader.Class import Control.Monad.Writer.Class@@ -260,6 +262,12 @@ hoistFree :: Functor g => (forall a. f a -> g a) -> Free f b -> Free g b hoistFree _ (Pure a) = Pure a hoistFree f (Free as) = Free (hoistFree f <$> f as)++-- | Convert a 'Free' monad from "Control.Monad.Free" to a 'FreeT.FreeT' monad+-- from "Control.Monad.Trans.Free".+toFreeT :: (Functor f, Monad m) => Free f a -> FreeT.FreeT f m a+toFreeT (Pure a) = FreeT.FreeT (return (FreeT.Pure a))+toFreeT (Free f) = FreeT.FreeT (return (FreeT.Free (fmap toFreeT f))) -- | This is @Prism' (Free f a) a@ in disguise --
src/Control/Monad/Free/Church.hs view
@@ -14,10 +14,38 @@ -- -- \"Free Monads for Less\" ----- This is based on the \"Free Monads for Less\" series of articles:+-- The most straightforward way of implementing free monads is as a recursive+-- datatype that allows for arbitrarily deep nesting of the base functor. This is+-- akin to a tree, with the leaves containing the values, and the nodes being a+-- level of 'Functor' over subtrees.+-- +-- For each time that the `fmap` or `>>=` operations is used, the old tree is+-- traversed up to the leaves, a new set of nodes is allocated, and+-- the old ones are garbage collected. Even if the Haskell runtime+-- optimizes some of the overhead through laziness and generational garbage+-- collection, the asymptotic runtime is still quadratic. ----- <http://comonad.com/reader/2011/free-monads-for-less/>--- <http://comonad.com/reader/2011/free-monads-for-less-2/>+-- On the other hand, if the Church encoding is used, the tree only needs to be+-- constructed once, because:+--+-- * All uses of `fmap` are collapsed into a single one, so that the values on the+-- _leaves_ are transformed in one pass.+-- +-- prop> fmap f . fmap g == fmap (f . g)+-- +-- * All uses of `>>=` are right associated, so that every new subtree created+-- is final.+-- +-- prop> (m >>= f) >>= g == m >>= (\x -> f x >>= g)+--+-- Asymptotically, the Church encoding supports the monadic operations more+-- efficiently than the naïve 'Free'.+--+-- This is based on the \"Free Monads for Less\" series of articles by Edward Kmett:+--+-- * <http://comonad.com/reader/2011/free-monads-for-less/ Free monads for less — Part 1>+--+-- * <http://comonad.com/reader/2011/free-monads-for-less-2/ Free monads for less — Part 2> ---------------------------------------------------------------------------- module Control.Monad.Free.Church ( F(..)@@ -42,9 +70,9 @@ import Data.Functor.Bind -- | The Church-encoded free monad for a functor @f@.---+-- -- It is /asymptotically/ more efficient to use ('>>=') for 'F' than it is to ('>>=') with 'Free'.---+-- -- <http://comonad.com/reader/2011/free-monads-for-less-2/> newtype F f a = F { runF :: forall r. (a -> r) -> (f r -> r) -> r } @@ -60,7 +88,7 @@ instance Applicative (F f) where pure a = F (\kp _ -> kp a)- F f <*> F g = F (\kp kf -> f (\a -> g (\b -> kp (a b)) kf) kf)+ F f <*> F g = F (\kp kf -> f (\a -> g (kp . a) kf) kf) instance Alternative f => Alternative (F f) where empty = F (\_ kf -> kf empty)@@ -127,15 +155,14 @@ go kp kf (Free fma) = kf (fmap (go kp kf) fma) -- | Improve the asymptotic performance of code that builds a free monad with only binds and returns by using 'F' behind the scenes.---+-- -- This is based on the \"Free Monads for Less\" series of articles by Edward Kmett:------ <http://comonad.com/reader/2011/free-monads-for-less/>--- <http://comonad.com/reader/2011/free-monads-for-less-2/>------ and \"Asymptotic Improvement of Computations over Free Monads\" by Janis Voightländer:------ <http://www.iai.uni-bonn.de/~jv/mpc08.pdf>+-- +-- * <http://comonad.com/reader/2011/free-monads-for-less/ Free monads for less — Part 1>+-- +-- * <http://comonad.com/reader/2011/free-monads-for-less-2/ Free monads for less — Part 2>+-- +-- and <http://www.iai.uni-bonn.de/~jv/mpc08.pdf \"Asymptotic Improvement of Computations over Free Monads\"> by Janis Voightländer. improve :: Functor f => (forall m. MonadFree f m => m a) -> Free f a improve m = fromF m {-# INLINE improve #-}
src/Control/Monad/Free/TH.hs view
@@ -1,4 +1,3 @@-{-# LANGUAGE TemplateHaskell #-} ----------------------------------------------------------------------------- -- | -- Module : Control.Monad.Trans.TH@@ -13,7 +12,13 @@ -- ---------------------------------------------------------------------------- module Control.Monad.Free.TH- ( makeFree+ (+ -- * Free monadic actions+ makeFree+ -- $doc++ -- ** Example+ -- $example ) where import Control.Arrow@@ -111,13 +116,13 @@ maybe' <- ConT <$> findTypeOrFail "Maybe" nothing' <- ConE <$> findValueOrFail "Nothing" just' <- ConE <$> findValueOrFail "Just"- return $ (AppT maybe' t, [nothing', mapRet (AppE just') e])+ return (AppT maybe' t, [nothing', mapRet (AppE just') e]) unifyT x y@(TupleT 0, _) = second reverse <$> unifyT y x unifyT (t1, e1) (t2, e2) = do either' <- ConT <$> findTypeOrFail "Either" left' <- ConE <$> findValueOrFail "Left" right' <- ConE <$> findValueOrFail "Right"- return $ (AppT (AppT either' t1) t2, [mapRet (AppE left') e1, mapRet (AppE right') e2])+ return (AppT (AppT either' t1) t2, [mapRet (AppE left') e1, mapRet (AppE right') e2]) -- | Unifying a list of types (possibly refining expressions). -- Name is used when the return type is supposed to be arbitrary.@@ -152,8 +157,12 @@ q = map PlainTV $ qa ++ m : ns qa = case retType of VarT b | a == b -> [a]; _ -> [] f' = foldl AppT f (map VarT ns)- return $+ return+#if __GLASGOW_HASKELL__ >= 709+ [ SigD opName (ForallT q [ConT monadFree `AppT` f' `AppT` VarT m] opType)+#else [ SigD opName (ForallT q [ClassP monadFree [f', VarT m]] opType)+#endif , FunD opName [ Clause pat (NormalB $ AppE (VarE liftF) fval) [] ] ] -- | Provide free monadic actions for a single value constructor.@@ -162,6 +171,7 @@ case con of NormalC cName fields -> liftCon' f n ns cName $ map snd fields RecC cName fields -> liftCon' f n ns cName $ map (\(_, _, ty) -> ty) fields+ InfixC (_,t1) cName (_,t2) -> liftCon' f n ns cName [t1, t2] _ -> fail $ "liftCon: Don't know how to lift " ++ show con -- | Provide free monadic actions for a type declaration.@@ -184,3 +194,183 @@ TyConI dec -> liftDec dec _ -> fail "makeFree expects a type constructor" +{- $doc+ To generate free monadic actions from a @Type@, it must be a @data@+ declaration with at least one free variable. For each constructor of the type, a+ new function will be declared.++ Consider the following generalized definitions:++ > data Type a1 a2 … aN param = …+ > | FooBar t1 t2 t3 … tJ+ > | (:+) t1 t2 t3 … tJ+ > | t1 :* t2+ > | t1 `Bar` t2+ > | Baz { x :: t1, y :: t2, …, z :: tJ }+ > | …++ where each of the constructor arguments @t1, …, tJ@ is either:++ 1. A type, perhaps depending on some of the @a1, …, aN@.++ 2. A type dependent on @param@, of the form @s1 -> … -> sM -> param@, M ≥ 0.+ At most 2 of the @t1, …, tJ@ may be of this form. And, out of these two,+ at most 1 of them may have @M == 0@; that is, be of the form @param@.++ For each constructor, a function will be generated. First, the name+ of the function is derived from the name of the constructor:++ * For prefix constructors, the name of the constructor with the first+ letter in lowercase (e.g. @FooBar@ turns into @fooBar@).++ * For infix constructors, the name of the constructor with the first+ character (a colon @:@), removed (e.g. @:+@ turns into @+@).++ Then, the type of the function is derived from the arguments to the constructor:++ > …+ > fooBar :: (MonadFree Type m) => t1' -> … -> tK' -> m ret+ > (+) :: (MonadFree Type m) => t1' -> … -> tK' -> m ret+ > baz :: (MonadFree Type m) => t1' -> … -> tK' -> m ret+ > …++ The @t1', …, tK'@ are those @t1@ … @tJ@ that only depend on the+ @a1, …, aN@.++ The type @ret@ depends on those constructor arguments that reference the+ @param@ type variable:++ 1. If no arguments to the constructor depend on @param@, @ret ≡ a@, where+ @a@ is a fresh type variable.++ 2. If only one argument in the constructor depends on @param@, then+ @ret ≡ (s1, …, sM)@. In particular, f @M == 0@, then @ret ≡ ()@; if @M == 1@, @ret ≡ s1@.++ 3. If two arguments depend on @param@, (e.g. @u1 -> … -> uL -> param@ and+ @v1 -> … -> vM -> param@, then @ret ≡ Either (u1, …, uL) (v1, …, vM)@.++ Note that @Either a ()@ and @Either () a@ are both isomorphic to @Maybe a@.+ Because of this, when @L == 0@ or @M == 0@ in case 3., the type of+ @ret@ is simplified:++ * @ret ≡ Either (u1, …, uL) ()@ is rewritten to @ret ≡ Maybe (u1, …, uL)@.++ * @ret ≡ Either () (v1, …, vM)@ is rewritten to @ret ≡ Maybe (v1, …, vM)@.++-}++-- BEGIN Teletype.lhs+{- $example++This is literate Haskell! To run this example, open the source of this+module and copy the whole comment block into a file with '.lhs'+extension. For example, @Teletype.lhs@.++@\{\-\# LANGUAGE DeriveFunctor, TemplateHaskell, FlexibleContexts \#\-\}@++> {-# LANGUAGE DeriveFunctor, TemplateHaskell, FlexibleContexts #-} --++> import Control.Monad (mfilter)+> import Control.Monad.Loops (unfoldM)+> import Control.Monad.Free (liftF, Free, iterM, MonadFree)+> import Control.Monad.Free.TH (makeFree)+> import Control.Applicative ((<$>))+> import System.IO (isEOF)+> import Control.Exception (catch)+> import System.IO.Error (ioeGetErrorString)+> import System.Exit (exitSuccess)++First, we define a data type with the primitive actions of a teleprinter. The+@param@ will stand for the next action to execute.++> type Error = String+>+> data Teletype param = Halt -- Abort (ignore all following instructions)+> | NL param -- Newline+> | Read (Char -> param) -- Get a character from the terminal+> | ReadOrEOF { onEOF :: param,+> onChar :: Char -> param } -- GetChar if not end of file+> | ReadOrError (Error -> param)+> (Char -> param) -- GetChar with error code+> | param :\^^ String -- Write a message to the terminal+> | (:%) param String [String] -- String interpolation+> deriving (Functor)++By including a 'makeFree' declaration:++> makeFree ''Teletype++the following functions have been made available:++@+ halt :: (MonadFree Teletype m) => m a+ nL :: (MonadFree Teletype m) => m ()+ read :: (MonadFree Teletype m) => m Char+ readOrEOF :: (MonadFree Teletype m) => m (Maybe Char)+ readOrError :: (MonadFree Teletype m) => m (Either Error Char)+ (\\^^) :: (MonadFree Teletype m) => String -> m ()+ (%) :: (MonadFree Teletype m) => String -> [String] -> m ()+@++To make use of them, we need an instance of 'MonadFree Teletype'. Since 'Teletype' is a+'Functor', we can use the one provided in the 'Control.Monad.Free' package.++> type TeletypeM = Free Teletype++Programs can be run in different ways. For example, we can use the+system terminal through the @IO@ monad.++> runTeletypeIO :: TeletypeM a -> IO a+> runTeletypeIO = iterM run where+> run :: Teletype (IO a) -> IO a+> run Halt = do+> putStrLn "This conversation can serve no purpose anymore. Goodbye."+> exitSuccess+>+> run (Read f) = getChar >>= f+> run (ReadOrEOF eof f) = isEOF >>= \b -> if b then eof+> else getChar >>= f+>+> run (ReadOrError ferror f) = catch (getChar >>= f) (ferror . ioeGetErrorString)+> run (NL rest) = putChar '\n' >> rest+> run (rest :\^^ str) = putStr str >> rest+> run ((:%) rest format tokens) = ttFormat format tokens >> rest+>+> ttFormat :: String -> [String] -> IO ()+> ttFormat [] _ = return ()+> ttFormat ('\\':'%':cs) tokens = putChar '%' >> ttFormat cs tokens+> ttFormat ('%':cs) (t:tokens) = putStr t >> ttFormat cs tokens+> ttFormat (c:cs) tokens = putChar c >> ttFormat cs tokens++Now, we can write some helper functions:++> readLine :: TeletypeM String+> readLine = unfoldM $ mfilter (/= '\n') <$> readOrEOF++And use them to interact with the user:++> hello :: TeletypeM ()+> hello = do+> (\^^) "Hello! What's your name?"; nL+> name <- readLine+> "Nice to meet you, %." % [name]; nL+> halt++We can transform any @TeletypeM@ into an @IO@ action, and run it:++> main :: IO ()+> main = runTeletypeIO hello++@+ Hello! What's your name?+ $ Dave+ Nice to meet you, Dave.+ This conversation can serve no purpose anymore. Goodbye.+@++When specifying DSLs in this way, we only need to define the semantics+for each of the actions; the plumbing of values is taken care of by+the generated monad instance.++-}+-- END Teletype.lhs
src/Control/Monad/Trans/Free.hs view
@@ -8,6 +8,10 @@ #if __GLASGOW_HASKELL__ >= 707 {-# LANGUAGE DeriveDataTypeable #-} #endif++#ifndef MIN_VERSION_mtl+#define MIN_VERSION_mtl(x,y,z) 1+#endif ----------------------------------------------------------------------------- -- | -- Module : Control.Monad.Trans.Free@@ -32,6 +36,7 @@ -- * Operations , liftF , iterT+ , iterTM , hoistFreeT , transFreeT -- * Operations of free monad@@ -43,14 +48,16 @@ ) where import Control.Applicative-import Control.Monad (liftM, MonadPlus(..), ap)+import Control.Monad (liftM, MonadPlus(..), ap, join) import Control.Monad.Trans.Class import Control.Monad.Free.Class import Control.Monad.IO.Class import Control.Monad.Reader.Class+import Control.Monad.Writer.Class import Control.Monad.State.Class import Control.Monad.Error.Class import Control.Monad.Cont.Class+import Data.Functor.Bind hiding (join) import Data.Monoid import Data.Foldable import Data.Functor.Identity@@ -111,10 +118,12 @@ -- | The \"free monad\" for a functor @f@. type Free f = FreeT f Identity +-- | Evaluates the first layer out of a free monad value. runFree :: Free f a -> FreeF f a (Free f a) runFree = runIdentity . runFreeT {-# INLINE runFree #-} +-- | Pushes a layer into a free monad value. free :: FreeF f a (Free f a) -> Free f a free = FreeT . Identity {-# INLINE free #-}@@ -141,6 +150,12 @@ (<*>) = ap {-# INLINE (<*>) #-} +instance (Functor f, Monad m) => Apply (FreeT f m) where+ (<.>) = (<*>)++instance (Functor f, Monad m) => Bind (FreeT f m) where+ (>>-) = (>>=)+ instance (Functor f, Monad m) => Monad (FreeT f m) where return a = FreeT (return (Pure a)) {-# INLINE return #-}@@ -162,6 +177,24 @@ local f = hoistFreeT (local f) {-# INLINE local #-} +instance (Functor f, MonadWriter w m) => MonadWriter w (FreeT f m) where+ tell = lift . tell+ {-# INLINE tell #-}+ listen (FreeT m) = FreeT $ liftM concat' $ listen (fmap listen `liftM` m)+ where+ concat' (Pure x, w) = Pure (x, w)+ concat' (Free y, w) = Free $ fmap (second (w <>)) <$> y+ pass m = FreeT . pass' . runFreeT . hoistFreeT clean $ listen m+ where+ clean = pass . liftM (\x -> (x, const mempty))+ pass' = join . liftM g+ g (Pure ((x, f), w)) = tell (f w) >> return (Pure x)+ g (Free f) = return . Free . fmap (FreeT . pass' . runFreeT) $ f+#if MIN_VERSION_mtl(2,1,1)+ writer w = lift (writer w)+ {-# INLINE writer #-}+#endif+ instance (Functor f, MonadState s m) => MonadState s (FreeT f m) where get = lift get {-# INLINE get #-}@@ -175,7 +208,7 @@ instance (Functor f, MonadError e m) => MonadError e (FreeT f m) where throwError = lift . throwError {-# INLINE throwError #-}- FreeT m `catchError` f = FreeT $ (liftM (fmap (`catchError` f)) m) `catchError` (runFreeT . f)+ FreeT m `catchError` f = FreeT $ liftM (fmap (`catchError` f)) m `catchError` (runFreeT . f) instance (Functor f, MonadCont m) => MonadCont (FreeT f m) where callCC f = FreeT $ callCC (\k -> runFreeT $ f (lift . k . Pure))@@ -200,6 +233,14 @@ iterT f (FreeT m) = do val <- m case fmap (iterT f) val of+ Pure x -> return x+ Free y -> f y++-- | Tear down a free monad transformer using iteration over a transformer.+iterTM :: (Functor f, Monad m, MonadTrans t, Monad (t m)) => (f (t m a) -> t m a) -> FreeT f m a -> t m a+iterTM f (FreeT m) = do+ val <- lift m+ case fmap (iterTM f) val of Pure x -> return x Free y -> f y
src/Control/Monad/Trans/Free/Church.hs view
@@ -1,7 +1,26 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE UndecidableInstances #-}++#ifndef MIN_VERSION_mtl+#define MIN_VERSION_mtl(x,y,z) 1+#endif++-----------------------------------------------------------------------------+-- |+-- Module : Control.Monad.Trans.Free.Church+-- Copyright : (C) 2008-2014 Edward Kmett+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Edward Kmett <ekmett@gmail.com>+-- Stability : provisional+-- Portability : non-portable (rank-2 polymorphism, MTPCs)+-- +-- Church-encoded free monad transformer.+--+----------------------------------------------------------------------------- module Control.Monad.Trans.Free.Church ( -- * The free monad transformer@@ -11,6 +30,7 @@ -- * Operations , toFT, fromFT , iterT+ , iterTM , hoistFT , transFT -- * Operations of free monad@@ -29,6 +49,7 @@ import Control.Monad.Trans.Class import Control.Monad.IO.Class import Control.Monad.Reader.Class+import Control.Monad.Writer.Class import Control.Monad.State.Class import Control.Monad.Error.Class import Control.Monad.Cont.Class@@ -109,6 +130,16 @@ local f = hoistFT (local f) {-# INLINE local #-} +instance (Functor f, MonadWriter w m) => MonadWriter w (FT f m) where+ tell = lift . tell+ {-# INLINE tell #-}+ listen = toFT . listen . fromFT+ pass = toFT . pass . fromFT+#if MIN_VERSION_mtl(2,1,1)+ writer w = lift (writer w)+ {-# INLINE writer #-}+#endif+ instance (Functor f, MonadState s m) => MonadState s (FT f m) where get = lift get {-# INLINE get #-}@@ -135,9 +166,11 @@ -- | The \"free monad\" for a functor @f@. type F f = FT f Identity +-- | Unwrap the 'Free' monad to obtain it's Church-encoded representation. runF :: Functor f => F f a -> (forall r. (a -> r) -> (f r -> r) -> r) runF (FT m) = \kp kf -> runIdentity $ m (return . kp) (return . kf . fmap runIdentity) +-- | Wrap a Church-encoding of a \"free monad\" as the free monad for a functor. free :: Functor f => (forall r. (a -> r) -> (f r -> r) -> r) -> F f a free f = FT (\kp kf -> return $ f (runIdentity . kp) (runIdentity . kf . fmap return)) @@ -145,6 +178,10 @@ iterT :: (Functor f, Monad m) => (f (m a) -> m a) -> FT f m a -> m a iterT phi (FT m) = m return phi {-# INLINE iterT #-}++-- | Tear down a free monad transformer using iteration over a transformer.+iterTM :: (Functor f, Monad m, MonadTrans t, Monad (t m)) => (f (t m a) -> t m a) -> FT f m a -> t m a+iterTM f (FT m) = join . lift $ m (return . return) (return . f . fmap (join .lift)) -- | Lift a monad homomorphism from @m@ to @n@ into a monad homomorphism from @'FT' f m@ to @'FT' f n@ --
src/Control/Monad/Trans/Iter.hs view
@@ -3,12 +3,11 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE DeriveDataTypeable #-} -#ifndef MIN_VERSION_MTL-#define MIN_VERSION_MTL(x,y,z) 1+#ifndef MIN_VERSION_mtl+#define MIN_VERSION_mtl(x,y,z) 1 #endif -----------------------------------------------------------------------------@@ -27,37 +26,61 @@ ---------------------------------------------------------------------------- module Control.Monad.Trans.Iter (+ -- |+ -- Functions in Haskell are meant to be pure. For example, if an expression+ -- has type Int, there should exist a value of the type such that the expression+ -- can be replaced by that value in any context without changing the meaning+ -- of the program.+ --+ -- Some computations may perform side effects (@unsafePerformIO@), throw an+ -- exception (using @error@); or not terminate+ -- (@let infinity = 1 + infinity in infinity@).+ --+ -- While the 'IO' monad encapsulates side-effects, and the 'Either'+ -- monad encapsulates errors, the 'Iter' monad encapsulates+ -- non-termination. The 'IterT' transformer generalizes non-termination to any monadic+ -- computation.+ -- * The iterative monad transformer IterT(..) -- * Capretta's iterative monad , Iter, iter, runIter- -- * Operations+ -- * Combinators , delay , hoistIterT+ , liftIter+ , cutoff+ , never+ , interleave, interleave_ -- * Consuming iterative monads , retract , fold , foldM -- * IterT ~ FreeT Identity , MonadFree(..)+ -- * Example+ -- $example ) where import Control.Applicative-import Control.Monad (ap, liftM, MonadPlus(..))+import Control.Monad (ap, liftM, MonadPlus(..), join) import Control.Monad.Fix import Control.Monad.Trans.Class import Control.Monad.Free.Class import Control.Monad.State.Class import Control.Monad.Error.Class import Control.Monad.Reader.Class+import Control.Monad.Writer.Class import Control.Monad.Cont.Class import Control.Monad.IO.Class import Data.Bifunctor import Data.Bitraversable-import Data.Functor.Bind+import Data.Either+import Data.Functor.Bind hiding (join) import Data.Functor.Identity import Data.Foldable hiding (fold)-import Data.Traversable+import Data.Traversable hiding (mapM)+import Data.Monoid import Data.Semigroup.Foldable import Data.Semigroup.Traversable import Data.Typeable@@ -76,12 +99,19 @@ deriving (Typeable) #endif +-- | Plain iterative computations. type Iter = IterT Identity +-- | Builds an iterative computation from one first step.+--+-- prop> runIter . iter == id iter :: Either a (Iter a) -> Iter a iter = IterT . Identity {-# INLINE iter #-} +-- | Executes the first step of an iterative computation+--+-- prop> iter . runIter == id runIter :: Iter a -> Either a (Iter a) runIter = runIdentity . runIterT {-# INLINE runIter #-}@@ -164,13 +194,31 @@ go (Right a) = Right <$> traverse1 f a {-# INLINE traverse1 #-} -instance (Functor m, MonadReader e m) => MonadReader e (IterT m) where+instance MonadReader e m => MonadReader e (IterT m) where ask = lift ask {-# INLINE ask #-} local f = hoistIterT (local f) {-# INLINE local #-} -instance (Functor m, MonadState s m) => MonadState s (IterT m) where+instance MonadWriter w m => MonadWriter w (IterT m) where+ tell = lift . tell+ {-# INLINE tell #-}+ listen (IterT m) = IterT $ liftM concat' $ listen (fmap listen `liftM` m)+ where+ concat' (Left x, w) = Left (x, w)+ concat' (Right y, w) = Right $ second (w <>) <$> y+ pass m = IterT . pass' . runIterT . hoistIterT clean $ listen m+ where+ clean = pass . liftM (\x -> (x, const mempty))+ pass' = join . liftM g+ g (Left ((x, f), w)) = tell (f w) >> return (Left x)+ g (Right f) = return . Right . IterT . pass' . runIterT $ f+#if MIN_VERSION_mtl(2,1,1)+ writer w = lift (writer w)+ {-# INLINE writer #-}+#endif++instance MonadState s m => MonadState s (IterT m) where get = lift get {-# INLINE get #-} put s = lift (put s)@@ -180,21 +228,28 @@ {-# INLINE state #-} #endif -instance (Functor m, MonadError e m) => MonadError e (IterT m) where+instance MonadError e m => MonadError e (IterT m) where throwError = lift . throwError {-# INLINE throwError #-}- IterT m `catchError` f = IterT $ (liftM (fmap (`catchError` f)) m) `catchError` (runIterT . f)+ IterT m `catchError` f = IterT $ liftM (fmap (`catchError` f)) m `catchError` (runIterT . f) -instance (Functor m, MonadIO m) => MonadIO (IterT m) where+instance MonadIO m => MonadIO (IterT m) where liftIO = lift . liftIO -instance (MonadCont m) => MonadCont (IterT m) where+instance MonadCont m => MonadCont (IterT m) where callCC f = IterT $ callCC (\k -> runIterT $ f (lift . k . Left)) instance Monad m => MonadFree Identity (IterT m) where wrap = IterT . return . Right . runIdentity {-# INLINE wrap #-} +-- | Adds an extra layer to a free monad value.+--+-- In particular, for the iterative monad 'Iter', this makes the+-- computation require one more step, without changing its final+-- result.+--+-- prop> runIter (delay ma) == Right ma delay :: (Monad f, MonadFree f m) => m a -> m a delay = wrap . return {-# INLINE delay #-}@@ -220,7 +275,94 @@ hoistIterT :: Monad n => (forall a. m a -> n a) -> IterT m b -> IterT n b hoistIterT f (IterT as) = IterT (fmap (hoistIterT f) `liftM` f as) -#if defined(GHC_TYPEABLE) && __GLASGOW_HASKELL__ < 707+-- | Lifts a plain, non-terminating computation into a richer environment.+-- 'liftIter' is a 'Monad' homomorphism.+liftIter :: (Monad m) => Iter a -> IterT m a+liftIter = hoistIterT (return . runIdentity)++-- | A computation that never terminates+never :: (Monad f, MonadFree f m) => m a+never = delay never++-- | Cuts off an iterative computation after a given number of+-- steps. If the number of steps is 0 or less, no computation nor+-- monadic effects will take place.+--+-- The step where the final value is produced also counts towards the limit.+--+-- Some examples (n ≥ 0):+--+-- prop> cutoff 0 _ == return Nothing+-- prop> cutoff (n+1) . return == return . Just+-- prop> cutoff (n+1) . lift == lift . liftM Just+-- prop> cutoff (n+1) . delay == delay . cutoff n+-- prop> cutoff n never == iterate delay (return Nothing) !! n+--+-- Calling 'retract . cutoff n' is always terminating, provided each of the+-- steps in the iteration is terminating.+cutoff :: (Monad m) => Integer -> IterT m a -> IterT m (Maybe a)+cutoff n | n <= 0 = const $ return Nothing+cutoff n = IterT . liftM (either (Left . Just)+ (Right . cutoff (n - 1))) . runIterT++-- | Interleaves the steps of a finite list of iterative computations, and+-- collects their results.+--+-- The resulting computation has as many steps as the longest computation+-- in the list.+interleave :: Monad m => [IterT m a] -> IterT m [a]+interleave ms = IterT $ do+ xs <- mapM runIterT ms+ if null (rights xs)+ then return . Left $ lefts xs+ else return . Right . interleave $ map (either return id) xs+{-# INLINE interleave #-}++-- | Interleaves the steps of a finite list of computations, and discards their+-- results.+--+-- The resulting computation has as many steps as the longest computation+-- in the list.+--+-- Equivalent to @void . interleave@.+interleave_ :: (Monad m) => [IterT m a] -> IterT m ()+interleave_ [] = return ()+interleave_ xs = IterT $ liftM (Right . interleave_ . rights) $ mapM runIterT xs+{-# INLINE interleave_ #-}++instance (Monad m, Monoid a) => Monoid (IterT m a) where+ mempty = return mempty+ x `mappend` y = IterT $ do+ x' <- runIterT x+ y' <- runIterT y+ case (x', y') of+ ( Left a, Left b) -> return . Left $ a `mappend` b+ ( Left a, Right b) -> return . Right $ liftM (a `mappend`) b+ (Right a, Left b) -> return . Right $ liftM (`mappend` b) a+ (Right a, Right b) -> return . Right $ a `mappend` b++ mconcat = mconcat' . map Right+ where+ mconcat' :: (Monad m, Monoid a) => [Either a (IterT m a)] -> IterT m a+ mconcat' ms = IterT $ do+ xs <- mapM (either (return . Left) runIterT) ms+ case compact xs of+ [l@(Left _)] -> return l+ xs' -> return . Right $ mconcat' xs'+ {-# INLINE mconcat' #-}++ compact :: (Monoid a) => [Either a b] -> [Either a b]+ compact [] = []+ compact (r@(Right _):xs) = r:(compact xs)+ compact ( Left a :xs) = compact' a xs++ compact' a [] = [Left a]+ compact' a (r@(Right _):xs) = (Left a):(r:(compact xs))+ compact' a ( (Left a'):xs) = compact' (a <> a') xs++#if defined(GHC_TYPEABLE)++#if __GLASGOW_HASKELL__ < 707 instance Typeable1 m => Typeable1 (IterT m) where typeOf1 t = mkTyConApp freeTyCon [typeOf1 (f t)] where f :: IterT m a -> m a@@ -234,6 +376,12 @@ #endif {-# NOINLINE freeTyCon #-} +#else++#define Typeable1 Typeable++#endif+ instance ( Typeable1 m, Typeable a , Data (m (Either a (IterT m a)))@@ -256,3 +404,150 @@ {-# NOINLINE iterDataType #-} #endif++-- BEGIN MandelbrotIter.lhs+{- $example+This is literate Haskell! To run the example, open the source and copy+this comment block into a new file with '.lhs' extension. Compiling to an executable+file with the @-O2@ optimization level is recomended.++For example: @ghc -o 'mandelbrot_iter' -O2 MandelbrotIter.lhs ; ./mandelbrot_iter@++@ \{\-\# LANGUAGE PackageImports \#\-\} @++> {-# LANGUAGE PackageImports #-}++> import Control.Arrow+> import Control.Monad.Trans.Iter+> import "mtl" Control.Monad.Reader+> import "mtl" Control.Monad.List+> import "mtl" Control.Monad.Identity+> import Control.Monad.IO.Class+> import Data.Complex+> import Graphics.HGL (runGraphics, Window, withPen,+> line, RGB (RGB), RedrawMode (Unbuffered, DoubleBuffered), openWindowEx,+> drawInWindow, mkPen, Style (Solid))++Some fractals can be defined by infinite sequences of complex numbers. For example,+to render the <https://en.wikipedia.org/wiki/Mandelbrot_set Mandelbrot set>,+the following sequence is generated for each point @c@ in the complex plane:++@+z₀ = c ++z₁ = z₀² + c ++z₂ = z₁² + c ++…+@++If, after some iterations, |z_i| ≥ 2, the point is not in the set. We+can compute if a point is not in the Mandelbrot set this way:++@+ escaped :: Complex Double -> Int+ escaped c = loop 0 0 where+ loop z n = if (magnitude z) >= 2 then n+ else loop (z*z + c) (n+1)+@++If @c@ is not in the Mandelbrot set, we get the number of iterations required to+prove that fact. But, if @c@ is in the mandelbrot set, 'escaped' will+run forever.++We can use the 'Iter' monad to delimit this effect. By applying+'delay' before the recursive call, we decompose the computation into+terminating steps.++> escaped :: Complex Double -> Iter Int+> escaped c = loop 0 0 where+> loop z n = if (magnitude z) >= 2 then return n+> else delay $ loop (z*z + c) (n+1)+>++If we draw each point on a canvas after it escapes, we can get a _negative_+image of the Mandelbrot set. Drawing pixels is a side-effect, so it+should happen inside the IO monad. Also, we want to have an+environment to store the size of the canvas, and the target window.++By using 'IterT', we can add all these behaviours to our non-terminating+computation.++> data Canvas = Canvas { width :: Int, height :: Int, window :: Window }+>+> type FractalM a = IterT (ReaderT Canvas IO) a++Any simple, non-terminating computation can be lifted into a richer environment.++> escaped' :: Complex Double -> IterT (ReaderT Canvas IO) Int+> escaped' = liftIter . escaped++Then, to draw a point, we can just retrieve the number of iterations until it+finishes, and draw it. The color will depend on the number of iterations.++> mandelbrotPoint :: (Int, Int) -> FractalM ()+> mandelbrotPoint p = do+> c <- scale p+> n <- escaped' c+> let color = if (even n) then RGB 0 0 255 -- Blue+> else RGB 0 0 127 -- Darker blue+> drawPoint color p++The pixels on the screen don't match the region in the complex plane where the+fractal is; we need to map them first. The region we are interested in is+Im z = [-1,1], Re z = [-2,1].++> scale :: (Int, Int) -> FractalM (Complex Double)+> scale (xi,yi) = do+> (w,h) <- asks $ (fromIntegral . width) &&& (fromIntegral . height)+> let (x,y) = (fromIntegral xi, fromIntegral yi)+> let im = (-y + h / 2 ) / (h/2)+> let re = ( x - w * 2 / 3 ) / (h/2)+> return $ re :+ im++Drawing a point is equivalent to drawing a line of length one.++> drawPoint :: RGB -> (Int,Int) -> FractalM ()+> drawPoint color p@(x,y) = do+> w <- asks window+> let point = line (x,y) (x+1, y+1)+> liftIO $ drawInWindow w $ mkPen Solid 1 color (flip withPen point)++We may want to draw more than one point. However, if we just sequence the computations+monadically, the first point that is not a member of the set will block the whole+process. We need advance all the points at the same pace, by interleaving the+computations.++> drawMandelbrot :: FractalM ()+> drawMandelbrot = do+> (w,h) <- asks $ width &&& height+> let ps = [mandelbrotPoint (x,y) | x <- [0 .. (w-1)], y <- [0 .. (h-1)]]+> interleave_ ps++To run this computation, we can just use @retract@, which will run indefinitely:++> runFractalM :: Canvas -> FractalM a -> IO a+> runFractalM canvas = flip runReaderT canvas . retract++Or, we can trade non-termination for getting an incomplete result,+by cutting off after a certain number of steps.++> runFractalM' :: Integer -> Canvas -> FractalM a -> IO (Maybe a)+> runFractalM' n canvas = flip runReaderT canvas . retract . cutoff n++Thanks to the 'IterT' transformer, we can separate timeout concerns from+computational concerns.++> main :: IO ()+> main = do+> let windowWidth = 800+> let windowHeight = 480+> runGraphics $ do+> w <- openWindowEx "Mandelbrot" Nothing (windowWidth, windowHeight) DoubleBuffered (Just 1)+> let canvas = Canvas windowWidth windowHeight w+> runFractalM' 100 canvas drawMandelbrot+> putStrLn $ "Fin"++-}+-- END MandelbrotIter.lhs
− src/Control/MonadPlus/Free.hs
@@ -1,305 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE Rank2Types #-}-#if __GLASGOW_HASKELL__ >= 707-{-# LANGUAGE DeriveDataTypeable #-}-#endif--------------------------------------------------------------------------------- |--- Module : Control.MonadPlus.Free--- Copyright : (C) 2008-2012 Edward Kmett--- License : BSD-style (see the file LICENSE)------ Maintainer : Edward Kmett <ekmett@gmail.com>--- Stability : provisional--- Portability : MPTCs, fundeps------ left-distributive MonadPlus for free.------------------------------------------------------------------------------module Control.MonadPlus.Free- ( MonadFree(..)- , Free(..)- , retract- , liftF- , iter- , iterM- , hoistFree- ) where--import Control.Applicative-import Control.Monad (liftM, MonadPlus(..))-import Control.Monad.Trans.Class-import Control.Monad.Free.Class-import Control.Monad.Reader.Class-import Control.Monad.Writer.Class-import Control.Monad.State.Class-import Control.Monad.Error.Class-import Control.Monad.Cont.Class-import Data.Functor.Bind-import Data.Foldable-import Data.Traversable-import Data.Semigroup--#ifdef GHC_TYPEABLE-import Data.Data-#endif---- | The 'Free' 'MonadPlus' for a 'Functor' @f@.------ /Formally/------ A 'MonadPlus' @n@ is a free 'MonadPlus' for @f@ if every monadplus homomorphism--- from @n@ to another MonadPlus @m@ is equivalent to a natural transformation--- from @f@ to @m@.------ We model this internally as if left-distribution holds.------ <<http://www.haskell.org/haskellwiki/MonadPlus>>-data Free f a- = Pure a- | Free (f (Free f a))- | Plus [Free f a]-#if __GLASGOW_HASKELL__ >= 707- deriving (Typeable)-#endif--instance (Eq (f (Free f a)), Eq a) => Eq (Free f a) where- Pure a == Pure b = a == b- Free fa == Free fb = fa == fb- Plus as == Plus bs = as == bs- _ == _ = False--instance (Ord (f (Free f a)), Ord a) => Ord (Free f a) where- Pure a `compare` Pure b = a `compare` b- Pure _ `compare` Free _ = LT- Pure _ `compare` Plus _ = LT- Free _ `compare` Pure _ = GT- Free fa `compare` Free fb = fa `compare` fb- Free _ `compare` Plus _ = LT- Plus _ `compare` Pure _ = GT- Plus _ `compare` Free _ = GT- Plus as `compare` Plus bs = as `compare` bs--instance (Show (f (Free f a)), Show a) => Show (Free f a) where- showsPrec d (Pure a) = showParen (d > 10) $- showString "Pure " . showsPrec 11 a- showsPrec d (Free m) = showParen (d > 10) $- showString "Free " . showsPrec 11 m- showsPrec d (Plus as) = showParen (d > 10) $- showString "Plus " . showsPrec 11 as--instance (Read (f (Free f a)), Read a) => Read (Free f a) where- readsPrec d r = readParen (d > 10)- (\r' -> [ (Pure m, t)- | ("Pure", s) <- lex r'- , (m, t) <- readsPrec 11 s]) r- ++ readParen (d > 10)- (\r' -> [ (Free m, t)- | ("Free", s) <- lex r'- , (m, t) <- readsPrec 11 s]) r- ++ readParen (d > 10)- (\r' -> [ (Plus as, t)- | ("Plus", s) <- lex r'- , (as, t) <- readsPrec 11 s]) r--instance Functor f => Functor (Free f) where- fmap f = go where- go (Pure a) = Pure (f a)- go (Free fa) = Free (go <$> fa)- go (Plus as) = Plus (map go as)- {-# INLINE fmap #-}--instance Functor f => Apply (Free f) where- Pure f <.> Pure b = Pure (f b)- Pure f <.> Plus bs = Plus $ fmap f <$> bs- Pure f <.> Free fb = Free $ fmap f <$> fb- Free ff <.> b = Free $ (<.> b) <$> ff- Plus fs <.> b = Plus $ (<.> b) <$> fs -- left distribution ???--instance Functor f => Applicative (Free f) where- pure = Pure- {-# INLINE pure #-}- Pure f <*> Pure b = Pure (f b)- Pure f <*> Free mb = Free $ fmap f <$> mb- Pure f <*> Plus bs = Plus $ fmap f <$> bs- Free ff <*> b = Free $ (<*> b) <$> ff- Plus fs <*> b = Plus $ (<*> b) <$> fs -- left distribution--instance Functor f => Bind (Free f) where- Pure a >>- f = f a- Free m >>- f = Free ((>>- f) <$> m)- Plus m >>- f = Plus ((>>- f) <$> m)--instance Functor f => Monad (Free f) where- return = Pure- {-# INLINE return #-}- Pure a >>= f = f a- Free m >>= f = Free ((>>= f) <$> m)- Plus m >>= f = Plus (map (>>= f) m) -- left distribution law--instance Functor f => Alternative (Free f) where- empty = Plus []- {-# INLINE empty #-}- Plus [] <|> r = r- l <|> Plus [] = l- Plus as <|> Plus bs = Plus (as ++ bs)- a <|> b = Plus [a, b]- {-# INLINE (<|>) #-}--instance Functor f => MonadPlus (Free f) where- mzero = empty- {-# INLINE mzero #-}- mplus = (<|>)- {-# INLINE mplus #-}--instance Functor f => Semigroup (Free f a) where- (<>) = (<|>)- {-# INLINE (<>) #-}--instance Functor f => Monoid (Free f a) where- mempty = empty- {-# INLINE mempty #-}- mappend = (<|>)- {-# INLINE mappend #-}- mconcat as = from (as >>= to)- where- to (Plus xs) = xs- to x = [x]- from [x] = x- from xs = Plus xs- {-# INLINE mconcat #-}---- | This is not a true monad transformer. It is only a monad transformer \"up to 'retract'\".-instance MonadTrans Free where- lift = Free . liftM Pure- {-# INLINE lift #-}--instance Foldable f => Foldable (Free f) where- foldMap f = go where- go (Pure a) = f a- go (Free fa) = foldMap go fa- go (Plus as) = foldMap go as- {-# INLINE foldMap #-}--instance Traversable f => Traversable (Free f) where- traverse f = go where- go (Pure a) = Pure <$> f a- go (Free fa) = Free <$> traverse go fa- go (Plus as) = Plus <$> traverse go as- {-# INLINE traverse #-}--instance (Functor m, MonadPlus m, MonadWriter e m) => MonadWriter e (Free m) where- tell = lift . tell- {-# INLINE tell #-}- listen = lift . listen . retract- {-# INLINE listen #-}- pass = lift . pass . retract- {-# INLINE pass #-}--instance (Functor m, MonadPlus m, MonadReader e m) => MonadReader e (Free m) where- ask = lift ask- {-# INLINE ask #-}- local f = lift . local f . retract- {-# INLINE local #-}--instance (Functor m, MonadState s m) => MonadState s (Free m) where- get = lift get- {-# INLINE get #-}- put s = lift (put s)- {-# INLINE put #-}--instance (Functor m, MonadPlus m, MonadError e m) => MonadError e (Free m) where- throwError = lift . throwError- {-# INLINE throwError #-}- catchError as f = lift (catchError (retract as) (retract . f))- {-# INLINE catchError #-}--instance (Functor m, MonadPlus m, MonadCont m) => MonadCont (Free m) where- callCC f = lift (callCC (retract . f . liftM lift))- {-# INLINE callCC #-}--instance Functor f => MonadFree f (Free f) where- wrap = Free- {-# INLINE wrap #-}---- |--- 'retract' is the left inverse of 'lift' and 'liftF'------ @--- 'retract' . 'lift' = 'id'--- 'retract' . 'liftF' = 'id'--- @-retract :: MonadPlus f => Free f a -> f a-retract (Pure a) = return a-retract (Free as) = as >>= retract-retract (Plus as) = Prelude.foldr (mplus . retract) mzero as---- | Tear down a 'Free' 'Monad' using iteration.-iter :: Functor f => (f a -> a) -> ([a] -> a) -> Free f a -> a-iter phi psi = go where- go (Pure a) = a- go (Free as) = phi (go <$> as)- go (Plus as) = psi (go <$> as)-{-# INLINE iter #-}---- | Like iter for monadic values.-iterM :: (Monad m, Functor f) => (f (m a) -> m a) -> ([m a] -> m a) -> Free f a -> m a-iterM phi psi = go where- go (Pure a) = return a- go (Free as) = phi (go <$> as)- go (Plus as) = psi (go <$> as)---- | Lift a natural transformation from @f@ to @g@ into a natural transformation from @'FreeT' f@ to @'FreeT' g@.-hoistFree :: Functor g => (forall a. f a -> g a) -> Free f b -> Free g b-hoistFree f = go where- go (Pure a) = Pure a- go (Free as) = Free (go <$> f as)- go (Plus as) = Plus (map go as)--#if defined(GHC_TYPEABLE) && __GLASGOW_HASKELL__ < 707-instance Typeable1 f => Typeable1 (Free f) where- typeOf1 t = mkTyConApp freeTyCon [typeOf1 (f t)] where- f :: Free f a -> f a- f = undefined--freeTyCon :: TyCon-#if __GLASGOW_HASKELL__ < 704-freeTyCon = mkTyCon "Control.MonadPlus.Free.Free"-#else-freeTyCon = mkTyCon3 "free" "Control.MonadPlus.Free" "Free"-#endif-{-# NOINLINE freeTyCon #-}--instance- ( Typeable1 f, Typeable a- , Data a, Data (f (Free f a))- ) => Data (Free f a) where- gfoldl f z (Pure a) = z Pure `f` a- gfoldl f z (Free as) = z Free `f` as- gfoldl f z (Plus as) = z Plus `f` as- toConstr Pure{} = pureConstr- toConstr Free{} = freeConstr- toConstr Plus{} = plusConstr- gunfold k z c = case constrIndex c of- 1 -> k (z Pure)- 2 -> k (z Free)- 3 -> k (z Plus)- _ -> error "gunfold"- dataTypeOf _ = freeDataType- dataCast1 f = gcast1 f--pureConstr, freeConstr, plusConstr :: Constr-pureConstr = mkConstr freeDataType "Pure" [] Prefix-freeConstr = mkConstr freeDataType "Free" [] Prefix-plusConstr = mkConstr freeDataType "Plus" [] Prefix-{-# NOINLINE pureConstr #-}-{-# NOINLINE freeConstr #-}--freeDataType :: DataType-freeDataType = mkDataType "Control.MonadPlus.Free.Free" [pureConstr, freeConstr, plusConstr]-{-# NOINLINE freeDataType #-}--#endif