[Haskell-cafe] "Quantization" of computations, or step-wise termination, as an extension of Logic Monads

[Li-yao Xia]

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