Internalised Guarded Recursion for Equational Reasoning

Links
#1

I just published a post at The Comonad.Reader » Internalized Guarded Recursion for Equational Reasoning which gives a introduction to work I presented at the Haskell Symposium, with a few simple examples of its use.

The post shows how the technique introduced in that paper, “internal guarded recursion,” can be used not only in a lightweight formal way, but just in everyday programming as a “back of the envelope” technique to quickly figure out when recursive functional programs terminate and when they go into infinite loops.

I think the approach is very simple to use, and hope people can come up with lots of classes of examples where it can be helpful.

4 Likes
#2

I just saw the talk on youtube. It was very interesting. I wonder when I’ll get an excuse to use it.

#3

It looks like some of the code lines are cut off on the website, e.g. I only see this on my screen:

repMin1 :: (Traversable t, Ord a) => t a -> t a
repMin1 xs = let (ans,m) = fmap minimum . runWriter $ traverse (\x -> tell [x]
1 Like
#4

Based on that mangled (<*>) operator in the initial Haskell example:

newtype Later a = Later a deriving Functor
instance Applicative Later where
    pure = Later
    Later f < *> Later x = Later (f x)
     --     ^^^^

…it could be yet another site-formatting error.

As for the concept itself: it looks like a “small-footprint” variant of total programming (as opposed to actual total programming, which bans implicit general recursion outright) - nicely done.

#5

Whoops, fixed the formatting a bit for those lines. Thanks for noticing!

2 Likes
#6

Very interesting!

I still have a lot of the code snippets getting cut off, as well as < *>.