On Type-directed Generation of Lambda Terms
Paul Tarau · International Conference on Lightning Protection · 2015
We describe a Prolog-based combined lambda term generator and type-inferrer for closed well-typed terms of a given size, in de Bruijn notation. By taking advantage of Prolog’s unique bidirectional execution model and sound unification algorithm, our generator can build “customized” closed terms of a given type. This relational view of terms and their types enables the discovery of interesting patterns about frequently used type expressions occurring in well-typed functional programs. Our study uncovers the most “popular” types that govern function applications among a about a million small-sized lambda terms and hints toward practical uses to combinatorial software testing. It also shows the effectiveness of Prolog as a meta-language for modeling properties of lambda terms and their types.