W algorithm using recursion schemes

Question

I wanted to be able to formulate an hindley-milner type inference algorithm using fixed-point data types and recursion schemes. Excluding all details except the actual parts of the recursion:

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

The algorithm builds the data structure of the env environment as it recursively traverses the tree until it reaches the leaves. He then uses this information as he creates the result again.

Without the env part, this can be easily implemented using cata . Can this (with env ) be done in the general case using recursion schemes?

Answer 1

Without the env part, this can be easily implemented using cata. Could this (with env) be done as a whole using recursive schemas?

What you are looking for is chronomorphism . This allows recursion using both results from the future and the past. It is not quite as convenient as it sounds, but it is a canonical way of doing things using recursion schemes.

Answer 2

Yes, just make the cata target of the Env -> a function Env -> a

- luqui

Yes, but you may have to use cata with a higher carrier type, calculating an action that can change the environment and possibly fail.

- pig farmer