EPISODE · May 19, 2020 · 10 MIN
Mendler-style iteration
from Iowa Type Theory Commute · host 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.
What this episode covers
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...
NOW PLAYING
Mendler-style iteration
No transcript for this episode yet
Similar Episodes
Mar 4, 2026 ·7m
Feb 22, 2026 ·9m
Feb 8, 2026 ·11m
Feb 2, 2026 ·12m
Jan 30, 2026 ·31m
Jan 29, 2026 ·39m