Trying to understand non termination for mapcat on colist

[bsless]

Hi, I'm playing with https://okmij.org/ftp/papers/LogicT.pdf When I get to the implementation of logic monad interleave, the example diverges on rewrites although it should succeed. What am I doing wrong here? Do I need to delay evaluation in some way?

// Test driver
(Main test n) = (Test test n)

// Logic

(If 1 t e) = t
(If 0 t e) = e

// List ops
(Map f Nil        ) = Nil
(Map f (Cons x xs)) = (Cons (f x) (Map f xs))

(Concat Nil ys) = ys
(Concat (Cons x xs) ys) = (Cons x (Concat xs ys))

(Mapcat f (Cons x xs)) = (Concat (f x) (Mapcat f xs))
(Mapcat f Nil) = Nil

(Test 0 a) = (Mapcat @x(Cons x (Cons x Nil)) [1, 2, 3])

(Take n Nil) = Nil
(Take 0 _) = Nil
(Take n (Cons x y)) = (Cons x (Take (- n 1) y))

Nats = (Cons 0 (Map λx(+ x 1) Nats))

// Test take
(Test 111 n) = (Take n (Nats))

// Test mapcat and concat
(Test 112 n) = (Take n (Mapcat @a(Cons a (Cons a Nil)) Nats))
(Test 113 n) = (Concat
                (Take n (Mapcat @a(Cons a (Cons a Nil)) Nats))
                (Take n (Mapcat @a(Cons a (Cons a Nil)) Nats)))

// Monad

(Bind (Cons x xs) f) = (Mapcat f (Cons x xs))
(Bind Nil f) = Nil

(Return (Cons x xs) y) = (Cons y Nil)
(Return Nil y) = (Cons y Nil)

// Mplus

(Mplus (Cons x xs) ys) = (Concat (Cons x xs) ys)
(Mplus Nil ys) = (Concat Nil ys)

(Mzero (Cons x xs)) = Nil

// Msplit - runs computation

(Msplit (Cons x xs)) = (Cons (Just (Tuple x xs)) Nil)
(Msplit (Cons)) = (Cons Nothing Nil)
(Msplit Nil) = (Cons Nothing Nil)

// Interleave - fair disjunction

(Interleave xs ys) =
    (Bind (Msplit xs) @r(Interleave.Case r ys))

(Interleave.Case Nothing ys) = ys
(Interleave.Case (Just (Tuple x xs)) ys) =
    (Mplus (Return xs x) (Interleave ys xs))

(Test 2 a) = (Interleave [1, 2, 3, 4, 5, 6, 7] [11, 12, 13, 14, 15, 16, 17, 18, 19, 20])

// Some tests

Odds = (Mplus
        (Cons 1 Nil)
        (Bind Odds @a(Cons (+ 2 a) Nil)))

(Test 114 n) = (Take n (Odds))

// (Test 115 n) = (Take n (Bind
//                         (Mplus (Odds) (Cons 2 Nil))
//                         @x(If (== 2 x) (Cons x Nil) Nil)))

// Works
(Test 116 n) = (Take n (Interleave (Odds) (Cons 2 Nil)))


// Works
(Test 117 n) = (Take n (Map
                        @x(If (== 2 x) (Cons x Nil) Nil)
                        (Interleave (Odds) (Cons 2 Nil))))

// Borked - mapcat?
(Test 118 n) = (Take n (Mapcat
                        @x(If (== 2 x) (Cons x Nil) Nil)
                        (Interleave (Odds) (Cons 2 Nil))))

Specifically, it eventually expands to (Cons 2 (Take (- 1 1) (lots of stuff))) at which point I'd expect it to reduce to Take 0 and terminate

[VictorTaelin]

I don't have the time to study your code right now, but two suggestions are:

1. Use hvm debug file.hvm to see step-by-steep how your code is reduced.
2. Use the new (HVM.log msg return) feature (see the /examples dir) to inspect relevant parts of your reduction.

Let me know if you figure out what is going on.

[bsless]

I'm still not sure what the problem is. I opened the ticket after running in debug mode, which is where my last remark comes in, eventually, I end up with:

