Safe Haskell	Trustworthy
Language	Haskell2010

DeFun.Function

Contents

Id, I
Const, K
Flip, C
Comp, B
Ap, S
Join, W

Description

Defunctionalized function combinators, from SKI and BCKW combinator calculi.

These may be useful for writing anonymous functions in point-free style, as pointful style would require extra defunctionalization symbols (see e.g. Map2 for an example).

Synopsis

type family Id x where ...
data IdSym x
id :: a x -> a (Id x)
idSym :: Lam a a IdSym
type family Const x y where ...
data ConstSym x
data ConstSym1 x y
const :: a x -> b y -> a x
constSym :: Lam2 a b a ConstSym
constSym1 :: a x -> Lam b a (ConstSym1 x)
type family Flip f b a where ...
data FlipSym f
data FlipSym1 f x
data FlipSym2 f b a
flip :: Lam2 a b c f -> b x -> a y -> c (Flip f x y)
flipSym :: Lam (a :~> (b :~> c)) (b :~> (a :~> c)) FlipSym
flipSym1 :: Lam2 a b c f -> Lam2 b a c (FlipSym1 f)
flipSym2 :: Lam2 a b c f -> b x -> Lam a c (FlipSym2 f x)
type family Comp f g x where ...
data CompSym f
data CompSym1 f g
data CompSym2 f g x
comp :: Lam b c f -> Lam a b g -> a x -> c (Comp f g x)
compSym :: Lam (b :~> c) (Lam a b :~> Lam a c) CompSym
compSym1 :: Lam b c f -> Lam (a :~> b) (a :~> c) (CompSym1 f)
compSym2 :: Lam b c f -> Lam a b g -> Lam a c (CompSym2 f g)
type family Ap f g x where ...
data ApSym f
data ApSym1 f g
data ApSym2 f g x
ap :: Lam2 a b c f -> Lam a b g -> a x -> c (Ap f g x)
apSym :: Lam3 (a :~> (b :~> c)) (a :~> b) a c ApSym
apSym1 :: Lam2 a b c f -> Lam2 (a :~> b) a c (ApSym1 f)
apSym2 :: Lam2 a b c f -> Lam a b g -> Lam a c (ApSym2 f g)
type family Join f x where ...
data JoinSym f
data JoinSym1 f x
join :: Lam2 a a b f -> a x -> b (Join f x)
joinSym :: Lam2 (a :~> (a :~> b)) a b JoinSym
joinSym1 :: Lam2 a a b fun -> Lam a b (JoinSym1 fun)

Id, I

type family Id x where ... Source #

Identity function. Combinator I in https://en.wikipedia.org/wiki/SKI_combinator_calculus.

Equations

Id x = x

data IdSym x Source #

Instances

Instances details

type App (IdSym :: FunKind a a -> Type) (x :: a) Source #
Instance details Defined in DeFun.Function type App (IdSym :: FunKind a a -> Type) (x :: a) = Id x

id :: a x -> a (Id x) Source #

idSym :: Lam a a IdSym Source #

Const, K

type family Const x y where ... Source #

Constant function. Combinator K in https://en.wikipedia.org/wiki/SKI_combinator_calculus and https://en.wikipedia.org/wiki/B,_C,_K,_W_system.

Equations

Const x y = x

data ConstSym x Source #

Instances

Instances details

type App (ConstSym :: FunKind a (b ~> a) -> Type) (x :: a) Source #
Instance details Defined in DeFun.Function type App (ConstSym :: FunKind a (b ~> a) -> Type) (x :: a) = ConstSym1 x :: FunKind b a -> Type

data ConstSym1 x y Source #

Instances

Instances details

type App (ConstSym1 x :: FunKind b a -> Type) (y :: b) Source #
Instance details Defined in DeFun.Function type App (ConstSym1 x :: FunKind b a -> Type) (y :: b) = Const x y

const :: a x -> b y -> a x Source #

constSym :: Lam2 a b a ConstSym Source #

constSym1 :: a x -> Lam b a (ConstSym1 x) Source #

Flip, C

type family Flip f b a where ... Source #

Function flip. Combinator C in https://en.wikipedia.org/wiki/B,_C,_K,_W_system.

Equations

Flip f b a = (f @@ a) @@ b

data FlipSym f Source #

Instances

Instances details

type App (FlipSym :: FunKind (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) (f :: a ~> (b ~> c)) Source #
Instance details Defined in DeFun.Function type App (FlipSym :: FunKind (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) (f :: a ~> (b ~> c)) = FlipSym1 f

data FlipSym1 f x Source #

Instances

Instances details

type App (FlipSym1 f :: FunKind b (a ~> c) -> Type) (x :: b) Source #
Instance details Defined in DeFun.Function type App (FlipSym1 f :: FunKind b (a ~> c) -> Type) (x :: b) = FlipSym2 f x

data FlipSym2 f b a Source #

Instances

Instances details

type App (FlipSym2 f b2 :: FunKind a1 c -> Type) (a2 :: a1) Source #
Instance details Defined in DeFun.Function type App (FlipSym2 f b2 :: FunKind a1 c -> Type) (a2 :: a1) = Flip f b2 a2

flip :: Lam2 a b c f -> b x -> a y -> c (Flip f x y) Source #

flipSym :: Lam (a :~> (b :~> c)) (b :~> (a :~> c)) FlipSym Source #

flipSym1 :: Lam2 a b c f -> Lam2 b a c (FlipSym1 f) Source #

flipSym2 :: Lam2 a b c f -> b x -> Lam a c (FlipSym2 f x) Source #

Comp, B

type family Comp f g x where ... Source #

Function composition. Combinator B in https://en.wikipedia.org/wiki/B,_C,_K,_W_system.

Equations

Comp f g x = f @@ (g @@ x)

data CompSym f Source #

Instances

Instances details

type App (CompSym :: FunKind (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) (f :: b ~> c) Source #
Instance details Defined in DeFun.Function type App (CompSym :: FunKind (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) (f :: b ~> c) = CompSym1 f :: FunKind (a ~> b) (a ~> c) -> Type

data CompSym1 f g Source #

Instances

Instances details

type App (CompSym1 f :: FunKind (a ~> b) (a ~> c) -> Type) (g :: a ~> b) Source #
Instance details Defined in DeFun.Function type App (CompSym1 f :: FunKind (a ~> b) (a ~> c) -> Type) (g :: a ~> b) = CompSym2 f g

data CompSym2 f g x Source #

Instances

Instances details

type App (CompSym2 f g :: FunKind a c -> Type) (x :: a) Source #
Instance details Defined in DeFun.Function type App (CompSym2 f g :: FunKind a c -> Type) (x :: a) = Comp f g x

comp :: Lam b c f -> Lam a b g -> a x -> c (Comp f g x) Source #

compSym :: Lam (b :~> c) (Lam a b :~> Lam a c) CompSym Source #

compSym1 :: Lam b c f -> Lam (a :~> b) (a :~> c) (CompSym1 f) Source #

compSym2 :: Lam b c f -> Lam a b g -> Lam a c (CompSym2 f g) Source #

Ap, S

type family Ap f g x where ... Source #

Combinator S in https://en.wikipedia.org/wiki/SKI_combinator_calculus.

Equations

Ap f g x = (f @@ x) @@ (g @@ x)

data ApSym f Source #

Instances

Instances details

type App (ApSym :: FunKind (a ~> (b ~> c)) ((a ~> b) ~> (a ~> c)) -> Type) (f :: a ~> (b ~> c)) Source #
Instance details Defined in DeFun.Function type App (ApSym :: FunKind (a ~> (b ~> c)) ((a ~> b) ~> (a ~> c)) -> Type) (f :: a ~> (b ~> c)) = ApSym1 f

data ApSym1 f g Source #

Instances

Instances details

type App (ApSym1 f :: FunKind (a ~> b) (a ~> c) -> Type) (g :: a ~> b) Source #
Instance details Defined in DeFun.Function type App (ApSym1 f :: FunKind (a ~> b) (a ~> c) -> Type) (g :: a ~> b) = ApSym2 f g

data ApSym2 f g x Source #

Instances

Instances details

type App (ApSym2 f g :: FunKind a c -> Type) (x :: a) Source #
Instance details Defined in DeFun.Function type App (ApSym2 f g :: FunKind a c -> Type) (x :: a) = Ap f g x

ap :: Lam2 a b c f -> Lam a b g -> a x -> c (Ap f g x) Source #

apSym :: Lam3 (a :~> (b :~> c)) (a :~> b) a c ApSym Source #

apSym1 :: Lam2 a b c f -> Lam2 (a :~> b) a c (ApSym1 f) Source #

apSym2 :: Lam2 a b c f -> Lam a b g -> Lam a c (ApSym2 f g) Source #

Join, W

type family Join f x where ... Source #

Combinator W in https://en.wikipedia.org/wiki/B,_C,_K,_W_system

Equations

Join f x = (f @@ x) @@ x

data JoinSym f Source #

Instances

Instances details

type App (JoinSym :: FunKind (a ~> (a ~> b)) (a ~> b) -> Type) (f :: a ~> (a ~> b)) Source #
Instance details Defined in DeFun.Function type App (JoinSym :: FunKind (a ~> (a ~> b)) (a ~> b) -> Type) (f :: a ~> (a ~> b)) = JoinSym1 f

data JoinSym1 f x Source #

Instances

Instances details

type App (JoinSym1 f :: FunKind a b -> Type) (x :: a) Source #
Instance details Defined in DeFun.Function type App (JoinSym1 f :: FunKind a b -> Type) (x :: a) = Join f x

join :: Lam2 a a b f -> a x -> b (Join f x) Source #

joinSym :: Lam2 (a :~> (a :~> b)) a b JoinSym Source #

joinSym1 :: Lam2 a a b fun -> Lam a b (JoinSym1 fun) Source #