nom-0.1.0.2: Name-binding & alpha-equivalence

Copyright(c) Murdoch J. Gabbay 2020
LicenseGPL-3
Maintainermurdoch.gabbay@gmail.com
Stabilityexperimental
PortabilityPOSIX
Safe HaskellNone
LanguageHaskell2010

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

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

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

example2 :: Exp Source #

(x xy) x