Termination checking of recursive monadic programs

[Li-yao Xia]

Hi all,

I'm wondering about ways to prove termination of certain monadic programs. It looks like this concerns other total languages like Coq, and I'd be happy to hear about those too; I'm asking here first because I'm primarily interested in verifying Haskell programs.

With some type P :: Type -> Type of parsers for example, say there is a primitive consume :: P (Maybe Word) to consume tokens from a finite stream, returning Nothing if none is left. Then we can imagine a parser that consumes all remaining tokens:

    consumeAll :: P [Word]

    consumeAll = do

      x' <- consume

      case x' of

        Just x -> do

          xs <- consumeAll

          return (x : xs)

        Nothing -> return []

Here we have a recursive call that will be rejected with a positivity check based on decreasing arguments, simply because there are no visible arguments. But this function does terminate for the simple reason that the token stream is one element shorter after each recursive step. Many parsers of recursive structures work that way.

Two workarounds I could think of are:

- add a fuel parameter;

- unwrap the P type and inline consume so we can pass the (decreasing) input stream explicitly.

The first adds a fair amount of distracting boilerplate, especially in proofs, and the second defeats the whole point of making P a monad.

Am I missing a simple way to convince liquid that this parser terminates? Can you foresee other problems in using Liquid Haskell for such monadic programs?

Here is a gist to put the above code in context.

Cheers,

Li-yao

[Ranjit Jhala]

Hmm, great question! Ithink the short answer is “I don’t know”

As this has long been an item on our todo list, but we have 

never found a satisfactory solution.

One way, may be to use “bounded refinements” (see the Icfp 15 paper) 

to index the monad with a “ghost” counter 

that gets decremented appropriately? But this is speculation 

and it would be very cool to have a nice solution to this problem!

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.