(Cons 2 (Take (- 1 1) $(Concat a0 (Mapcat @x2 (If (= 2 a3) (Cons b3 b0) b4) (Concat (Concat (Concat (Nil) (Interleave a5 (Nil))) (Mapcat @x12 (Interleave.Case x12 b5) (Nil))) (Mapcat @x13 (Interleave.Case x13 (Cons 2 (Nil))) (Nil)))))))
dup a5 b5 = (Cons b6 b8);
dup * b1 = (Nil);
dup a9 b9 = (Nil);
dup * b8 = (Concat a9 (Mapcat @x10 (Cons b7 b9) (Concat (Nil) (Bind (Odds) @x11 (Cons (+ 2 x11) (Nil))))));
dup * b4 = (Nil);
dup a7 b7 = (+ 2 {1 x10});
dup * b6 = a7;
dup a0 b0 = b1;
dup a3 b3 = x2;

I'd expect (- 1 1) to get reduced to 0, then (Take 0 ...) to be reduced to Nil but it just never gets there. Instead, the chain of the recursively defined list keeps getting expanded ad infinitum. Is it possible there's a problem with my definition of concat?

[VictorTaelin]

Your Concat is fine. Isn't the non-termination caused by the fact the first element of the (Interleave (Odds) (Cons 2 Nil)) list is 1? Thus, since your Mapcat has an if x != 2 then (Concat Nil ...), and since (Head your_list) != 2, then, what you're doing is, essentially, (Concat Nil (Concat Nil (Concat Nil (Concat Nil ....)))) infinitely, so you never reach any productive output. I may be wrong, not familiar with your algo. But if you replace @x(If (== 2 x) (Cons x Nil) Nil) by @x(If (== 2 x) (Cons x Nil) (Cons 5 Nil)) for example, it will work fine,

[bsless]

The algorithm:

• interleave odds and [2]
• mapcat @x(If (== 2 x) (Cons x Nil) Nil)
• take the first element

my expectation, which may be wrong, is that the runtime is lazy, thus I can take the first element, while even trying to take the second will diverge. As you can see It ends up Consing the 2 out of that interleaved list, but (Take (-1 1) ...) isn't ever reduced to (Take 0 ...), the other argument to Take keeps getting expanded

[VictorTaelin]

