deep-econom (deep_econom) wrote,
deep-econom
deep_econom

ссылка на память

---
Cedille: Полиморфное лямбда-исчисление с выводимой индукцией
https://akuklev.livejournal.com/1271526.html
Некоторое время назад Aaron Stump сотоварищи предложил интересный вариант полиморфного лямбда-исчисления, где существуют кодировки широчайшего класса индуктивных типов данных, для которых выводима индукция. В этом посте я хотел обрисовать идеи его подхода.

Стартовой точкой подхода Стумпа является наблюдение (сделанное не им, и очень давно), что термы, реализующие рекурсию, и термы реализующие индукцию, после стирания ти́повых аннотаций (англ. erasure), становятся одинаковыми.

Давайте начнём с натуральных чисел и рекурсии. Пусть у нас есть функция f : Nat ⟶ Nat. Как будет выглядеть функция высшего порядка, которая повторяет наше f n раз?
---
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic
  • 0 comments