Abstract
We use generic programming techniques to generate well-typed lambda terms. We encode well-typed terms by means of generalized algebraic datatypes (GADTs) and existential types. The Spine approach to generic programming supports GADTs, but it does not support the definition of generic producers for existentials. We describe how to extend the Spine approach to support existentials and we use the improved Spine to define a generic enumeration function. We show that the enumeration function can be used to generate the terms of simply typed lambda calculus.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Augustsson, L.: Announcing Djinn, version 2004-12-11, a coding wizard (2005), http://permalink.gmane.org/gmane.comp.lang.haskell.general/12747
Benke, M., Dybjer, P., Jansson, P.: Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing 10(4), 265–289 (2003)
Cheney, J., Hinze, R.: First-class phantom types. Technical report, Cornell University (2003)
Claessen, K., Hughes, J.: QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In: ICFP 2000, pp. 286–279 (2000)
Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. The Journal of Symbolic Logic 57(3), 795–807 (1992)
Hinze, R., Löh, A.: “Scrap Your Boilerplate” revolutions. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 180–208. Springer, Heidelberg (2006)
Hinze, R., Löh, A., Oliveira, B.C.d.S.: “Scrap your boilerplate” reloaded. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol. 3945, pp. 13–29. Springer, Heidelberg (2006)
Katayama, S.: Systematic search for lambda expressions. In: TFP 2005 (2005)
Koopman, P., Alimarine, A., Tretmans, J., Plasmeijer, R.: Gast: Generic automated software testing. In: Peña, R., Arts, T. (eds.) IFL 2002. LNCS, vol. 2670. Springer, Heidelberg (2003)
Koopman, P., Plasmeijer, R.: Systematic synthesis of λ-terms. In: Essays dedicated to Henk Barendregt on the Occasion of his 60th Birthday (2007)
Lämmel, R., Jones, S.P.: Scrap your boilerplate: A practical design pattern for generic programming. In: TLDI 2003, pp. 26–37 (2003)
Morris, P.: Constructing Universes for Generic Programming. PhD thesis, The University of Nottingham (2007)
Peyton Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: ICFP 2006, pp. 50–61 (2006)
Spivey, M.: Combinators for breadth-first search. Journal of Functional Programming 10(4), 397–408 (2000)
Weirich, S.: Higher-order intensional type analysis. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 98–114. Springer, Heidelberg (2002)
Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: POPL 2003, pp. 224–235 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rodriguez Yakushev, A., Jeuring, J. (2010). Enumerating Well-Typed Terms Generically. In: Schmid, U., Kitzelmann, E., Plasmeijer, R. (eds) Approaches and Applications of Inductive Programming. AAIP 2009. Lecture Notes in Computer Science, vol 5812. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11931-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-11931-6_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11930-9
Online ISBN: 978-3-642-11931-6
eBook Packages: Computer ScienceComputer Science (R0)