\begin{code}
module Syntax (Type(..), Func(..), Term(..), etaReduce) where

import Control.Monad.State


data Type = Alpha | Bool | Int | List Type | Maybe Type | Type `To` Type

data Func v  =  Id | Map String (Func v) | Lambda (v -> Func v) | Func v `Comp` Func v
             |  Embed v

data Term v = Const String | Var v | Term v `Apply` Term v | Lambda' (v -> Term v)


etaReduce :: Term String -> Term String
etaReduce t = evalState (go t) ['*':show n | n <- [1..]]
  where  go t@(Const _)    = return t
         go t@(Var _)      = return t
         go (f `Apply` t)  = liftM2 Apply (go f) (go t)
         go (Lambda' f)    = do  vars <- get
                                 let  v   = head vars
                                      vs  = tail vars
                                 put vs
                                 body <- go (f v)
                                 case body of
                                   t `Apply` Var v' |  not (freeVar v t) && v' == v
                                                       -> return t
                                   _ -> return (Lambda' (\v -> evalState (go (f v)) vs))

         freeVar _  (Const _)      = False
         freeVar v  (Var v')       = v' == v
         freeVar v  (f `Apply` t)  = freeVar v f || freeVar v t
         freeVar v  (Lambda' f)    = freeVar v (f "")
\end{code}