de Bruijn indicies that don't suck

bound.hs

import Data.List

import Data.Foldable
import Data.Traversable
import Control.Applicative
import Control.Monad (ap)

import Prelude.Extras
import Bound

data E a
  = V a
  | E a :@ E a
  | Lam (Scope () E a)
  | Let [Scope Int E a] (Scope Int E a)
  deriving (Eq, Ord, Show, Read)
infixl 9 :@

--------------------------------------------------------------------------------
-- Instance bonanza

instance Functor E  where fmap    = fmapDefault
instance Foldable E where foldMap = foldMapDefault

instance Applicative E where
  pure  = V
  (<*>) = ap

instance Traversable E where
  traverse f (V a)      = V <$> f a
  traverse f (x :@ y)   = (:@) <$> traverse f x <*> traverse f y
  traverse f (Lam e)    = Lam <$> traverse f e
  traverse f (Let bs b) = Let <$> traverse (traverse f) bs <*> traverse f b

instance Monad E where
  return x       = V x
  V a      >>= f = f a
  (x :@ y) >>= f = (x >>= f) :@ (y >>= f)
  Lam e    >>= f = Lam (e >>>= f)
  Let bs b >>= f = Let (map (>>>= f) bs) (b >>>= f)
  
instance Eq1   E where (==#)      = (==)
instance Ord1  E where compare1   = compare
instance Show1 E where showsPrec1 = showsPrec
instance Read1 E where readsPrec1 = readsPrec

--------------------------------------------------------------------------------
-- Smart constructors

lam :: Eq a => a -> E a -> E a
lam v e = Lam (abstract1 v e)

infixr 0 !
(!) :: Eq a => a -> E a -> E a
(!) = lam

let_ :: Eq a => [(a, E a)] -> E a -> E a
let_ [] b = b
let_ bs b = Let (map (abstr . snd) bs) (abstr b)
  where abstr = abstract (`elemIndex` map fst bs)

--------------------------------------------------------------------------------
-- Evaluation

whnf :: E a -> E a
whnf e@V{}    = e
whnf e@Lam{}  = e
whnf (f :@ a) = case whnf f of
  Lam b -> whnf (instantiate1 a b)
  f' -> f' :@ a
whnf (Let bs b) = whnf (inst b)
  where es = map inst bs
        inst = instantiate (es !!)

--------------------------------------------------------------------------------
-- Examples

true, true' :: E String
true  = lam "F" (lam "T" (V "T"))
true' = "F" ! ("T" ! V "T")