Skip to content

Instantly share code, notes, and snippets.

@cls cls/debruijn.hs
Last active Oct 21, 2017

Embed
What would you like to do?
Untyped lambda calculus with De Bruijn indices as a nested data type
import Control.Applicative (liftA2)
data Term a = App (Term a) (Term a)
| Lam (Term (Maybe a))
| Var a
instance Functor Term where
fmap f (App s t) = App (fmap f s) (fmap f t)
fmap f (Lam t) = Lam (fmap (fmap f) t)
fmap f (Var x) = Var (f x)
instance Applicative Term where
App s t <*> u = App (s <*> u) (t <*> u)
Lam t <*> u = Lam (liftA2 (<*>) t (fmap pure u))
Var x <*> u = fmap x u
pure = Var
instance Monad Term where
App s t >>= f = App (s >>= f) (t >>= f)
Lam t >>= f = Lam (t >>= traverse f)
Var x >>= f = f x
data Void
type ClosedTerm = Term Void
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.