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?

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
– pigworker, Commented Sep 8, 2017 at 23:55
@user47376 something about it feels a bit magical, doesn't it? — luqui
– luqui, Commented Sep 9, 2017 at 1:52

score 3 · Accepted Answer · 2017-09-09 04:11:34Z

3

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.

edited Sep 9, 2017 at 4:11

answered Sep 9, 2017 at 4:04

user8174234

Sign up to request clarification or add additional context in comments.

Comments

dfeuer · Accepted Answer · 2017-09-09 03:22:10Z

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

answered Sep 9, 2017 at 3:22

community wiki

dfeuer

1 Comment

pigworker Over a year ago

Now write algorithm W as a tail-recursive traversal using the same data structure as both the zipper and the environment of unification variables. You'll be glad you did.

Collectives™ on Stack Overflow

Algorithm W using recursion schemes

2 Answers 2

Comments

1 Comment

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

2 Answers 2

Comments

1 Comment

Your Answer

Sign up or log in

Post as a guest

Related