Oleg.hs

{-  That makes a lot of sense indeed. And the code becomes easier to
understand. Your original code is perhaps too advanced for this
task. I'm sending the simplified verison, requiring no extensions. It
is also easier to relate to the familiar De Bruijn indices, so it
should be easier to explain.  -}

module DBL1 where

import           Prelude hiding ((/))

-- Take the state s focused on a and return the state t with a replaced by b
-- In other words, replace a with b deep inside s and return the resulting t
-- If we also want to extract, we should pair the below with the function
-- (s->a) or (t->b), as desired
type Lens s t a b = (a->b) -> s->t

lz :: Lens a b a b
lz f s = f s                            -- the I combinator

ls :: Lens s t a b -> Lens (x,s) (x,t) a b
ls l = \f -> \ (x,s) -> (x,l f s)

n0 = lz
n1 = ls n0
n2 = ls n1

-- variables: the same as with De Bruijn indices
v0 :: (a,x) -> a
v0 (x,_) = x

vs :: (s -> a) -> ((x,s) -> a)
vs v = \ (_,s) -> v s

v1 = vs v0
v2 = vs v1

-- application
-- This is the S combinator (pretty understandable, for the env passing)

(/) :: (s -> a -> b) -> (s -> a) -> s -> b
(f / x) s = f s (x s)

-- abstraction

deposit :: Lens s t () (a,()) -> a -> s -> t
deposit n a = n (\ () -> (a,()))

lam :: Lens s t () (a,()) -> (t -> t') -> s -> a -> t'
lam n phi = \s x -> phi (deposit n x s)

-- examples, as before

ex1 :: (a,()) -> (a -> b -> c) -> b -> c
ex1 = lam n1 $ lam n2 (v1 / v0 / v2)

ex2 :: () -> a -> (a -> b -> c) -> b -> c
ex2 = lam n0 ex1

-- ex3 = lam n0 v1
-- type error: lam n0 presupposes that the context is 0 levels deep
-- v n1 presupposes that the context is 1 level deep

ex4 :: (a,()) -> b -> b
ex4 = lam n1 v1 / lam n1 v1

-- ex5 = lam n1 v1 / lam n2 v1
-- type error: lam n1 and lam n2 presuppose incompatible things about the
-- depth of the context

ex6 :: () -> a -> b -> (a -> c) -> c
ex6 = lam n0 (lam n1 (lam n2 (v2 / v0)))

ex7 :: () -> (a -> b) -> a -> b
ex7 = lam n0 (lam n1 ((lam n2 v2) / (v0 / v1)))