Algorithm to derive generic functions

Example

Implement the bind operation for the Continuation monad

1
2
3
newtype Cont r a = Cont { runCont :: (a -> r) -> r }

(>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b

 

Question

1
2
3
4
(>>=) m f = x1
m  :: (a -> r) -> r
f  :: a -> (b -> r) -> r
x1 :: (b -> r) -> r

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 ?

x1 from ctx -> YES / NO

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

1
2
3
4
x1 from funapp
    candidate   "x1 = f x2 x3"      x2 :: a        x3 :: b -> r
    x2 from ctx -> YES / NO
    (...)

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

1
2
3
4
-- if x1 :: (b -> r) -> r
x1 from lambda    "x1 = \l -> x2"   x2 :: r     l :: b -> r
    x2 from ctx -> YES / NO
(...)

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:

-- Problem:
-- How do we implement (>>) ?
newtype Cont r a = Cont { runCont :: (a -> r) -> r }
(>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b

-- ctx contains:
--      f  :: a -> (b -> r) -> r
--      m  :: (a -> r) -> r
-- and we're looking for:
--      x1 :: (b -> r) -> r

x1 from ctx -> NO
x1 from funapp
     candidate    "f x2"            x2 :: a
     x2 from ctx    -> NO
     x2 from funapp -> NO
     => NO
x1 from lambda    "x1 = \l -> x2"            x2 :: r        l :: b -> r
    x2 from ctx -> NO
    x2 from funapp
         candidate    "x2 = f x3 x4"        x3 :: a        x4 :: b -> r
         x3 from ctx    -> NO
         x3 from funapp -> NO
         => NO
         candidate    "x2 = m x3"            x3 :: a -> r
         x3 from ctx    -> NO
         x3 from funapp -> NO
         x3 from lambda    "x3 = \g -> x4"        x4 :: r        g :: a
             x4 from ctx -> NO
             x4 from funapp
                  candidate    "x4 = f x5 x6"        x5 :: a        x6 :: b -> r
                 
                  -- ctx contains:
                  --      f  :: a -> (b -> r) -> r
                  --      m  :: (a -> r) -> r
                  --      l :: b -> r
                  --      g :: a
                  -- and we're looking for:
                  --      x5 :: a
                  --      x6 :: b -> r
                  -- we can then find the solution using:
                  --      x4 = f x5 x6
                  --      x3 = \g -> x4
                  --      x2 = m x3
                  --      x1 = \l -> x2
                 
                  x5 from ctx -> YES    x5 = g
                  x6 from ctx -> YES    x6 = l
                  => YES
         => YES

===>

x4 = f g l
x3 = \g -> f g l
x2 = m (\g -> f g l)
x1 = \l -> m (\g -> f g l)

Result:

1
2
3
4
newtype Cont r a = Cont { runCont :: (a -> r) -> r }

(>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b
(>>=) m f = \l -> m (\g -> f g l)
Edit
Pub: 09 Apr 2023 05:05 UTC
Views: 50