CODEWITHSUNDEEP
haskellrecursiontype-inferencehindley-milnerrecursion-schemes
user47376
user47376

Reputation: 2273

Algorithm W using recursion schemes

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?

Upvotes: 6

Views: 439

Answers (2)

user8174234
user8174234

Reputation:

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.

Upvotes: 3

dfeuer
dfeuer

Reputation: 48631

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

Upvotes: 2

Related Questions