bound.idr

%default total

interface Bifunctor (f : Type -> Type -> Type) where
  bimap : (a -> b) -> (c -> d) -> f a c -> f b d

  first : (a -> b) -> f a c -> f b c
  first f = bimap f id

  second : (a -> b) -> f c a -> f c b
  second = bimap id

data V : (b : Type) -> (f : Type) -> Type where
  B : (bound : b) -> V b f
  F : (free  : f) -> V b f

Bifunctor V where
  bimap f g (B bound) = B (f bound)
  bimap f g (F free)  = F (g free)

Functor (V b) where
  map = second

Applicative (V b) where
  pure = F
  (B bound) <*> _ = B bound
  (F free)  <*> v = map free v

data Scope : (b : Type) -> (f : Type -> Type) -> (a : Type) -> Type where
  S : f (V b (f a)) -> Scope b f a

data Expr : (v : Type) -> Type where
  Var : v -> Expr v
  App : (e1 : Expr v) -> (e2 : Expr v) -> Expr v
  Lam : (s : Scope () Expr v) -> Expr v

data Compose : f -> g -> a -> Type where
  C : f (g a) -> Compose f g a

getCompose : Compose f g a -> f (g a)
getCompose (C c) = c

(Functor f, Functor g) => Functor (Compose f g) where
  map f (C x) = C (map (map f) x)

(Applicative f, Applicative g) => Applicative (Compose f g) where
  pure x = C (pure (pure x))
  (C f) <*> (C x) = C ((<*>) <$> f <*> x)

lift : Applicative f => Applicative g
  => f (g (a -> b))
  -> f (g a)
  -> f (g b)
lift {f} {g} x y =
  let cx : (Compose f g) _ = C x
      cy : (Compose f g) _ = C y
  in getCompose (cx <*> cy)

lifty : Applicative f => Applicative g
  => f (g (f (a -> b)))
  -> f (g (f a))
  -> f (g (f b))
lifty {f} {g} x y =
  let cx : Compose (Compose f g) f _ = C (C x)
      cy : Compose (Compose f g) f _ = C (C y)
  in getCompose (getCompose (cx <*> cy))


mutual
  Functor f => Functor (Scope b f) where
    map f (S a) = S (map (map (map f)) a)

  partial
  expr_map : (v -> w) -> Expr v -> Expr w
  expr_map f (Var x)     = (Var (f x))
  expr_map f (App e1 e2) = App (expr_map f e1) (expr_map f e2)
  expr_map f (Lam s)     = Lam (map f s)

  Functor Expr where
    map = assert_total expr_map

  Applicative f => Applicative (Scope b f) where
    pure a = S (pure (F (pure a)))
    (S a1) <*> (S a2) = S (lifty a1 a2)

  partial
  expr_app : Expr (v -> w) -> Expr v -> Expr w
  expr_app (Var x)     e2 = map x e2
  expr_app (App x y)   e2 = App (expr_app x e2) (expr_app y e2)
  expr_app (Lam (S s)) e2 = Lam (S (lifty s (map (F . Var) e2)))

  partial
  Applicative Expr where
    pure = Var
    (<*>) = assert_total expr_app

  bind : Monad f => Scope b f a -> (a -> f c) -> Scope b f c
  bind (S s) f = S (liftA (map (>>= f)) s)

  partial
  expr_bind : Expr v -> (v -> Expr w) -> Expr w
  expr_bind (Var x)     f = f x
  expr_bind (App e1 e2) f = App (expr_bind e1 f) (expr_bind e2 f)
  expr_bind (Lam s)     f = Lam (bind s f)

  partial
  Monad Expr where
    (>>=) = assert_total expr_bind

e1 : Expr String
e1 = App (Var "x") (Var "y")

e2 : Expr String
e2 = do
  x <- e1
  pure $ case x of
    "x" => "y"
    "y" => "x"
    _   => x

abs : Eq v => v -> Expr v -> Scope () Expr v
abs v e = S $ e >>= \x => Var $ if x == v then B () else F (Var v)

lam : Eq v => v -> Expr v -> Expr v
lam v e = Lam (abs v e)

e3 : Expr String
e3 = lam "x" e1

e4 : Expr String
e4 = do
  x <- e3
  pure $ case x of
    "x" => "y"
    "y" => "x"
    _   => x

inst : Scope () Expr String -> String -> Expr String
inst (S s) v = s >>= \x => case x of
  F (Var f) => Var $ if v == f then f ++ "_lolol" else f
  F f => f
  B b => Var v


e5 : Expr String
e5 = case e4 of
  Lam s => inst s "y"