Lambda calculus with de Bruijn representation in tagless-final style

stlc.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
-- Tuesday, September 15, 2020 at 16:20
-- Lambda calculus with de Bruijn representation in tagless-final
-- style

-- Just so that we can write repr γ ⊢ a -> repr γ ⊢ b, etc.
infix 3 ⊢
type a ⊢ b = a b

class Lam repr where
  int :: Int
         ------------
      -> repr γ ⊢ Int
      
  add :: repr γ ⊢ Int
      -> repr γ ⊢ Int
         ------------
      -> repr γ ⊢ Int
  
  z   ::
         --------------
         repr (γ,α) ⊢ α
  
  s   :: repr γ      ⊢ β
         ---------------
      -> repr (γ, α) ⊢ β
    
  lam :: repr (γ, α) ⊢ β
         -----------------
      -> repr γ ⊢ (α -> β)

  app :: repr γ ⊢ (α -> β)
      -> repr γ ⊢ α
         -----------------
      -> repr γ ⊢ β
  

ex1 = add (int 1) (int 2)
ex2 = lam (add z (s z))

newtype R g a = R { unR :: g -> a }

instance Lam R where
  z = R snd
  s (R v) = R (\(g,a) -> v g)
  int i = R (pure i)
  add (R x) (R y) = R ((+) <$> x <*> y)
  lam (R f) = R (curry f)
  app (R f) (R x) = R (f <*> x)

eval e = unR e ()