Internalized Guarded Recursion for Equational Reasoning

50 · Edward Kmett · Oct. 21, 2022, 7:31 p.m.
I recently presented a paper on infinite traversals at the Haskell Symposium: A totally predictable outcome: an investigation of traversals of infinite structures. The main result there is a characterization of when a call to traverse on an infinite Traversable functor (like an infinite lazy list) yields a non-bottom result. It turns out this is a condition on the Applicative one traverses with that loosely amounts to it having only a single data constructor. What I want to talk about here is ho...