diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown --- a/CHANGELOG.markdown +++ b/CHANGELOG.markdown @@ -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. diff --git a/HLint.hs b/HLint.hs new file mode 100644 --- /dev/null +++ b/HLint.hs @@ -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" diff --git a/doc/proof/Control/Comonad/Cofree/instance-Applicative-Cofree.md b/doc/proof/Control/Comonad/Cofree/instance-Applicative-Cofree.md new file mode 100644 --- /dev/null +++ b/doc/proof/Control/Comonad/Cofree/instance-Applicative-Cofree.md @@ -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. diff --git a/doc/proof/Control/Comonad/Cofree/instance-Monad-Cofree.md b/doc/proof/Control/Comonad/Cofree/instance-Monad-Cofree.md new file mode 100644 --- /dev/null +++ b/doc/proof/Control/Comonad/Cofree/instance-Monad-Cofree.md @@ -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. diff --git a/doc/proof/Control/Comonad/Cofree/instance-MonadZip-Cofree.md b/doc/proof/Control/Comonad/Cofree/instance-MonadZip-Cofree.md new file mode 100644 --- /dev/null +++ b/doc/proof/Control/Comonad/Cofree/instance-MonadZip-Cofree.md @@ -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`. diff --git a/doc/proof/Control/Comonad/Trans/Cofree/instance-Applicative-CofreeT.md b/doc/proof/Control/Comonad/Trans/Cofree/instance-Applicative-CofreeT.md new file mode 100644 --- /dev/null +++ b/doc/proof/Control/Comonad/Trans/Cofree/instance-Applicative-CofreeT.md @@ -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 + ≡ 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 + ≡ 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 : 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) + +``` + + diff --git a/doc/proof/Control/Comonad/Trans/Cofree/instance-Monad-CofreeT.md b/doc/proof/Control/Comonad/Trans/Cofree/instance-Monad-CofreeT.md new file mode 100644 --- /dev/null +++ b/doc/proof/Control/Comonad/Trans/Cofree/instance-Monad-CofreeT.md @@ -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). diff --git a/doc/proof/Control/Comonad/Trans/Cofree/instance-MonadTrans-CofreeT.md b/doc/proof/Control/Comonad/Trans/Cofree/instance-MonadTrans-CofreeT.md new file mode 100644 --- /dev/null +++ b/doc/proof/Control/Comonad/Trans/Cofree/instance-MonadTrans-CofreeT.md @@ -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) +``` + + + + diff --git a/doc/proof/Control/Comonad/Trans/Cofree/instance-MonadZip-CofreeT.md b/doc/proof/Control/Comonad/Trans/Cofree/instance-MonadZip-CofreeT.md new file mode 100644 --- /dev/null +++ b/doc/proof/Control/Comonad/Trans/Cofree/instance-MonadZip-CofreeT.md @@ -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) + +. +``` diff --git a/free.cabal b/free.cabal --- a/free.cabal +++ b/free.cabal @@ -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 diff --git a/src/Control/Alternative/Free.hs b/src/Control/Alternative/Free.hs --- a/src/Control/Alternative/Free.hs +++ b/src/Control/Alternative/Free.hs @@ -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 diff --git a/src/Control/Applicative/Free.hs b/src/Control/Applicative/Free.hs --- a/src/Control/Applicative/Free.hs +++ b/src/Control/Applicative/Free.hs @@ -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 , + -- 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 diff --git a/src/Control/Comonad/Cofree.hs b/src/Control/Comonad/Cofree.hs --- a/src/Control/Comonad/Cofree.hs +++ b/src/Control/Comonad/Cofree.hs @@ -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 +-- by Neil Ghani et al., Section 4.3 +-- for more details. +-- +-- In particular, if @f a ≡ [a]@, the +-- resulting data structure is a . +-- For a practical application, check +-- 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 diff --git a/src/Control/Comonad/Trans/Cofree.hs b/src/Control/Comonad/Trans/Cofree.hs --- a/src/Control/Comonad/Trans/Cofree.hs +++ b/src/Control/Comonad/Trans/Cofree.hs @@ -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 diff --git a/src/Control/Comonad/Trans/Coiter.hs b/src/Control/Comonad/Trans/Coiter.hs --- a/src/Control/Comonad/Trans/Coiter.hs +++ b/src/Control/Comonad/Trans/Coiter.hs @@ -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. + + +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 diff --git a/src/Control/Monad/Free.hs b/src/Control/Monad/Free.hs --- a/src/Control/Monad/Free.hs +++ b/src/Control/Monad/Free.hs @@ -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 -- diff --git a/src/Control/Monad/Free/Church.hs b/src/Control/Monad/Free/Church.hs --- a/src/Control/Monad/Free/Church.hs +++ b/src/Control/Monad/Free/Church.hs @@ -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. -- --- --- +-- 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: +-- +-- * +-- +-- * ---------------------------------------------------------------------------- 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'. --- +-- -- 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: --- --- --- --- --- and \"Asymptotic Improvement of Computations over Free Monads\" by Janis Voightländer: --- --- +-- +-- * +-- +-- * +-- +-- and by Janis Voightländer. improve :: Functor f => (forall m. MonadFree f m => m a) -> Free f a improve m = fromF m {-# INLINE improve #-} diff --git a/src/Control/Monad/Free/TH.hs b/src/Control/Monad/Free/TH.hs --- a/src/Control/Monad/Free/TH.hs +++ b/src/Control/Monad/Free/TH.hs @@ -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 diff --git a/src/Control/Monad/Trans/Free.hs b/src/Control/Monad/Trans/Free.hs --- a/src/Control/Monad/Trans/Free.hs +++ b/src/Control/Monad/Trans/Free.hs @@ -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 diff --git a/src/Control/Monad/Trans/Free/Church.hs b/src/Control/Monad/Trans/Free/Church.hs --- a/src/Control/Monad/Trans/Free/Church.hs +++ b/src/Control/Monad/Trans/Free/Church.hs @@ -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 +-- 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@ -- diff --git a/src/Control/Monad/Trans/Iter.hs b/src/Control/Monad/Trans/Iter.hs --- a/src/Control/Monad/Trans/Iter.hs +++ b/src/Control/Monad/Trans/Iter.hs @@ -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 , +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 diff --git a/src/Control/MonadPlus/Free.hs b/src/Control/MonadPlus/Free.hs deleted file mode 100644 --- a/src/Control/MonadPlus/Free.hs +++ /dev/null @@ -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 --- 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. --- --- <> -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