Functional pearl: Folding polynomials of polynomials

Polynomials are a central concept to many branches in mathematics and computer science. In particular, manipulation of polynomial expressions can be used to model a wide variety of computation. In this paper, we consider a simple recursive construction of multivariate polynomials over a base ring such as the integers or a (finite) field. We show that this construction allows inductive implementation of polynomial operations such as arithmetic, evaluation, substitution, etc. Furthermore, we can transform a polynomial expression into in a sequence of arithmetic expressions in the base ring and prove the correctness of this transformation in Agda. Combined with our recursive construction, this allows for compiling polynomial expressions over a tower of extension fields into scalar expressions over the ground field, for example. Such a technique is not only interesting in its own right but also finds plentiful application in research areas such as cryptography.