Fegaras.hs

{-# language RankNTypes #-}
{-# language BlockArguments #-}
{-# language LambdaCase #-}
{-# language TypeOperators #-}
{-# language GADTs #-}
{-# language MultiParamTypeClasses #-}
{-# language FlexibleInstances #-}
{-# language FunctionalDependencies #-}
{-# language UndecidableInstances #-}

class Lam f where
  lam :: (f a -> f b) -> f (a -> b)
  app :: f (a -> b) -> f a -> f b
  int :: Int -> f Int
  add :: f Int -> f Int -> f Int

newtype Eval a = Eval { eval :: a }

instance Lam Eval where
  lam f = Eval (eval . f . Eval)
  app f = Eval . eval f . eval
  int = Eval
  add (Eval x) (Eval y) = Eval (x + y)

type f ~> g = forall i. f i -> g i
infixr 0 ~>

-- initial encoding of one layer, our indexed base "functor"
data F r a where
  Lam :: (r a -> r b) -> F r (a -> b)
  App :: r (a -> b) -> r a -> F r b
  Int :: Int -> F r Int
  Add :: r Int -> r Int -> F r Int

step :: Lam r => F r ~> r
step (Lam h) = lam h
step (App y z) = app y z
step (Int i) = int i
step (Add y z) = add y z

xmap :: (r ~> s) -> (s ~> r) -> (F r ~> F s)
xmap f g = \case
  Lam h -> Lam (f . h . g)
  App y z -> App (f y) (f z)
  Int i -> Int i
  Add y z -> Add (f y) (f z)

-- free indexed monad over our base functor
newtype E r a = E { runE :: (F r ~> r) -> r a }

roll :: F (E r) ~> E r
roll x = E \k -> k (xmap (cata k) place x)

instance Lam (E r) where
  app y z = roll (App y z)
  lam f = roll (Lam f)
  add f g = roll (Add f g) 
  int i = roll (Int i)

-- fegaras-sheard catamorphism
cata :: (F r ~> r) -> E r ~> r
cata f x = runE x f

-- fegaras-sheard place operator, indexed monad return
--
-- @cata f . place = id@
place :: r ~> E r
place x = E \_ -> x

-- indexed monad join
join :: E (E r) ~> E r
join x = runE x roll

class Iterable r m n | m -> r, n -> r where
  openiter :: (F r ~> r) -> m -> n
  uniter :: (F r ~> r) -> n -> m

instance Iterable r (E r a) (r a) where
  openiter f x = cata f x
  uniter f = place

instance (Iterable r m n, Iterable r m' n') => Iterable r (m -> m') (n -> n') where
  openiter f x = openiter f . x . uniter f
  uniter f x = uniter f . x . openiter f

iter0 :: (F r ~> r) -> (forall s. E s a) -> r a
iter0 f x = cata f x

iter1 :: (F r ~> r) -> (forall s. E s a -> E s b) -> r a -> r b
iter1 = openiter

compile :: Lam r => E r ~> r
compile = cata step

compile1 :: Lam r => (forall s. E s a -> E s b) -> r a -> r b
compile1 = openiter step