Ticket #10665: Fixedpoint.hs

File Fixedpoint.hs, 10.4 KB (added by slyfox, 2 years ago)

taken as-is from unification-fd-0.10.0.1/src/Data/Functor/Fixedpoint.hs

Line 
1-- For the Show (Fix f) instance
2{-# LANGUAGE UndecidableInstances #-}
3-- For 'build' and 'hmap'
4{-# LANGUAGE Rank2Types #-}
5
6-- Unfortunately GHC < 6.10 needs -fglasgow-exts in order to actually
7-- parse RULES (see -ddump-rules); the -frewrite-rules flag only
8-- enables the application of rules, instead of doing what we want.
9-- Apparently this is fixed in 6.10. In newer GHC (e.g., 7.6.1) the
10-- -frewrite-rules flag is deprecated in favor of -fenable-rewrite-rules.
11-- It's unclear whether we can use CPP to switch between -fglasgow-exts
12-- -frewrite-rules and -fenable-rewrite-rules based on the GHC
13-- version...
14--
15-- http://hackage.haskell.org/trac/ghc/ticket/2213
16-- http://www.mail-archive.com/glasgow-haskell-users@haskell.org/msg14313.html
17{-# OPTIONS_GHC -O2 -fenable-rewrite-rules #-}
18
19-- NOTE #1: on GHC >= 7.8 we need to eta expand rules to avoid a
20-- warning about the fact that the rule may never fire because (.)
21-- might inline first...
22
23{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
24----------------------------------------------------------------
25--                                                    2014.05.28
26-- |
27-- Module      :  Data.Functor.Fixedpoint
28-- Copyright   :  Copyright (c) 2007--2015 wren gayle romano
29-- License     :  BSD
30-- Maintainer  :  wren@community.haskell.org
31-- Stability   :  provisional
32-- Portability :  semi-portable (Rank2Types)
33--
34-- This module provides a fixed point operator on functor types.
35-- For Haskell the least and greatest fixed points coincide, so we
36-- needn't distinguish them. This abstract nonsense is helpful in
37-- conjunction with other category theoretic tricks like Swierstra's
38-- functor coproducts (not provided by this package). For more on
39-- the utility of two-level recursive types, see:
40--
41--     * Tim Sheard (2001) /Generic Unification via Two-Level Types/
42--         /and Paramterized Modules/, Functional Pearl, ICFP.
43--
44--     * Tim Sheard & Emir Pasalic (2004) /Two-Level Types and/
45--         /Parameterized Modules/. JFP 14(5): 547--587. This is
46--         an expanded version of Sheard (2001) with new examples.
47--
48--     * Wouter Swierstra (2008) /Data types a la carte/, Functional
49--         Pearl. JFP 18: 423--436.
50----------------------------------------------------------------
51
52module Data.Functor.Fixedpoint
53    (
54    -- * Fixed point operator for functors
55      Fix(..)
56    -- * Maps
57    , hmap,  hmapM
58    , ymap,  ymapM
59    -- * Builders
60    , build
61    -- * Catamorphisms
62    , cata,  cataM
63    , ycata, ycataM
64    -- * Anamorphisms
65    , ana,   anaM
66    -- * Hylomorphisms
67    , hylo,  hyloM
68    ) where
69
70import Prelude          hiding (mapM, sequence)
71import Control.Monad    hiding (mapM, sequence)
72import Data.Traversable
73
74----------------------------------------------------------------
75----------------------------------------------------------------
76
77-- | @Fix f@ is a fix point of the 'Functor' @f@. Note that in
78-- Haskell the least and greatest fixed points coincide, so we don't
79-- need to distinguish between @Mu f@ and @Nu f@. This type used
80-- to be called @Y@, hence the naming convention for all the @yfoo@
81-- functions.
82--
83-- This type lets us invoke category theory to get recursive types
84-- and operations over them without the type checker complaining
85-- about infinite types. The 'Show' instance doesn't print the
86-- constructors, for legibility.
87newtype Fix f = Fix { unFix :: f (Fix f) }
88
89-- This requires UndecidableInstances because the context is larger
90-- than the head and so GHC can't guarantee that the instance safely
91-- terminates. It is in fact safe, however.
92instance (Show (f (Fix f))) => Show (Fix f) where
93    showsPrec p (Fix f) = showsPrec p f
94
95instance (Eq (f (Fix f))) => Eq (Fix f) where
96    Fix x == Fix y  =  x == y
97    Fix x /= Fix y  =  x /= y
98
99instance (Ord (f (Fix f))) => Ord (Fix f) where
100    Fix x `compare` Fix y  =  x `compare` y
101    Fix x >  Fix y         =  x >  y
102    Fix x >= Fix y         =  x >= y
103    Fix x <= Fix y         =  x <= y
104    Fix x <  Fix y         =  x <  y
105    Fix x `max` Fix y      =  Fix (max x y)
106    Fix x `min` Fix y      =  Fix (min x y)
107
108----------------------------------------------------------------
109
110-- | A higher-order map taking a natural transformation @(f -> g)@
111-- and lifting it to operate on @Fix@.
112hmap :: (Functor f, Functor g) => (forall a. f a -> g a) -> Fix f -> Fix g
113{-# INLINE [0] hmap #-}
114hmap eps = ana (eps . unFix)
115    -- == cata (Fix . eps) -- But the anamorphism is a better producer.
116
117{-# RULES
118"hmap id"
119        hmap id = id
120
121-- cf., NOTE #1
122"hmap-compose"
123    forall (eps :: forall a. g a -> h a) (eta :: forall a. f a -> g a) x.
124        hmap eps (hmap eta x) = hmap (eps . eta) x
125    #-}
126
127
128-- | A monadic variant of 'hmap'.
129hmapM
130    :: (Functor f, Traversable g, Monad m)
131    => (forall a. f a -> m (g a)) -> Fix f -> m (Fix g)
132{-# INLINE [0] hmapM #-}
133hmapM eps = anaM (eps . unFix)
134
135{-# RULES
136"hmapM return"
137    hmapM return = return
138
139-- "hmapM-compose"
140--     forall eps eta.
141--         hmap eps <=< hmap eta = hmapM (eps <=< eta)
142    #-}
143
144
145-- | A version of 'fmap' for endomorphisms on the fixed point. That
146-- is, this maps the function over the first layer of recursive
147-- structure.
148ymap :: (Functor f) => (Fix f -> Fix f) -> Fix f -> Fix f
149{-# INLINE [0] ymap #-}
150ymap f = Fix . fmap f . unFix
151
152{-# RULES
153"ymap id"
154        ymap id = id
155
156-- cf., NOTE #1
157"ymap-compose"
158    forall f g x.
159        ymap f (ymap g x) = ymap (f . g) x
160    #-}
161
162
163-- | A monadic variant of 'ymap'.
164ymapM :: (Traversable f, Monad m)
165      => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f)
166{-# INLINE [0] ymapM #-}
167ymapM f = liftM Fix . mapM f . unFix
168
169{-# RULES
170"ymapM id"
171        ymapM return = return
172
173-- "ymapM-compose"
174--     forall f g.
175--         ymapM f <=< ymapM g = ymapM (f <=< g)
176    #-}
177
178
179----------------------------------------------------------------
180-- BUG: this isn't as helful as normal build\/fold fusion as in Data.Functor.Fusable
181--
182-- | Take a Church encoding of a fixed point into the data
183-- representation of the fixed point.
184build :: (Functor f) => (forall r. (f r -> r) -> r) -> Fix f
185{-# INLINE [0] build #-}
186build g = g Fix
187
188-- N.B., the signature is required on @g@ in order to be Rank-2.
189-- The signature is required on @phi@ in order to bring @f@ into
190-- scope. Otherwise we'd need -XScopedTypeVariables.
191{-# RULES
192"build/cata" [1]
193    forall (phi :: f a -> a) (g :: forall r. (f r -> r) -> r).
194        cata phi (build g) = g phi
195    #-}
196
197----------------------------------------------------------------
198-- | A pure catamorphism over the least fixed point of a functor.
199-- This function applies the @f@-algebra from the bottom up over
200-- @Fix f@ to create some residual value.
201cata :: (Functor f) => (f a -> a) -> (Fix f -> a)
202{-# INLINE [0] cata #-}
203cata phi = self
204    where
205    self = phi . fmap self . unFix
206
207{-# RULES
208"cata-refl"
209        cata Fix = id
210
211-- cf., NOTE #1
212"cata-compose"
213    forall (eps :: forall a. f a -> g a) phi x.
214        cata phi (cata (Fix . eps) x) = cata (phi . eps) x
215    #-}
216
217-- We can't really use this one because of the implication constraint
218{- RULES
219"cata-fusion"
220    forall f phi. (f . phi) == (phi . fmap f) ==>
221        f . cata phi = cata phi
222-}
223
224
225-- | A catamorphism for monadic @f@-algebras. Alas, this isn't wholly
226-- generic to @Functor@ since it requires distribution of @f@ over
227-- @m@ (provided by 'sequence' or 'mapM' in 'Traversable').
228--
229-- N.B., this orders the side effects from the bottom up.
230cataM :: (Traversable f, Monad m) => (f a -> m a) -> (Fix f -> m a)
231{-# INLINE [0] cataM #-}
232cataM phiM = self
233    where
234    self = phiM <=< (mapM self . unFix)
235
236-- TODO: other rules for cataM
237{-# RULES
238"cataM-refl"
239        cataM (return . Fix) = return
240    #-}
241
242
243-- TODO: remove this, or add similar versions for ana* and hylo*?
244-- | A variant of 'cata' which restricts the return type to being
245-- a new fixpoint. Though more restrictive, it can be helpful when
246-- you already have an algebra which expects the outermost @Fix@.
247--
248-- If you don't like either @fmap@ or @cata@, then maybe this is
249-- what you were thinking?
250ycata :: (Functor f) => (Fix f -> Fix f) -> Fix f -> Fix f
251{-# INLINE ycata #-}
252ycata f = cata (f . Fix)
253
254
255-- TODO: remove this, or add similar versions for ana* and hylo*?
256-- | Monadic variant of 'ycata'.
257ycataM :: (Traversable f, Monad m)
258       => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f)
259{-# INLINE ycataM #-}
260ycataM f = cataM (f . Fix)
261
262
263----------------------------------------------------------------
264-- | A pure anamorphism generating the greatest fixed point of a
265-- functor. This function applies an @f@-coalgebra from the top
266-- down to expand a seed into a @Fix f@.
267ana :: (Functor f) => (a -> f a) -> (a -> Fix f)
268{-# INLINE [0] ana #-}
269ana psi = self
270    where
271    self = Fix . fmap self . psi
272
273
274{-# RULES
275"ana-refl"
276        ana unFix = id
277
278-- BUG: I think I dualized this right...
279-- cf., NOTE #1
280"ana-compose"
281    forall (eps :: forall a. f a -> g a) psi x.
282        ana (eps . unFix) (ana psi x) = ana (eps . psi) x
283    #-}
284
285-- We can't really use this because of the implication constraint
286{- RULES
287-- BUG: I think I dualized this right...
288"ana-fusion"
289    forall f psi. (psi . f) == (fmap f . psi) ==>
290        ana psi . f = ana psi
291-}
292
293
294-- | An anamorphism for monadic @f@-coalgebras. Alas, this isn't
295-- wholly generic to @Functor@ since it requires distribution of
296-- @f@ over @m@ (provided by 'sequence' or 'mapM' in 'Traversable').
297--
298-- N.B., this orders the side effects from the top down.
299anaM :: (Traversable f, Monad m) => (a -> m (f a)) -> (a -> m (Fix f))
300{-# INLINE anaM #-}
301anaM psiM = self
302    where
303    self = (liftM Fix . mapM self) <=< psiM
304
305
306----------------------------------------------------------------
307-- Is this even worth mentioning? We can amortize the construction
308-- of @Fix f@ (which we'd do anyways because of laziness), but we
309-- can't fuse the @f@ away unless we inline all of @psi@, @fmap@,
310-- and @phi@ at the use sites. Will inlining this definition be
311-- sufficient to do that?
312
313-- | @hylo phi psi == cata phi . ana psi@
314hylo :: (Functor f) => (f b -> b) -> (a -> f a) -> (a -> b)
315{-# INLINE hylo #-}
316hylo phi psi = self
317    where
318    self = phi . fmap self . psi
319
320-- TODO: rules for hylo?
321
322
323-- | @hyloM phiM psiM == cataM phiM <=< anaM psiM@
324hyloM :: (Traversable f, Monad m)
325      => (f b -> m b) -> (a -> m (f a)) -> (a -> m b)
326{-# INLINE hyloM #-}
327hyloM phiM psiM = self
328    where
329    self = phiM <=< mapM self <=< psiM
330
331-- TODO: rules for hyloM?
332
333----------------------------------------------------------------
334----------------------------------------------------------- fin.