Language.Symantic.Transforming.Beta

Interpreter to beta-reduce static lambdas introduced only because of the compiling machinery (hence preserving lambdas put by the user).

Type BetaT

data BetaT term a where

The annotation here is if a lambda is known statically, and so can be applied if given an argument, Moreover, it only does this beta-reduction if the lambda has been introduced by the compiling phase (which happens when a symantic method is a function between terms instead of being only a term) (i.e. lam1 is used, not lam)

Constructors

BetaT_Unk :: term a -> BetaT term a

BetaT_Lam1 :: (BetaT term a -> BetaT term b) -> BetaT term (a -> b)

Instances

Sym_Lambda term => Trans (BetaT term)

Associated Types

type UnT (BetaT term :: * -> *) :: * -> *

Methods

trans :: UnT (BetaT term) a -> BetaT term a

unTrans :: BetaT term a -> UnT (BetaT term) a

trans1 :: (UnT (BetaT term) a -> UnT (BetaT term) b) -> BetaT term a -> BetaT term b

trans2 :: (UnT (BetaT term) a -> UnT (BetaT term) b -> UnT (BetaT term) c) -> BetaT term a -> BetaT term b -> BetaT term c

trans3 :: (UnT (BetaT term) a -> UnT (BetaT term) b -> UnT (BetaT term) c -> UnT (BetaT term) d) -> BetaT term a -> BetaT term b -> BetaT term c -> BetaT term d

Sym_Lambda term => Sym_Lambda (BetaT term)

lam1 adds annotations, app uses it

Methods

apply :: BetaT term ((a -> b) -> a -> b)

app :: BetaT term (a -> b) -> BetaT term a -> BetaT term b

lam :: (BetaT term a -> BetaT term b) -> BetaT term (a -> b)

let_ :: BetaT term var -> (BetaT term var -> BetaT term res) -> BetaT term res

lam1 :: (BetaT term a -> BetaT term b) -> BetaT term (a -> b)

qual :: proxy q -> BetaT term t -> BetaT term (q #> t)

type UnT (BetaT term)

type UnT (BetaT term) = term

betaT :: Trans (BetaT term) => BetaT term a -> term a

Transformer