Language.Symantic.Lib.Function

Symantic for '(->)'.

Class Sym_Function

class Sym_Function term where

Methods

comp :: term (b -> c) -> term (a -> b) -> term (a -> c) infixr 9

const :: term a -> term b -> term a

flip :: term (a -> b -> c) -> term (b -> a -> c)

id :: term a -> term a

comp :: Sym_Function (UnT term) => Trans term => term (b -> c) -> term (a -> b) -> term (a -> c) infixr 9

const :: Sym_Function (UnT term) => Trans term => term a -> term b -> term a

flip :: Sym_Function (UnT term) => Trans term => term (a -> b -> c) -> term (b -> a -> c)

id :: Sym_Function (UnT term) => Trans term => term a -> term a

Instances

Sym_Function Eval

Methods

comp :: Eval (b -> c) -> Eval (a -> b) -> Eval (a -> c)

const :: Eval a -> Eval b -> Eval a

flip :: Eval (a -> b -> c) -> Eval (b -> a -> c)

id :: Eval a -> Eval a

Sym_Function View

Methods

comp :: View (b -> c) -> View (a -> b) -> View (a -> c)

const :: View a -> View b -> View a

flip :: View (a -> b -> c) -> View (b -> a -> c)

id :: View a -> View a

(Sym_Function term, Sym_Lambda term) => Sym_Function (BetaT term)

Methods

comp :: BetaT term (b -> c) -> BetaT term (a -> b) -> BetaT term (a -> c)

const :: BetaT term a -> BetaT term b -> BetaT term a

flip :: BetaT term (a -> b -> c) -> BetaT term (b -> a -> c)

id :: BetaT term a -> BetaT term a

(Sym_Function r1, Sym_Function r2) => Sym_Function (Dup r1 r2)

Methods

comp :: Dup r1 r2 (b -> c) -> Dup r1 r2 (a -> b) -> Dup r1 r2 (a -> c)

const :: Dup r1 r2 a -> Dup r1 r2 b -> Dup r1 r2 a

flip :: Dup r1 r2 (a -> b -> c) -> Dup r1 r2 (b -> a -> c)

id :: Dup r1 r2 a -> Dup r1 r2 a

Types

tyFun :: Source src => Inj_Len vs => Type src vs (->)

a0 :: Source src => Inj_Len vs => Inj_Kind (K a) => Type src (Proxy a ': vs) a

b1 :: Source src => Inj_Len vs => Inj_Kind (K b) => Type src (a ': (Proxy b ': vs)) b

c2 :: Source src => Inj_Len vs => Inj_Kind (K c) => Type src (a ': (b ': (Proxy c ': vs))) c

Terms

teFunction_compose :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((b -> c) -> (a -> b) -> a -> c))

teFunction_const :: TermDef (->) '[Proxy a, Proxy b] (() #> (a -> b -> a))

teFunction_flip :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> b -> a -> c))

teFunction_id :: TermDef (->) '[Proxy a] (() #> (a -> a))

Orphan instances

ClassInstancesFor (* -> * -> *) (->)

Methods

proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q)

TypeInstancesFor (* -> * -> *) (->)

Methods

expandFamFor :: Source src => proxy c -> Len Type vs -> Const kt src fam -> Types src vs ts -> Maybe (Type kt src vs (Fam kt fam ts))

(Source src, Inj_Sym (* -> * -> *) ss (->)) => ModuleFor (* -> * -> *) src ss (->)

Methods

moduleFor :: (PathMod, Module ss (->))

Gram_Term_AtomsFor (* -> * -> *) src ss g (->)

Methods

g_term_atomsFor :: [CF (->) (AST_Term ss g)]