On Fri, Nov 18, 2005 at 11:37:40AM -0500, Paul Hudak wrote: > This is a very late response to an old thread...
ditto :-) > > unwind :: Expr -> Expr > > unwind (Add e1 e2) = Add (unwind e1) (unwind e2) > > unwind (Rec fe) = x where x = unwind (fe x) > > unwind e = e Since this discussion started around observing sharing in the implementation, I wanted to see whether, by the time we convert your cunning representation back into an infinite data structure, we have the sharing we hoped to observe in the first place. > > fe2 e = Add (Const 1) e -- recursive > > e2 = Rec fe2 -- top-level loop > > e2u = unwind e2 -- infinite main = walk e4u where walk (Add e1 e2) = walk e2 blows up, showing that we do not. The problem with unwind seems to be that the computation of the fixed point keeps calling unwind, which keeps reconstructing the fixed point: e2u = unwind e2 = x where x = unwind ((\e -> Add (Const 1) e) x) = Add (Const 1) (unwind x) = Add (Const 1) (Add (Const 1) (unwind (unwind x))) = ... I then tried unwind (Rec fe) = unwind (fix fe) fix f = x where x = f x even though I didn't think it would work: (fix fe) would create a properly sharing structure, but unwind would unshare it: e2u = unwind (x where x = ((\e -> Add (Const 1) e) x)) ( = Add (Const 1) x) = Add (Const 1) (unwind (x where x = Add (Const 1) x)) = Add (Const 1) (Add (Const 1) (unwind (x where x = Add (Const 1) x))) = ... This does blow up in ghci, but not in ghc (6.4.1), even without optimization. I'm not quite sure why, but anyway I want a version that exhibits sharing even in any reasonable implementation. Your message gives the technique (in mapE); we only have to apply it to unwind. But there is a problem--your code has a bug! > > mapE :: (Int->Int) -> Expr -> Expr > > mapE f e = mapE' f e 0 where > > mapE' f (Const i) n = Const (f i) > > mapE' f (Add e1 e2) n = Add (mapE' f e1 n) (mapE' f e2 n) > > mapE' f (Rec fe) n = Rec (absLoop n (mapE' f (fe (Loop n)) (n+1))) > > mapE' f (Loop i) n = Loop i > > > absLoop :: Int -> Expr -> Fix Expr > > absLoop n e = \e' -> > > let abs (Loop n') | n==n' = e' > > abs (Add e1 e2) = Add (abs e1) (abs e2) > > abs e = e > > in abs e > > > e4 = Rec (\e1-> Add (Const 1) > > (Rec (\e2-> Add e1 e2))) -- nested loop > > e7 = mapE succ e4 > > e8 = Rec (\e1-> Add (Const 2) > > (Rec (\e2-> Add e1 e2))) > > b4 = e7==e8 -- returns True! Notice that absLoop does not look inside Rec. But there could be a Loop (with the right n) there! e7 is actually Rec (\e1-> Add (Const 2) (Rec (\e2-> Add (Loop 0) e2))) We might also cast a suspicious eye at (==), which spuriously returned True! Really, we want absLoop to eliminate all the Loops it can find. But it can't, because it only knows the replacement expression for one Loop. It would be simpler for the Loop just to contain the expression. To enable that, I added a constructor Stop that is like Loop, except it takes an Expr instead of an Int. I use this constructor for my sharing unwind as well; Loop is only needed for (==). (It would probably be even better to add an annotation type argument to Expr; this could enable stricter typechecking that would have caught the bug.) Complete code: > {-# OPTIONS -fglasgow-exts #-} > > data Expr = Const Int > | Add Expr Expr > | Rec (Fix Expr) -- implicit loop > | Loop ID -- not exported > | Stop Expr > > type Fix a = a -> a > type ID = Int > > instance Eq Expr where > e1 == e2 = > let eq (Const x) (Const y) n = x == y > eq (Loop i1) (Loop i2) n = i1 == i2 > eq (Add e1 e2) (Add e1' e2') n = eq e1 e1' n && eq e2 e2' n > eq (Rec fe1) (Rec fe2) n = eq (fe1 (Loop n)) > (fe2 (Loop n)) (n+1) > eq _ _ n = False > in eq e1 e2 0 > > unwind :: Expr -> Expr > unwind e = absStop (unwind' e) where > unwind' (Add e1 e2) = Add (unwind' e1) (unwind' e2) > unwind' (Rec fe) = Stop e where e = absStop (unwind' (fe (Stop e))) > unwind' e = e > > mapE :: (Int->Int) -> Expr -> Expr > mapE f e = mapE' e where > mapE' (Const i) = Const (f i) > mapE' (Add e1 e2) = Add (mapE' e1) (mapE' e2) > mapE' (Rec fe) = Rec (\e -> absStop (mapE' (fe (Stop e)))) > mapE' e@(Stop _) = e Replacement for absLoop that removes all Stops, unlike absLoop which only removed the Loops that its caller owned. > absStop (Stop e) = e > absStop (Add e1 e2) = Add (absStop e1) (absStop e2) > absStop e = e The mapE examples still work ... > e4 = Rec (\e1-> Add (Const 1) > (Rec (\e2-> Add e1 e2))) -- nested loop > e4u = unwind e4 -- infinite > e7 = mapE succ e4 > e8 = Rec (\e1-> Add (Const 2) > (Rec (\e2-> Add e1 e2))) > b4 = e7==e8 -- returns True! ... and we verify that we didn't leave behind any Loops/Stops. > hasLoop (Const _) = False > hasLoop (Add e1 e2) = hasLoop e1 || hasLoop e2 > hasLoop (Rec fe) = hasLoop (fe (Const 1)) > hasLoop (Loop _) = True > hasLoop (Stop _) = True > > hasLoop e7 -- False Unwound infinite data structures (even with nested loops) exhibit sharing: main runs in constant space. > main = walk e4u where > walk (Add e1 e2) = walk e2 Andrew _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe