A Totally Predictable Outcome: An Investigation of Traversals of Infinite Structures
summary
Claims that every traversable functor admits an infinite traversable instance and that an infinite traversal is productive iff the applicative used is of the right kind. Builds a lightweight guarded-recursion model inside Haskell using an opaque newtype later, an evaluator/coerce export and a later applicative, and formulates guarded equivalence to lift proofs to ordinary Haskell. Characterizes a new class called predictable functors (Reader/representable, many compositions and products) and explains why coproducts like Maybe/Either and some State cases fail; extracts practical equational reasoning (a few lines of code).
AI-written summary · about
chapters (8)
- 0:00Intro
- 0:44Traversable Functors circa 2010s
- 4:37Internal Guarded Recursion
- 6:19Evaluation of Guarded Recursive Terms
- 7:58Equivalence of Guarded Recursive Terms
- 10:24Infinite Traversals
- 13:07Predictable Functors
- 16:35Immediate Results
related talks
49mMaking sense of the Haskell type system
38mRefactoring Recursion
34mHaskell⁻¹: Automatic Function Inversion in Haskell
01h 06mTransient: Unrestricted Algebraic and Monadic Composability
01h 04mHaskell - A Peek Inside the Ivory Tower
01h 22mHaskell for Everyday Programmers
59mKeynote: Dependently-Typed Haskell
01h 10mA History of Effect Systems