Start / Iowa Type Theory Commute / Mendler style iteration

Mendler-style iteration

11 min • 19 maj 2020

Another type-based approach to termination-checking for recursive functions over inductive datatypes is to use so-called Mendler-style iteration. On this approach, we write recursive functions by coding against a certain interface that features an abstract type R, which abstracts the datatype over which we are recursing; and a function from R to the result type of the recursion. Subdata of the input data are available at type R only, not at the original datatype. This allows us to make explicit recursive calls, but only on subdata.