Skip to content

Instantly share code, notes, and snippets.

@thoughtpolice
Created December 30, 2012 09:13
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save thoughtpolice/4411745 to your computer and use it in GitHub Desktop.
Save thoughtpolice/4411745 to your computer and use it in GitHub Desktop.
de Bruijn indicies that don't suck
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")
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment