DBL.hs

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TupleSections #-}

module DBL where

import           Prelude hiding ((/))

-- indexed store coalgebra lenses

type Lens s t a b = s -> IStore a b t

data IStore a b t = IStore a (b -> t) deriving Functor

-- lensed indices

lz :: Lens a b a b
lz a = IStore a id

ls :: Lens s t a b -> Lens (y,s) (y,t) a b
ls n (y,s) = (y,) <$> n s

-- variables

v :: Lens s t (a,b) c -> s -> a
v n s = a where
  IStore (a,b) ct = n s

n0 = lz
n1 = ls n0
n2 = ls n1

-- application

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

-- abstraction

modify :: Lens s t a b -> (a -> b) -> s -> t
modify n f s = bt (f a) where
  IStore a bt = n s

deposit :: Lens s t () (a,()) -> a -> s -> t
deposit n a = modify n $ const (a, ())

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

-- examples

ex1 :: (a,()) -> (a -> b -> c) -> b -> c
ex1 = lam n1 $ lam n2 (v n1 / v n0 / v n2)

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

-- ex3 = lam n0 (v n1)
-- 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 (v n1) / lam n1 (v n1)

-- ex5 = lam n1 (v n1) / lam n2 (v n1)
-- 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 (v n2 / v n0)))

ex7 :: () -> (a -> b) -> a -> b
ex7 = lam n0 (lam n1 ((lam n2 (v n2)) / (v n0 / v n1)))