Podcasts Technology Iowa Type Theory Commute The Mendler encoding and the problem of explicit recursion

The Mendler encoding and the problem of explicit recursion

Published: Feb. 25, 2020, 9 p.m.

b'

The Church encoding allows definition of certain recursive functions, but all the recursive calls are implicit.\\xa0 The encoding simply presents you with the results of recursion for all immediate subdata.\\xa0 Using a technique due to Mendler, an encoding is possible where recursions are explicitly made by the combining functions given to the data.

'