[Haskell-cafe] "Quantization" of computations, or step-wise termination, as an extension of Logic Monads
lysxia at gmail.com
Fri Jul 12 01:21:51 UTC 2019
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
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 ...
- 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.
More information about the Haskell-Cafe