Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Haskell self-referential List termination

EDIT: see this followup question that simplifies the problem I am trying to identify here, and asks for input on a GHC modification proposal.

So I was trying to write a generic breadth-first search function and came up with the following:

bfs :: (a -> Bool) -> (a -> [a]) -> [a] -> Maybe a
bfs predf expandf xs = find predf bfsList
    where bfsList = xs ++ concatMap expandf bfsList

which I thought was pretty elegant, however in the does-not-exist case it blocks forever.

After all the terms have been expanded to [], concatMap will never return another item, so concatMap is blocking waiting for another item from itself? Could Haskell be made smart enough to realize the list generation is blocked reading the self-reference and terminate the list?

The best replacement I've been able to come up with isn't quite as elegant, since I have to handle the termination case myself:

    where bfsList = concat.takeWhile (not.null) $ iterate (concatMap expandf) xs

For concrete examples, the first search terminates with success, and the second one blocks:

bfs (==3) (\x -> if x<1 then [] else [x/2, x/5]) [5, 3*2**8]
bfs (==3) (\x -> if x<1 then [] else [x/2, x/5]) [5, 2**8]
like image 533
Erik Avatar asked Jan 04 '23 09:01

Erik


1 Answers

Edited to add a note to explain my bfs' solution below.

The way your question is phrased ("could Haskell be made smart enough"), it sounds like you think the correct value for a computation like:

bfs (\x -> False) (\x -> []) []

given your original definition of bfs should be Nothing, and Haskell is just failing to find the correct answer.

However, the correct value for the above computation is bottom. Substituting the definition of bfs (and simplifying the [] ++ expression), the above computation is equal to:

find (\x -> False) bfsList
   where bfsList = concatMap (\x -> []) bfsList

Evaluating find requires determining if bfsList is empty or not, so it must be forced to weak head normal form. This forcing requires evaluating the concatMap expression, which also must determine if bfsList is empty or not, forcing it to WHNF. This forcing loop implies bfsList is bottom, and therefore so is find.

Haskell could be smarter in detecting the loop and giving an error, but it would be incorrect to return [].

Ultimately, this is the same thing that happens with:

foo = case foo of [] -> []

which also loops infinitely. Haskell's semantics imply that this case construct must force foo, and forcing foo requires forcing foo, so the result is bottom. It's true that if we considered this definition an equation, then substituting foo = [] would "satisfy" it, but that's not how Haskell semantics work, for the same reason that:

bar = bar

does not have value 1 or "awesome", even though these values satisfy it as an "equation".

So, the answer to your question is, no, this behavior couldn't be changed so as to return an empty list without fundamentally changing Haskell semantics.

Also, as an alternative that looks pretty slick -- even with its explicit termination condition -- maybe consider:

bfs' :: (a -> Bool) -> (a -> [a]) -> [a] -> Maybe a
bfs' predf expandf = look
  where look [] = Nothing
        look xs = find predf xs <|> look (concatMap expandf xs)

This uses the Alternative instance for Maybe, which is really very straightforward:

Just x  <|> ...     -- yields `Just x`
Nothing <|> Just y  -- yields `Just y`
Nothing <|> Nothing -- yields `Nothing` (doesn't happen above)

so look checks the current set of values xs with find, and if it fails and returns Nothing, it recursively looks in their expansions.

As a silly example that makes the termination condition look less explicit, here's its double-monad (Maybe in implicit Reader) version using listToMaybe as the terminator! (Not recommended in real code.)

bfs'' :: (a -> Bool) -> (a -> [a]) -> [a] -> Maybe a
bfs'' predf expandf = look
  where look = listToMaybe *>* find predf *|* (look . concatMap expandf)

        (*>*) = liftM2 (>>)
        (*|*) = liftM2 (<|>)
        infixl 1 *>*
        infixl 3 *|*

How does this work? Well, it's a joke. As a hint, the definition of look is the same as:

  where look xs = listToMaybe xs >> 
                  (find predf xs <|> look (concatMap expandf xs))
like image 100
K. A. Buhr Avatar answered Jan 13 '23 13:01

K. A. Buhr