ABSTRACT
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.
Using generic programming techniques, we define an arity-generic version of the operator to model mutually recursive definitions. We recover intuitive user syntax with a form of shallow syntactic sugar: an alet construct that syntactically resembles the let construct, which we have implemented in the GHC Haskell compiler. We describe a proposed axiom for the afix operator. We demonstrate usefulness with examples from Applicative parser combinators and functional reactive programming. We show how higher-order recursive operators like many can be encoded without special library support, unlike previous approaches, and we demonstrate an implementation of the left recursion removal transform.
- A. I. Baars, A. Löh, and S. D. Swierstra. Parsing permutation phrases. J. Funct. Program., 14(6):635--646, 2004. Google ScholarDigital Library
- A. I. Baars and S. D. Swierstra. Type-safe, self inspecting code. In Haskell, pages 69--79, 2004. Google ScholarDigital Library
- A. I. Baars, S. D. Swierstra, and M. Viera. Typed transformations of typed abstract syntax: The left corner transform. In LDTA, pages 18--33, 2009. Google ScholarDigital Library
- K. Brink, S. Holdermans, and A. Löh. Dependently typed grammars. In MPC, 2010. Google ScholarDigital Library
- J. Carette, O. Kiselyov, and C.-c. Shan. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. J. Funct. Program., 19(05):509--543, 2009. Google ScholarDigital Library
- A. Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In ICFP, pages 143--156, 2008. Google ScholarDigital Library
- N. A. Danielsson. Total parser combinators. In ICFP, pages 285--296, 2010. Google ScholarDigital Library
- N. A. Danielsson, J. Hughes, P. Jansson, and J. Gibbons. Fast and loose reasoning is morally correct. In POPL, pages 206--217, 2006. Google ScholarDigital Library
- N. A. Danielsson and U. Norell. Structurally recursive descent parsing. Draft, 2008.Google Scholar
- D. Devriese and F. Piessens. Explicitly recursive grammar combinators - Implemention of some grammar algorithms. Technical Report CW594, KULeuven CS, 2010.Google Scholar
- D. Devriese and F. Piessens. Explicitly recursive grammar combinators. In PADL, pages 84--98. Springer, 2011. Google ScholarDigital Library
- D. Devriese and F. Piessens. Finally tagless observable recursion for an abstract grammar model. Journal of Functional Programming, 22(06):757--796, 2012. Google ScholarDigital Library
- C. Elliott and P. Hudak. Functional reactive animation. In ICFP, pages 263--273, 1997. Google ScholarDigital Library
- L. Erkök and J. Launchbury. Recursive Monadic Bindings. In ICFP, pages 174--185, 2000. Google ScholarDigital Library
- L. Erkök and J. Launchbury. A recursive do for Haskell. In Haskell, pages 29--37, 2002. Google ScholarDigital Library
- R. Frost, R. Hafiz, and P. Callaghan. Parser combinators for ambiguous left-recursive grammars. In PADL, 2008. Google ScholarDigital Library
- J. E. Hopcroft, R. Motwani, and J. D. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley, 2003. Google ScholarDigital Library
- J. Hughes. Generalising monads to arrows. Sci. Comput. Program., 37(1--3):67--111, 2000. Google ScholarDigital Library
- N. R. Krishnaswami and N. Benton. A semantic model for graphical user interfaces. In ICFP, pages 45--57, 2011. Google ScholarDigital Library
- S. Lindley, P. Wadler, and J. Yallop. Idioms are oblivious, arrows are meticulous, monads are promiscuous. In MSFP, pages 97--117, 2008. Google ScholarDigital Library
- P. Ljunglöf. Pure functional parsing - an advanced tutorial. Master's thesis, Chalmers, 2002.Google Scholar
- C. McBride. Faking it: Simulating dependent types in Haskell. J. Funct. Program., 12(4--5):375--392, 2002. Google ScholarDigital Library
- C. McBride and R. Paterson. Applicative programming with effects. J. Funct. Program., 18:1--13, January 2008. Google ScholarDigital Library
- M. Might, D. Darais, and D. Spiewak. Parsing with derivatives: a functional pearl. In ICFP, pages 189--195, 2011. Google ScholarDigital Library
- B. C. Oliveira and W. R. Cook. Functional programming with structured graphs. In ICFP, pages 77--88, 2012. Google ScholarDigital Library
- B. C. Oliveira and A. Löh. Abstract syntax graphs for domain specific languages. In PEPM, 2013. Google ScholarDigital Library
- R. Paterson. A new notation for arrows. In ICFP, pages 229--240, 2001. Google ScholarDigital Library
- J. Peterson, P. Hudak, and C. Elliott. Lambda in Motion: Controlling Robots with Haskell. In PADL, pages 91--105, 1999. Google ScholarDigital Library
- S. Peyton Jones, D. Vytiniotis, S. Weirich, and G. Washburn. Simple unification-based type inference for GADTs. In ICFP, pages 50--61, 2006. Google ScholarDigital Library
- M. Sulzmann, M. M. T. Chakravarty, S. P. Jones, and K. Donnelly. System F with type equality coercions. In TLDI, pages 53--66, 2007. Google ScholarDigital Library
- S. D. Swierstra and L. Duponcheel. Deterministic, error-correcting combinator parsing. In AFP, pages 184--207, 1996. Google ScholarDigital Library
- J. Voigtl\"ander. Free theorems involving type constructor classes: functional pearl. In ICFP, pages 173--184, 2009.Google Scholar
- D. Vytiniotis, S. Peyton Jones, T. Schrijvers, and M. Sulzmann. OutsideIn (X) Modular type inference with local assumptions. J. Funct. Program., 1(1):1--80, 2011. Google ScholarDigital Library
- P. Wadler. Theorems for free! In FPLCA, pages 347--359, 1989. Google ScholarDigital Library
- G. Washburn and S. Weirich. Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. In ICFP, pages 249--262, 2003. Google ScholarDigital Library
- G. Winskel. The formal semantics of programming languages: an introduction. MIT Press, 1993. Google ScholarDigital Library
Index Terms
Fixing idioms: a recursion primitive for applicative DSLs
Recommendations
Desugaring Haskell's do-notation into applicative operations
Haskell '16Monads have taken the world by storm, and are supported by do-notation (at least in Haskell). Programmers are increasingly waking up to the usefulness and ubiquity of Applicatives, but they have so far been hampered by the absence of supporting ...
Idioms are Oblivious, Arrows are Meticulous, Monads are Promiscuous
We revisit the connection between three notions of computation: Moggi s monads, Hughes s arrows and McBride and Paterson s idioms (also called applicative functors). We show that idioms are equivalent to arrows that satisfy the type isomorphism A B 1 (A ...
Desugaring Haskell's do-notation into applicative operations
Haskell 2016: Proceedings of the 9th International Symposium on HaskellMonads have taken the world by storm, and are supported by do-notation (at least in Haskell). Programmers are increasingly waking up to the usefulness and ubiquity of Applicatives, but they have so far been hampered by the absence of supporting ...
Comments