Cedille: Полиморфное лямбда-исчисление с выводимой индукцией
https://akuklev.livejournal.com/1271526.html
Некоторое время назад Aaron Stump сотоварищи предложил интересный вариант полиморфного лямбда-исчисления, где существуют кодировки широчайшего класса индуктивных типов данных, для которых выводима индукция. В этом посте я хотел обрисовать идеи его подхода.
Стартовой точкой подхода Стумпа является наблюдение (сделанное не им, и очень давно), что термы, реализующие рекурсию, и термы реализующие индукцию, после стирания ти́повых аннотаций (англ. erasure), становятся одинаковыми.
Давайте начнём с натуральных чисел и рекурсии. Пусть у нас есть функция f : Nat ⟶ Nat. Как будет выглядеть функция высшего порядка, которая повторяет наше f n раз?
---
