Алгоритм W с использованием рекурсивных схем

Question

Я хотел иметь возможность сформулировать алгоритм вывода типа Хиндли-Милнера, используя типы данных с фиксированной точкой и схемы рекурсии. Не обращая внимания на все детали, кроме реальных рекурсивных частей:

w env term = case term of 
    Lam n e -> lam (w (modify1 env) e)
    App a b -> app (w (modify2 env) a) (w (modify3 env) b)
    ...

Алгоритм строит структуру данных среды env поскольку это рекурсивно пересекает дерево, пока это не достигает листьев. Затем он использует эту информацию, поскольку создает результат снова.

Без env часть, это может быть легко реализовано с cata, Может это (с env) сделать вообще с использованием рекурсивных схем?

Answer 1

Без части env это можно легко реализовать с помощью cata. Можно ли это сделать (с помощью env) в целом, используя схемы рекурсии?

То, что вы ищете, это хрономорфизм. Это позволяет вам делать рекурсию, используя результаты из будущего и прошлого. Это не так удобно для пользователя, как кажется, но это канонический способ делать вещи, используя схемы рекурсии.

Answer 2

Да, просто сделать цель cata функция Env -> a

- Луки

Да, но вам, вероятно, придется использовать cata с типом носителя более высокого порядка, вычисление действия, которое может изменить среду и, возможно, потерпеть неудачу.

- свиновод