Algorithm W using recursion schemes

Question

I wanted to be able to formulate the hindley-milner type inference algorithm using fix-point data types and recursion schemes. Disregarding all detail apart from the actual recursion parts:

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)
    ...

The algorithm builds an environment data structure env as it recursively traverses the tree until it reaches the leafs. Then it uses this information as it builds up the result again.

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

Answer 1

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

What you're looking for is a chronomorphism. This allows you to do recursion using both results from the future and the past. It's not quite as user-friendly as it sounds, but it is the canonical way of doing things using recursion schemes.

Answer 2

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

– luqui

Yes, but you'll probably need to use cata with a higher-order carrier type, computing an action that can modify the environment and possibly fail.

– pigworker