“Fuzzing” is a popular testing approach where we throw random inputs at a program and check that it respects some expected properties on all inputs. Fuzzing a metaprogram such as a compiler requires producing random input programs. To exercise interesting behaviors of the compiler, we want our input programs to be well-formed in a strong sense, in particular to be well-typed. Generating random well-typed program is difficult when the type-system is powerful, there is a whole scientific literature on the topic, see for example [Testing an Optimising Compiler by Generating Random Lambda Terms, Pałka, 2012].

Most existing generators integrate a large part of the implementation of a type-checker, “inverted” to assist in top-down random term generation by efficiently discarding choices that result in ill-typed programs. Scaling this approach to a full language would result in implementing two sophisticated type-checkers, once in the compiler and once in the program generator. This is one type-checker too many!

We present preliminary work on reusing the constraint-based type inference approach [The Essence of ML-based type inference, Pottier and Rémy, 2004] to write a single type-checker that can be used for both purposes: to check types of user-provided programs, and to efficiently guide a random program generator. This only requires a fairly simple modification to constraint generators: parametrizing them over a search monad. We have succesfully implemented a generator of simply-typed terms in this style, and are in the process (almost done) of scaling it to Hindley-Milner type inference.

(Relevant previous work is [Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System, Fetscher, Claessen, Pałka, Hughes, Findler]. They start from Redex, a Racket DSL to implement simple type systems, and derive a random program generator. The limitation of this approach is that Redex only works with fairly simple type system, in particular we do not expect it to scale to ML-style type inference with polymorphism, which is the part that hand-crafted generators also struggle on.)

Author note: we are submitting due to the signals we received that TyDe is struggling to attract submissions this year, possibly due to the remote conference location. We would present remotely if accepted. The topic is arguably peripheral for TyDe, and the idea of giving a remote talk at 8am Paris time on a Sunday morning is only moderately exciting, so we would encourage the PC to consider this as an “if need be” submission: do not hesitate to reject us if you have a nice programme otherwise. Thanks for your work for TyDe!