[Haskell-cafe] "Quantization" of computations, or step-wise termination, as an extension of Logic Monads
Juan Casanova
juan.casanova at ed.ac.uk
Thu Jul 11 19:24:50 UTC 2019
Dear all,
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. I'll also try to keep this message as short as possible,
but this is hard for me and it is a complex topic, so I will
presumably fail. Apologies for that in advance.
Short introduction. I'm a PhD student at University of Edinburgh. My
research is not on programming languages itself, but during the course
of it I ended up programming in Haskell and more particularly faced a
problem that I developed a strategy (and eventually a library) for.
After some discussions with my supervisors and with some more Haskell
experienced people around university, they suggested that I looked
into some existing work and also that I posted on this list, and here
I am.
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).
As I said, I developed my own (particular) approach to this, then
generalized it in a library, and then, after talking to some people,
realized this might be something quite interesting to share, but first
had to check that it's not something that has already been done.
Long story short, the most relevant piece of research I was pointed to
was "Backtracking, interleaving and terminating monad transformers",
by O Kiselyov, C Shan, DP Friedman and A Sabry, published in 2005.
(https://dl.acm.org/citation.cfm?id=1086390). I also know that this
approach is embodied in Haskell through the Control.Monad.Logic
library. I read the paper and skimmed through some related work, and
gave a try to the library. Indeed, it seems to be doing mostly what I
need. In particular, it can deal with infinite breadth/infinite width
searches through a process of what I call "diagonalization". That is,
a combination of breadth-first and depth-first that ensures fairness.
Note that the library actually does a lot more things that I didn't
consider because they were not relevant for my problem, for instance
cuts.
However, I find that there is something that this library does not
take into account, and after trying with the Haskell library I have
verified that indeed it does not work, whereas my library does work. I
am wondering if I have overlooked some work in which this is also
taken into account or if I may be onto some useful extension of
Control.Monad.Logic that hasn't been done yet. I still have to find a
stable name for the feature that I am talking about, but I usually
refer to it as "step-wise termination" or "quantization of
computations". To understand it consider an example (that I have
actually implemented):
1. Whenever I have a non-deterministic enumeration, I should have a
way to output a fair search among that non-deterministic search (a
list), following the properties that I indicated above.
2. I can make an enumeration that non-deterministically produces all
multiples of a certain number.
3. I can make an enumeration that non-deterministically produces all
powers of a certain number.
4. I can make a function that, given an enumeration, filters it
through a boolean function.
5. I can monadically combine computations, so that I can, for
instance, produce a computation that is the result of producing all
multiples of a number, and for each of those, producing all their
powers.
6. So what happens if I combine the three of them. In particular, what
if I output all *odd* powers of all multiples of 1 (all naturals)?
(multiples 1) >>= (\x -> filter odd (powers x))?
If I do this using the Control.Monad.Logic library (and using the >>-
operator provided there, of course), this does not produce a fair
search. Specifically, it outputs 1 and then hangs up. The reason? The
order in which the search is produced picks one value from each
sublist at a time, but because there are no odd powers of an even
number (say 2), it never finds any element in the sublist of powers of
2, and therefore never gets to even try with the powers of 3.
My library can deal with this by "quantizing" computation, making sure
that each individual step of a computation always terminates (in
Haskell terms, I wrap things up in a way that I can guarantee that a
single look-ahead on the list will always produce a head normal form
in finite time, even if that is still a continuation of the
computation). Therefore, while it keeps trying to find powers of 2
that are odd, this does not stop the search over all the other sublists.
This mail is already quite long, but let me make a few precisions. You
may stop reading here if you don't wanna get your hands dirty, I've
said the most important bits. I know a bit of what I say here will be
confusing if you don't think about it yourself, so skip it if it gets
confusing. It's mainly to answer some questions/comments I can foresee.
Of course, this only works if the embedding into the monad is
terminating itself. So, when you do "pure x" for my monad, you need to
guarantee that "x" will produce a head normal form in finite time).
But as long as you guarantee this atomic notion and you only use the
monadic transformation functions that are not labelled as "unsafe"
(which are only the unnatural ones for the semantics that I am
considering, such as appending in a list sense), then I can guarantee
the search will always be fair.
Also, a thing I've been thinking quite a bit is whether you can
consider this notion of "quantization" of computation separately from
the notion of an enumeration of a non-deterministic search space. Of
course you can, but the interesting bit is to do this diagonalization
over non-deterministic search spaces in a quantized way so that rabbit
holes like the odd powers of 2 are not a problem. I tried to implement
this in a generic way that you can later on "combine" with
Control.Monad.Logic in a non-specific way, but it won't work, due to
the particular reason that you'd need to do pattern matching over the
structure of the logic monad, and there's no way to type check that
for an arbitrary data type (because the pattern matching could give
literally any potential sub-types). Implementing the quantization
separately and then the combination individually as a one-of thing
could be done, of course, but it would essentially be the same that I
have right now. A different story would be had if ghci actually had
monadic functions to enable the evaluation of *any* thunk
one-step-at-a-time (that is, one function evaluation or one pattern
match). This is absolutely not what seq does, because seq evaluates
until it is a weak head normal form, which is not what I want.
Precisely, bottom seq a = bottom, and my quantized computation does
not fulfill this equation (and it should not).
My library is not perfect now, and after having read and understood
the Control.Monad.Logic library, I think the best thing would be to
extend it, which is something I don't do right now. But still so,
unless I have missed an already existing implementation of something
like this, or I am seeing something in a really convoluted way. Please
feel free to drop any questions or comments at all.
I'm attaching an example of why Control.Monad.Logic does not work in
the case that I said. It also includes an example using my library,
which I am not attaching. This example works. Just comment it. I'm not
attaching my library now because it's not "polished" and because it is
a lot for people to randomly look at, but feel free to ask for it and
I'll happily send it over, so that you can run the example with it.
Again, any questions or comments are welcome. Lead me the right
direction with this.
... And sorry for the wall of text.
Thank you very much for all of your time and attention,
Juan Casanova.
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: LogicVsEnumProc.hs
Type: text/x-haskell
Size: 2065 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190711/6c9484b5/attachment.hs>
More information about the Haskell-Cafe
mailing list