de Bruijn playground

dbp.hs

{-# LANGUAGE GADTs #-}

{-

Consider the standard "finally tagless" de Bruijn encoded lambda
calculus.

-}

class Db r where
  z   :: r (a, h) a
  s   :: r h a -> r (any, h) a
  con_ :: a -> r h a
  lam_ :: r (a, h) b -> r h (a -> b)
  app_ :: r h (a -> b) -> (r h a -> r h b)

{-

And it's evaluator

-}

newtype R h a = R (h -> a)
instance Db R where
  z                = R fst
  s (R z)          = R (z . snd)
  con_ a           = R (const a)
  lam_ (R f)       = R (\h a -> f (a, h))
  app_ (R f) (R a) = R (\h -> f h $ a h)

{-

What's interesting is that `z`, `s`, `con`, and `lam` each aren't much
more than a way of manipulating the environment to get an answer. If
we extend our class to include those mechanisms what do we get?

-}

class Dbi r where
  inj'  :: (h -> a) -> r h a
  lmap' :: (h' -> h) -> r h a -> r h' a

  -- lam is the most weird: we need to give a signature for (,) which
  -- takes an a value and lmaps the environment
  lam' :: (a -> (h' -> h)) -> r h b -> r h' (a -> b)
  app' :: r h (a -> b) -> (r h a -> r h b)

iz :: Dbi r => r (a, h) a
iz = inj' fst

is :: Dbi r => r h a -> r (any, h) a
is = lmap' snd

icon :: Dbi r => a -> r h a
icon = inj' . const

ilam :: Dbi r => r (a, h) b -> r h (a -> b)
ilam = lam' (,)

{-

So we are able to use this new Dbi basis to eliminate the notion of
carrying the environment via pairs. My original goal with this
construction was to be able to build more complex environments that
get passed around on the left side without making the types enormous.

But the `lmap'` name is suggestive. Can we get an `rmap` too and begin
to think of Dbi as being a Profunctor?

-}

class Profunctor p where
  dimap :: (i' -> i) -> (o -> o') -> (p i o -> p i' o')
  dimap f g = rmap g . lmap f
  rmap :: (o -> o') -> p i o -> p i o'
  rmap = dimap id
  lmap :: (i' -> i) -> p i o' -> p i' o'
  lmap f = dimap f id

class Profunctor r => Dbp r where
  inj :: (i -> o) -> r i o
  lam :: (a -> (i -> i')) -> (r i' b -> r i (a -> b))
  app :: r i (a -> b) -> (r i a -> r i b)

pz :: Dbp r => r (a, h) a
pz = inj fst

ps :: Dbp r => r h a -> r (any, h) a
ps = lmap snd

plam :: Dbp r => r (a, i) b -> r i (a -> b)
plam = lam (,)

pcon :: Dbp r => o -> r i o
pcon = inj . const

{-

If we try to build a model of Dbp we end up with something
interesting---we have to introduce a new type constructor to make the
obvious model a Profunctor

-}

data E h a where
  M    :: (h' -> h) -> E h a -> E h' a
  I    :: (h -> a) -> E h a
  Lam  :: (a -> h' -> h) -> E h b -> E h' (a -> b)
  App  :: E h (a -> b) -> E h a -> E h b
  Loop :: E i o -> E (a -> i) (a -> o)

instance Functor (E h) where
  fmap = rmap

instance Profunctor E where
  dimap f g e = case e of
    M q h     -> M (q . f) (rmap g h)
    I q       -> I (g . q . f)
    Lam q e   -> dimap (flip q . f) g (Loop e)
    App ef ea -> App (dimap f (g .) ef) (dimap f id ea)

instance Dbp E where
  inj = I
  lam = Lam
  app = App

{-

Evaluation of the Loop constructor works without much trouble

-}

eval :: E h a -> h -> a
eval e0 h = case e0 of
  M f e   -> eval e (f h)
  I f     -> f h
  Lam c e -> \a -> eval e (c a h)
  App f a -> eval f h $ eval a h
  Loop f  -> \a -> eval f (h a)

{-

But it's really unclear what this construction means. I think it'll
serve my purposes, though.

-}