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

[Li-yao Xia]

On 7/11/19 10:56 PM, Juan Casanova wrote:
> Thank you for your very detailed and very relevant response. It made me 
> think about some things.


I'm glad you appreciated my answer!


 >> I am curious to have a look at your library.
 >
 > I guess I'll just attach it here and end up sharing it with the whole
 > list. Just hope noone feels overwhelmed by too much code to look at.


That looks quite reasonable. At a high level, one can imagine this 
basically as a list library, so most functions look quite familiar at a 
glance.


 >> - infinite branching can be modeled by an infinite sequence of finite
 >> branches: Branch 1 (Branch 2 (Branch 3 (...)));
 >
 > This is correct, but not complete in general, although the logic monad
 > library does deal with this. The problem is, if you have a conceptual
 > infinite branching, in which each branch is infinite in depth, the
 > process of expressing the infinite branching as an infinite sequence of
 > finite branching will, if done naively, be unfair towards later
 > branches. So, if I want to search all the multiples of all powers of 2,
 > the "naive" transformation will "concatenate" all those lists /
 > branches, but because the first one is infinite, any search performed in
 > that way will not reach the latter ones. In other words, things that
 > were at depth 2 before will now be at depth infinity because you have
 > prepended them with an infinite amount of finite branches. This can be
 > overcome by doing the transformation from infinite branching to
 > binary/finite branching diagonally, as I described and as the logic
 > monad library does.


For "all the multiples of all powers of 2", the tree obtained naively by 
monadic composition will look like this:

mulPow2 = liftA2 (*) nats pow2s
-- Branch (... multiples of 2^0) (Branch (... multiples of 2^1) (Branch 
(... multiples of 2^2) (...)))

-- where nats contains all natural numbers and pow2s all powers of 2.

No elements are lost precisely thanks to the tree structure allowing you 
to nest subtrees without pushing others back.

That said, your approach is certainly still worth pursuing.


 > What I wonder is if there is indeed a way to do
 > these kind of things with the logic monad library (and perhaps other
 > standard libraries) without having to implement my own?


The problem you described appears to be deeply embedded in the 
definition of LogicT. A handwavy argument is that Logic is exactly the 
Church encoding of lists with Nil and Cons (Empty and Produce), but you 
really need the Continue constructor in there.

One idea to try is "Logic (Maybe a)", since it is isomorphic to [Maybe 
a] which is isomorphic to the Empty+Produce+Continue variant of lists 
(using the names from your code). But although the representation is 
equivalent, I'm not sure the abstractions are reusable enough to save 
much work.


Cheers,
Li-yao