Ah - HVM has a weird (that, to be fair, was accidental and I should change) property that it evaluates arguments from right to left. So, it attempts to first evaluate the second argument of Take, which loops (because you're trying to get the head of an infinite (Concat Nil (Concat Nil ...))), so it never has the chance of evaluating the first argument. You're right that your program would normalize if it did it in the opposite order (but then it would loop again if you inverted the order of Take). I completely forgot about that, otherwise I'd have pointed it earlier.

[bsless]

Huh, that's peculiar. Is there a way to sort of round-robin arguments reduction? There's no reason to prioritize one over the other in terms of processing time. And it violates laziness

[bsless]

To add a bit on the subject, it has a curious overlap with the paper I've been playing with in this thread: Fair evaluation (e.g. or) should interleave execution, it's BFS and not DFS. Composition (application?) is analogous to and, and can also be interleaved in a fairer manner. In Clojure it would look like:

(extend-protocol ILogicM
  nil
  (-interleave [_ sg2] sg2)
  (>>- [_ g] nil)

  clojure.lang.ISeq
  (-interleave [sg1 sg2]
    (lazy-seq
     (if-let [[sg11 & sg12] (seq sg1)] ;; like matching on (Cons x xs) or Nil
       (cons sg11 (-interleave sg2 sg12)) ;; note how sg2 and the rest of sg1 flip order here
       sg2)))
  (>>- [sg g]  ;; this is fair bind
    (lazy-seq
     (if-let [[sg1 & sg2] (seq sg)]
       (-interleave (g sg1) (>>- sg2 g))
       ()))))

[VictorTaelin]

Yep, that sounds right. HVM wasn't made with that in mind, but interleaving computations would be really cool. Note that the parallel version does that, to an extent, since it sparks a thread to reduce each argument independently. But surely that is one (of the many) areas that can be improved.

[bsless]

Since HVM is supposed to be fully lazy and in this exercises it eagerly evaluates an infinite computation, should it be considered a bug? Not trying to create extra work for you, even if it is a bug you got other priorities as well, but I'm not sure how to proceed with from here :upside_down_face:

[VictorTaelin]

I don't think this is bug, GHC will exhibit the same behavior, no? Interleaved computation would greatly impact performance, I suspect, so that isn't desirable. I don't think the usual definition of laziness covers interleaved execution of parallel matches, and I've never seen a language behave that way. A lazy language is one that doesn't do any work that isn't needed to reach the normal form, and the work it is doing in your case is needed, since the normal form of your program depends on observing the result of reducing that infinite list (which is impossible).

What you're asking isn't exactly laziness, but more akin to a runtime that operates like Cantor's diagonalization argument, or Haskell's Omega monad. Which is actually really cool, but stronger concept than what is usually meant by laziness, and I'm not sure if there is a name for it. But such concept isn't even possible on the λ-calculus, since there aren't parallel matches to begin with. HVM's lambda calculus is as lazy as technically defined, and so are its constructors. I wonder if we could achieve the effect you want by just selecting redexes breadth-first, or if we'd need something more complex/costly.

Anyway, that is just my analysis and understanding of the subject, but I may be wrong, let me know if you think that is the case.

[bsless]

I don't think you are wrong, I guess the fundamental question is: Does the runtime need to reduce all the arguments to reach a valid redex? If I have (Foo x y) = x I never need to reduce y to reduce (Foo x y) In my use case I have (Take 0 xs) = Nil, but reduction never ends up with that 0.

Why would interleaving computations be too expansive?

Anyway, there are some ML papers on selecting the optimal order of matching: Compiling Pattern Matching to good Decision Trees This could probably be a reasonable compromise and an optimization. Also see example implementation https://github.com/clojure/core.match/wiki/Understanding-the-algorithm

Do you have advice or thoughts on how I should proceed now with my case?

PS

interleaved execution of parallel matches

This is essentially the Amb operator?

[VictorTaelin]

Why would interleaving computations be too expansive?

I'm not sure, but I can't think of a way to do it right now. That's a great idea overall, if possible to implement.

[bsless]

I don't know why, but it reminds me of Dan Friedman's work on Frons, which are a sort of data structure X computation engine which managed to fairly allocate computational resources to different branches of computation. It's like two orthogonal problems - the abstract algorithm of efficiently reducing lambda terms, and an abstract computer, which efficiently, correctly and fairly executes those reductions.

[ydewit]

I am experiencing what I think is a similar behavior when trying to implement Delay and Force.

Consider the following mwe:

(If 1 t f) = t
(If 0 t f) = f
(Force (Delay c)) = c
(Force x        ) = x
(Loop n) = (Delay (If (== n 0) Done (Loop (- n 1))))
(Main) = (Loop 4)

I was expecting this to finish early with: Delay (If (= a0 0) (Done) (Loop (- b0 1))) since there is no LHS that matches Delay. But HVM is eagerly reducing nested constructor arguments causing the infinite loop.

Irrespective to left-to-right, right-to-left or interleaved, isn´t HVM being too eager here?

[ydewit]

@bsless Setting aside the lazy vs strict vs unbounded recursion issue, couldn't you achieve interleaving by switching the "rest of the stream" in MPlus:

...
(MPlus (List.cons x xs) list) = (List.cons x (MPlus list xs)) // invert list to interleave

Or are you trying to keep MPlus without interleaving the streams and then layer interleaving on top of it?

[bsless]

@ydewit I wanted to go for a straightforward implementation of the paper, where mplus is monadic concat and interleave is implemented with mplus and bind:

// Interleave - fair disjunction

(Interleave xs ys) =
    (Bind (Msplit xs) @r(Interleave.Case r ys))

(Interleave.Case Nothing ys) = ys
(Interleave.Case (Just (Tuple x xs)) ys) =
    (Mplus (Return xs x) (Interleave ys xs))