Algorithm to derive generic functions
Example
Implement the bind operation for the Continuation monad
Question
How to we implement x1 in function of m and f ?
Algorithm
To resolve a variable (ie: x1) we try in this order:
1) from ctx
Is x1 already in the current context ?
2) from funapp
Can x1 be obtained by function application from the current context ?
For this to work, the context needs to have functions that return a value of x1's type. We then need to construct the arguments needed to return the right type. So we create new variables and recurse on those
3) from lambda
If x1 is a function type, can we implement it as a lambda ?
create a new variable for the result (ie: x2) and recurse on it
Notes
- step 1) can be considered a special case of step 2)
Application
This is the algorithm finding how to implement the bind operation for the continuation monad: