{-# LANGUAGE
MultiParamTypeClasses,
FunctionalDependencies,
NoMonomorphismRestriction #-}

-- Simply typed LC
class LAM1 r where
  lit1  ::  t -> r t
  app1  ::  r (a -> b)    ->  r a -> r b
  lam1  ::  (r a -> r b)  ->  r (a -> b)
  
-- One application is straightforward.
t1 l = app1 (lam1 $ \a -> a) (lit1 l)

-- Curried arguments of course need multiple lam1 constructors, and
-- app1 constructons at application site.
f1' = (lam1 $ \a -> (lam1 $ \b -> a))
t1' l = app1 (app1 f1' (lit1 l)) (lit1 l)
  

-- Simply typed LC with only tail calls.  This just limits the return
-- type of the expression, so is not so interesting.
class LAM2 x r | r -> x, x -> r where
  lit2  ::  t -> r t
  app2  ::  r (a -> x)    ->  r a -> r x
  lam2  ::  (r a -> r x)  ->  r (a -> x)
  ret2  ::  x -> r x


-- Monadic LC
class Monad m => LAM3 r m | r -> m where
  lit3  ::  t -> r t
  app3  ::  r (a -> m b)      ->  r a -> m (r b)
  lam3  ::  (r a -> m (r b))  ->  r (a -> m b)
  
fn3 = lam3 (\a -> return a)
t3 l = app3 fn3 (lit3 l)

-- I don't see how to do multiple arguments though..