Hi Ryan,

On Fri, Jun 18, 2010 at 7:57 PM, Ryan Ingram <ryani.spam@gmail.com> wrote:
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.


-Edward Kmett