search

compiling-to-categories / concat

Compiling to Categories
http://conal.net/papers/compiling-to-categories
BSD 3-Clause "New" or "Revised" License
436 stars 50 forks source link

Should this auto diff example work? #84

Closed freckletonj closed 2 years ago

freckletonj commented 2 years ago

I'm still getting accustomed to this library+plugin, and I think I'm confusing what happens at what phase. For instance, the following exhausts the rewrite ticks, so I assume there's a rewrite loop. Is it because deriv is trying to make the derivative's category (->)? I'm really not sure, this all seems quite magical, but in a good way!

x :: (Double, Double)
x = let f :: Double -> Double
        f x = x ** 2 + 123
        df :: Double -> (Double -> Double)
        df x = deriv f x
    in (f 10, df 10 10)

Any chance I could get a hand with what I'm doing wrong?

freckletonj commented 2 years ago

solved it!

df :: Double -> (Double -+> Double)

let me know how I can help with this library!

mikesperber commented 2 years ago

let me know how I can help with this library!

Just try more stuff and report issues. I would have gotten to this one eventually, was just too slow.

conal commented 2 years ago

I appreciate the attention on & help with concat. My recent energy is devoted to reworking the theory and practice of designing and compiling with categories in Agda, this time with elegant formal specifications and proofs.