Fixing idioms
Dominique Devriese, Ilya Sergey, Dave Clarke, Frank Piessens · 2013
In a lazy functional language, the standard encoding of recursion in DSLs uses the host language's recursion, so that DSL algorithms automatically use the host language's least fixpoints, even though many domains require algorithms to produce different fixpoints. In particular, this is the case for DSLs implemented as Applicative functors (structures with a notion of pure computations and function application). We propose a recursion primitive afix that models a recursive binder in a finally tagless HOAS encoding, but with a novel rank-2 type that allows us to specify and exploit the effects-values separation that characterizes Applicative DSLs. Unlike related approaches for Monads and Arrows, we model effectful recursion, not value recursion.