Open rpglover64 opened 10 years ago
What are inc
and dec
semantically?
I think with multiple arguments you could generate and partially evaluate infinite sets of expression trees over the functions, but what troubles me there is that you'd want to have some way to guess at how to search efficiently through that space. Do you know any imperative algorithms to do this efficiently?
Non-commutative should be subsumed in a similar process as the commutative ones, but won't have as many optimizations. There's an interesting package floating around that lets people define H98 functions with proof of commutativity, so perhaps we could abuse that to get typesafe speedups.
In particular, you'd want to prune your expressions by their answers. I could see how that could be done if we had a lot of information about the function, but for any function/algebra signature I don't know a good strategy.
By inc
and dec
, I meant succ
and pred
; I used the Clojure names by accident.
Oh—I see. Altogether we're talking about closures of algebras. Given some set of functions
f1 :: A^n1 -> A
f2 :: A^n2 -> A
...
fm :: A^nm -> A
how can we find the set A
which is the fixed point of applying all of those. We can also express it as an algebra over a Functor
maybe which would be useful since it's similar to the notion of datatypes in Haskell. So we could express that as
Given some polynomial Functor F
which we express in disjunctive normal form we have
data F a = F1 (Vec n1 a)
| F2 (Vec n2 a)
...
| Fm (Vec nm a)
which represents the algebra specific previously with functions of the style F A -> A
alg :: F A -> A
alg (F1 as) = f1 as
alg (F2 as) = f2 as
...
alg (Fm as) = fm as
Which is nice because then if we define
newtype Fix f = Fix { unfix :: f (Fix f) }
then we can always define alg
by mapping from Fix F
. In other words, Fix F
is the (potentially infinite) data type which represents the entire expression tree for our algebra.
Now how to search that tree effectively...
Right. That's a very good way of putting it.
I think searching effectively in the fully general case is impossible, because if there are n
values known to be in the set and I have an m
-ary function and a new value, I think I have to try (n+1)^m - n^m
. I think the solution would have to be to take hints on what not to pass in from the user (e.g. don't pass (+)
zeros, because that won't give you any new information).
I was wrong about functions giving multiple outputs being encodeable with multiple functions, since they may give a different number of outputs depending on the input. Consider the following (impractical and pathological) function:
f a = genericTake a $ iterate succ a
I'm not sure how important that is to support, though.
I think it might be possible to at least give a little bit of direction to the functor algebra approach. I can't see how it would work at all with the multiple returns example you suggested there.
This feels so much like something that Bird would write about.
Bird?
With multiple returns, you have a separate set of new and set of old values (in concept if not in practice), you add each of the (possibly zero) outputs to the new set, then you loop over the new set, moving values to the old set as you close over them, merging their values into the new set if they're not in the old set; I think this is breadth-first, but depth-first can build up a lot of unnecessary thunks.
Richard Bird is who I usually associate with the Algebra of Programming and various calculation all methods to programming. This feels a lot like some of his books.
— Sent from Mailbox for iPhone
On Fri, Nov 8, 2013 at 5:54 AM, Alex R notifications@github.com wrote:
Bird?
With multiple returns, you have a separate set of new and set of old values (in concept if not in practice), you add each of the (possibly zero) outputs to the new set, then you loop over the new set, moving values to the old set as you close over them, merging their values into the new set if they're not in the old set; I think this is breadth-first, but depth-first can build up a lot of unnecessary thunks.
Reply to this email directly or view it on GitHub: https://github.com/tel/closure/issues/2#issuecomment-28054861
inc
anddec
both). Could this be encoded using a closure of closures?(+)
); these can be encoded by adding curried elements to the set, but that isn't particularly clean and it's not straightforward to see what e.g.(Curried 3) + (Curried 5)
is;Curried (3 + 5)
works in this case, but I don't know if it generalized