LogicT isn't lazy enough

[treeowl]

I would expect that

(pure 1 <|> pure 2) <|> undefined :: Logic

would be able to produce 1 and 2 before failing, but in fact it can only produce 1. The problem is the rather aggressive Empty matching in the definition of >< for bootstrapped queues. The fix is to remove that. The price of the fix is that if a bunch of emptys in a row get <|>ed onto the logic computation then views in multiple futures may each have to drop them. This is very similar, I think, to the cost of >=>ing a bunch of pures onto a free Kleisli category. Unfortunate, but unavoidable.

[treeowl]

I think the previous attempt to make it lazier should be backed out, in favor of a change to the underlying queue. I realized a couple things that may be helpful for keeping things theoretically clean, while also making them lazy enough:

1. We currently represent empty as an empty queue, but it can alternatively be represented as a singleton queue containing pure Nothing. That means we can actually use nonempty catenable queues instead of normal ones.
2. Nonempty catenable queues can be rather surprisingly (to me) lazy, while maintaining correct amortized bounds. The key idea is that amortization for normal catenable queues only requires strictness because allowing the tree to accumulate empty queues breaks amortization in the face of persistence.

Question: does this sort of thing help with any other monads?

[treeowl]

A minimal fix to the catenable queue implementation:

 C0        >< ys  = ys
-- Remove this line: xs        >< C0  = xs
 (CN x q)  >< ys   = CN x (q |> ys)

 tviewl C0             = TEmptyL
 tviewl (CN h t)  = h :| linkAll t
   where 
    linkAll :: TSequence q =>  q (CTQueue q c) a b -> CTQueue q c a b
    linkAll v = case tviewl v of
     TEmptyL      -> C0
     C0 :| t -> linkAll t
     CN x q :| t
       | TEmptyL <- tviewl t -> CN x q
       | otherwise -> CN x (q |> linkAll t)

The definition of mplus can be simplified back to

  ML xs `mplus` ML ys = ML (xs >< ys)

---

One caveat: that queue is used for several other monads. I have no idea whether the change makes sense for them.

[atzeus]

Hi! Sorry for the belated response. I would also expect this lazy behavior. Your minimal fix makes sense. I think this just improves the strictness properties so I do not think it can have any adverse effects (?)

[treeowl]

If you're looking to implement a principled data structure with the right persistently amortized bounds and then build the r-w-r stuff on top, then you need to replace the catenable list with a lazy catenable nonempty list. If you don't care about principled separation, you can make a lazy catenable list that doesn't drop empties, as I've shown, but that underlying structure doesn't have proper persistently amortized bounds—the same empties may need to be dropped multiple times.

Like I said, for LogicT I don't think there can be bad effects, but I haven't gone through and looked at the rest.