Copyright	(c) Murdoch J. Gabbay 2020
License	GPL-3
Maintainer	murdoch.gabbay@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	None
Language	Haskell2010

Language.Nominal.Examples.UntypedLambda

Description

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.

Synopsis

type Var = Name String
data Exp
- = V Var
- | Exp :@ Exp
- | Lam (KAbs Var Exp)
whnf :: Exp -> Exp
lam :: Var -> Exp -> Exp
example1 :: Exp
example1whnf :: Exp
example2 :: Exp
example2whnf :: Exp

Documentation

type Var = Name String Source #

Variables are string-labelled names

data Exp Source #

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 Source #
Instance details Defined in Language.Nominal.Examples.UntypedLambda Methods (==) :: Exp -> Exp -> Bool # (/=) :: Exp -> Exp -> Bool #
Data Exp Source #
Instance details 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 Source #
Instance details Defined in Language.Nominal.Examples.UntypedLambda Methods showsPrec :: Int -> Exp -> ShowS # show :: Exp -> String # showList :: [Exp] -> ShowS #
Generic Exp Source #
Instance details 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 Source #
Instance details Defined in Language.Nominal.Examples.UntypedLambda Methods kswp :: Typeable s => KAtom s -> KAtom s -> Exp -> Exp Source #
KSub Var Exp Exp Source #	Substitution. Capture-avoidance is automatic.
Instance details Defined in Language.Nominal.Examples.UntypedLambda Methods sub :: Var -> Exp -> Exp -> Exp Source #
type Rep Exp Source #
Instance details 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 Source #

weak head normal form of a lambda-term.

lam :: Var -> Exp -> Exp Source #

helper for building lambda-abstractions

example1 :: Exp Source #

(x x) y

example1whnf :: Exp Source #

y

example2 :: Exp Source #

(x xy) x

example2whnf :: Exp Source #

xy