Mendler-style iteration
from Iowa Type Theory Commute Hosted by Aaron Stump
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.
Embed this episode
No transcript yet.