Hi Ryan,
On Fri, Jun 18, 2010 at 7:57 PM, Ryan Ingram
Related to this, I really would like to be able to use arrow notation without "arr"; I was looking into writing a "circuit optimizer" that modified my arrow-like circuit structure, but since it's impossible to "look inside" arr, I ran into a brick wall.
Has anyone done any analysis of what operations arrow notation actually requires so that they can be made methods of some typeclass, instead of defining everything in terms of "arr"?
It seems to me the trickiness comes when you have patterns and complex expressions in your arrow notation, that is, you write
(a,b) <- some_arrow <- (c,d) returnA -< a
The design I've been using for this has been to use data-reify, and observable sharing and to use pure let bindings to build the circuit. full_adder :: Bit -> Bit -> Bit -> (Bit, Bit) full_adder a b cin = (s2, c1 || c2) where (s1,c1) = half_adder a b (s2,c2) = half_adder s1 cin half_adder :: Bit -> Bit -> (Bit, Bit) half_adder a b = (a `xor` b, a && b) foo = do x <- exists y <- exists z <- exists assert $ full_adder x y z === (1,1) assert $ forall $ \ a b c -> (a && b) ==> c === (a ==> b ==> c) return (x,y,z) I perform a similar sharing recovery in the back end code of Numeric.RAD from the 'rad' package and Numeric.AD.Internal.Reverse in the 'ad' package. I have uses in a number of unreleased bottom-up applicative parser combinators as well, so it has a wide arrange of applicable situations. Overall, let bindings tend to be a lot lighter than the accompanying arrow sugar. You might find Andy Gill's write-up on type safe observable sharing in kansas lava to be useful. http://www.ittc.ku.edu/~andygill/papers/reifyGraph.pdf -Edward Kmett