Language.Nominal.Examples.UntypedLambda

Untyped lambda-calculus: syntax, substitution, nominal-style recursion, weak head normal form function, and a couple of examples.

Compare with an example in the Bound package.

Documentation

type Var = Name String

Variables are string-labelled names

data Exp

Terms of the untyped lambda-calculus

Constructors

V Var

Variable

Exp :@ Exp infixl 9

Application

Lam (KAbs Var Exp)

Lambda, using abstraction-type

Instances

Eq Exp

Defined in Language.Nominal.Examples.UntypedLambda

Methods

(==) :: Exp -> Exp -> Bool

(/=) :: Exp -> Exp -> Bool

Data Exp

Defined in Language.Nominal.Examples.UntypedLambda

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Exp -> c Exp

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Exp

toConstr :: Exp -> Constr

dataTypeOf :: Exp -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Exp)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Exp)

gmapT :: (forall b. Data b => b -> b) -> Exp -> Exp

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Exp -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Exp -> r

gmapQ :: (forall d. Data d => d -> u) -> Exp -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Exp -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Exp -> m Exp

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Exp -> m Exp

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Exp -> m Exp

Show Exp

Defined in Language.Nominal.Examples.UntypedLambda

Methods

showsPrec :: Int -> Exp -> ShowS

show :: Exp -> String

showList :: [Exp] -> ShowS

Generic Exp

Defined in Language.Nominal.Examples.UntypedLambda

Associated Types

type Rep Exp :: Type -> Type

Methods

from :: Exp -> Rep Exp x

to :: Rep Exp x -> Exp

Swappable Exp

Defined in Language.Nominal.Examples.UntypedLambda

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Exp -> Exp

KSub Var Exp Exp

Substitution. Capture-avoidance is automatic.

Defined in Language.Nominal.Examples.UntypedLambda

Methods

sub :: Var -> Exp -> Exp -> Exp

type Rep Exp

Defined in Language.Nominal.Examples.UntypedLambda

type Rep Exp = D1 (MetaData "Exp" "Language.Nominal.Examples.UntypedLambda" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" False) (C1 (MetaCons "V" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Var)) :+: (C1 (MetaCons ":@" (InfixI LeftAssociative 9) False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Exp) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Exp)) :+: C1 (MetaCons "Lam" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (KAbs Var Exp)))))

whnf :: Exp -> Exp

weak head normal form of a lambda-term.

lam :: Var -> Exp -> Exp

helper for building lambda-abstractions

example1 :: Exp

(x x) y

example1whnf :: Exp

y

example2 :: Exp

(x xy) x

example2whnf :: Exp

xy