Hello Juan, On 7/11/19 3:24 PM, Juan Casanova wrote:
I just subscribed to this list so I'm not familiar with the usual way to go about things here. I hope you'll excuse any cultural mistakes I might make.
You're most definitely welcome here. I dare say that anyone who participates in the mailing list makes the rules (within the limits of moderation of course).
feel free to ask for it and I'll happily send it over, so that you can run the example with it.
I am curious to have a look at your library.
Let me introduce the problem that I'm trying to solve itself. I have a particular (yet somehow typical) case of non-determinism (search) in the program that I have been writing. It is characterized by:
- No joining back of branches ever. - Potentially infinite depth (this is usual). - Potentially infinite width. Meaning that at a single point I may have an infinite amount of possible paths to follow. - It is critical that the search is complete. After reading a bit, I have realized this is usually referred to as being a fair search order. For me this means that there can be many (infinite) valid solutions in the search space, and I want to find all of them (i.e. for every valid solution, the program will eventually output it).
I think all of these points can be addressed by starting from an infinite binary tree. data Tree a = Empty | Leaf a | Branch (Leaf a) (Leaf a) instance Monad Tree where ... In particular: - infinite branching can be modeled by an infinite sequence of finite branches: Branch 1 (Branch 2 (Branch 3 (...))); - the problem of completeness is addressed by, uh, postponing it. Okay that's not really addressed, but the point is that the data is all there at least (not lost in a diverging computation), and the search problem is now a very concrete tree traversal problem, which does not require any fancy monadic abstraction a priori, but also does not prevent you from building one up as other requirements make themselves known. Regarding the issue of fairness you mention, a key point is that "filter" should only replace Leaf with Empty, and not try to do any merging like rewriting (Branch Empty t) to t. More precisely, as soon as a function satisfies the equation f (Branch Empty t) = f t, then it has to diverge on trees with no leaves (or it has to discard leaves, so it's useless if completeness is a concern). I'm guessing that's where the logic monad goes astray. One way to think of this problem is in terms of "productivity": "filter" for Logic may not be productive if its argument represents an infinite search space. In total programming languages, i.e., those which enforce productivity, Agda and Coq being chief examples, you would actually be stopped because the Logic monad cannot represent infinite search spaces (such as log_multiples in your sample). Coinductive types are a promising alternative here, with two main solutions off the top of my head being coinductive trees, as I sketched above, and coinductive lists/streams with an extra "delay" constructor. I am curious to see how your library relates to that. Cheers, Li-yao