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 :: a) :: a where ...
data IdSym (x :: FunKind a a)
id :: forall {a1} a2 (x :: a1). a2 x -> a2 (Id x)
idSym :: forall {b} (a :: b -> Type). Lam a a (IdSym :: FunKind b b -> Type)
type family Const (x :: a) (y :: b) :: a where ...
data ConstSym (x :: FunKind a (b ~> a))
data ConstSym1 (x :: a) (y :: FunKind b a)
const :: forall {k1} {k2} a (x :: k1) b (y :: k2). a x -> b y -> a x
constSym :: forall {b1} {a1} (a :: b1 -> Type) (b2 :: a1 -> Type). Lam2 a b2 a (ConstSym :: FunKind b1 (a1 ~> b1) -> Type)
constSym1 :: forall {a1} {a2} a3 (x :: a1) (b :: a2 -> Type). a3 x -> Lam b a3 (ConstSym1 x :: FunKind a2 a1 -> Type)
type family Flip (f :: a ~> (b ~> c)) (b1 :: b) (a1 :: a) :: c where ...
data FlipSym (f :: FunKind (a ~> (b ~> c)) (b ~> (a ~> c)))
data FlipSym1 (f :: a ~> (b ~> c)) (x :: FunKind b (a ~> c))
data FlipSym2 (f :: a ~> (b ~> c)) (b1 :: b) (a1 :: FunKind a c)
flip :: forall {a1} {b1} {c1} a2 b2 c2 (f :: a1 ~> (b1 ~> c1)) (x :: b1) (y :: a1). Lam2 a2 b2 c2 f -> b2 x -> a2 y -> c2 (Flip f x y)
flipSym :: forall {a1} {a2} {b1} (a3 :: a1 -> Type) (b2 :: a2 -> Type) (c :: b1 -> Type). Lam (a3 :~> (b2 :~> c)) (b2 :~> (a3 :~> c)) (FlipSym :: FunKind (a1 ~> (a2 ~> b1)) (a2 ~> (a1 ~> b1)) -> Type)
flipSym1 :: forall {a1} {b1} {c1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (f :: a1 ~> (b1 ~> c1)). Lam2 a2 b2 c2 f -> Lam2 b2 a2 c2 (FlipSym1 f)
flipSym2 :: forall {a1} {b1} {c1} (a2 :: a1 -> Type) b2 (c2 :: c1 -> Type) (f :: a1 ~> (b1 ~> c1)) (x :: b1). Lam2 a2 b2 c2 f -> b2 x -> Lam a2 c2 (FlipSym2 f x)
type family Comp (f :: b ~> c) (g :: a ~> b) (x :: a) :: c where ...
data CompSym (f :: FunKind (b ~> c) ((a ~> b) ~> (a ~> c)))
data CompSym1 (f :: b ~> c) (g :: FunKind (a ~> b) (a ~> c))
data CompSym2 (f :: b ~> c) (g :: a ~> b) (x :: FunKind a c)
comp :: forall {b1} {c1} {a1} (b2 :: b1 -> Type) c2 (f :: b1 ~> c1) a2 (g :: a1 ~> b1) (x :: a1). Lam b2 c2 f -> Lam a2 b2 g -> a2 x -> c2 (Comp f g x)
compSym :: forall {b1} {b2} {a1} (b3 :: b1 -> Type) (c :: b2 -> Type) (a2 :: a1 -> Type). Lam (b3 :~> c) (Lam a2 b3 :~> Lam a2 c) (CompSym :: FunKind (b1 ~> b2) ((a1 ~> b1) ~> (a1 ~> b2)) -> Type)
compSym1 :: forall {b1} {c1} {a1} (b2 :: b1 -> Type) (c2 :: c1 -> Type) (f :: b1 ~> c1) (a2 :: a1 -> Type). Lam b2 c2 f -> Lam (a2 :~> b2) (a2 :~> c2) (CompSym1 f :: FunKind (a1 ~> b1) (a1 ~> c1) -> Type)
compSym2 :: forall {b1} {c1} {a1} (b2 :: b1 -> Type) (c2 :: c1 -> Type) (f :: b1 ~> c1) (a2 :: a1 -> Type) (g :: a1 ~> b1). Lam b2 c2 f -> Lam a2 b2 g -> Lam a2 c2 (CompSym2 f g)
type family Ap (f :: a ~> (b ~> c)) (g :: a ~> b) (x :: a) :: c where ...
data ApSym (f :: FunKind (a ~> (b ~> c)) ((a ~> b) ~> (a ~> c)))
data ApSym1 (f :: a ~> (b ~> c)) (g :: FunKind (a ~> b) (a ~> c))
data ApSym2 (f :: a ~> (b ~> c)) (g :: a ~> b) (x :: FunKind a c)
ap :: forall {a1} {b1} {c1} a2 (b2 :: b1 -> Type) c2 (f :: a1 ~> (b1 ~> c1)) (g :: a1 ~> b1) (x :: a1). Lam2 a2 b2 c2 f -> Lam a2 b2 g -> a2 x -> c2 (Ap f g x)
apSym :: forall {a2} {b1} {b2} (a :: a2 -> Type) (b3 :: b1 -> Type) (c :: b2 -> Type). Lam3 (a :~> (b3 :~> c)) (a :~> b3) a c (ApSym :: FunKind (a2 ~> (b1 ~> b2)) ((a2 ~> b1) ~> (a2 ~> b2)) -> Type)
apSym1 :: forall {a1} {b1} {c1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (f :: a1 ~> (b1 ~> c1)). Lam2 a2 b2 c2 f -> Lam2 (a2 :~> b2) a2 c2 (ApSym1 f)
apSym2 :: forall {a1} {b1} {c1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (f :: a1 ~> (b1 ~> c1)) (g :: a1 ~> b1). Lam2 a2 b2 c2 f -> Lam a2 b2 g -> Lam a2 c2 (ApSym2 f g)
type family Join (f :: a ~> (a ~> b)) (x :: a) :: b where ...
data JoinSym (f :: FunKind (a ~> (a ~> b)) (a ~> b))
data JoinSym1 (f :: a ~> (a ~> b)) (x :: FunKind a b)
join :: forall {a1} {b1} a2 b2 (f :: a1 ~> (a1 ~> b1)) (x :: a1). Lam2 a2 a2 b2 f -> a2 x -> b2 (Join f x)
joinSym :: forall {a1} {b1} (a :: a1 -> Type) (b2 :: b1 -> Type). Lam2 (a :~> (a :~> b2)) a b2 (JoinSym :: FunKind (a1 ~> (a1 ~> b1)) (a1 ~> b1) -> Type)
joinSym1 :: forall {a1} {b1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (fun :: a1 ~> (a1 ~> b1)). Lam2 a2 a2 b2 fun -> Lam a2 b2 (JoinSym1 fun)

Id, I

type family Id (x :: a) :: a where ... Source #

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

Equations

Id (x :: a) = x

data IdSym (x :: FunKind a a) 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 :: forall {a1} a2 (x :: a1). a2 x -> a2 (Id x) Source #

idSym :: forall {b} (a :: b -> Type). Lam a a (IdSym :: FunKind b b -> Type) Source #

Const, K

type family Const (x :: a) (y :: b) :: a 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 :: a) (y :: b) = x

data ConstSym (x :: FunKind a (b ~> a)) 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 :: a) (y :: FunKind b a) 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 :: forall {k1} {k2} a (x :: k1) b (y :: k2). a x -> b y -> a x Source #

constSym :: forall {b1} {a1} (a :: b1 -> Type) (b2 :: a1 -> Type). Lam2 a b2 a (ConstSym :: FunKind b1 (a1 ~> b1) -> Type) Source #

constSym1 :: forall {a1} {a2} a3 (x :: a1) (b :: a2 -> Type). a3 x -> Lam b a3 (ConstSym1 x :: FunKind a2 a1 -> Type) Source #

Flip, C

type family Flip (f :: a ~> (b ~> c)) (b1 :: b) (a1 :: a) :: c where ... Source #

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

Equations

Flip (f :: a1 ~> (a2 ~> k)) (b :: a2) (a3 :: a1) = (f @@ a3) @@ b

data FlipSym (f :: FunKind (a ~> (b ~> c)) (b ~> (a ~> c))) 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 :: a ~> (b ~> c)) (x :: FunKind b (a ~> c)) 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 :: a ~> (b ~> c)) (b1 :: b) (a1 :: FunKind a c) 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 :: forall {a1} {b1} {c1} a2 b2 c2 (f :: a1 ~> (b1 ~> c1)) (x :: b1) (y :: a1). Lam2 a2 b2 c2 f -> b2 x -> a2 y -> c2 (Flip f x y) Source #

flipSym :: forall {a1} {a2} {b1} (a3 :: a1 -> Type) (b2 :: a2 -> Type) (c :: b1 -> Type). Lam (a3 :~> (b2 :~> c)) (b2 :~> (a3 :~> c)) (FlipSym :: FunKind (a1 ~> (a2 ~> b1)) (a2 ~> (a1 ~> b1)) -> Type) Source #

flipSym1 :: forall {a1} {b1} {c1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (f :: a1 ~> (b1 ~> c1)). Lam2 a2 b2 c2 f -> Lam2 b2 a2 c2 (FlipSym1 f) Source #

flipSym2 :: forall {a1} {b1} {c1} (a2 :: a1 -> Type) b2 (c2 :: c1 -> Type) (f :: a1 ~> (b1 ~> c1)) (x :: b1). Lam2 a2 b2 c2 f -> b2 x -> Lam a2 c2 (FlipSym2 f x) Source #

Comp, B

type family Comp (f :: b ~> c) (g :: a ~> b) (x :: a) :: c where ... Source #

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

Equations

Comp (f :: k1 ~> k2) (g :: a ~> k1) (x :: a) = f @@ (g @@ x)

data CompSym (f :: FunKind (b ~> c) ((a ~> b) ~> (a ~> c))) 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 :: b ~> c) (g :: FunKind (a ~> b) (a ~> c)) 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 :: b ~> c) (g :: a ~> b) (x :: FunKind a c) 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 :: forall {b1} {c1} {a1} (b2 :: b1 -> Type) c2 (f :: b1 ~> c1) a2 (g :: a1 ~> b1) (x :: a1). Lam b2 c2 f -> Lam a2 b2 g -> a2 x -> c2 (Comp f g x) Source #

compSym :: forall {b1} {b2} {a1} (b3 :: b1 -> Type) (c :: b2 -> Type) (a2 :: a1 -> Type). Lam (b3 :~> c) (Lam a2 b3 :~> Lam a2 c) (CompSym :: FunKind (b1 ~> b2) ((a1 ~> b1) ~> (a1 ~> b2)) -> Type) Source #

compSym1 :: forall {b1} {c1} {a1} (b2 :: b1 -> Type) (c2 :: c1 -> Type) (f :: b1 ~> c1) (a2 :: a1 -> Type). Lam b2 c2 f -> Lam (a2 :~> b2) (a2 :~> c2) (CompSym1 f :: FunKind (a1 ~> b1) (a1 ~> c1) -> Type) Source #

compSym2 :: forall {b1} {c1} {a1} (b2 :: b1 -> Type) (c2 :: c1 -> Type) (f :: b1 ~> c1) (a2 :: a1 -> Type) (g :: a1 ~> b1). Lam b2 c2 f -> Lam a2 b2 g -> Lam a2 c2 (CompSym2 f g) Source #

Ap, S

type family Ap (f :: a ~> (b ~> c)) (g :: a ~> b) (x :: a) :: c where ... Source #

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

Equations

Ap (f :: a ~> (k1 ~> k2)) (g :: a ~> k1) (x :: a) = (f @@ x) @@ (g @@ x)

data ApSym (f :: FunKind (a ~> (b ~> c)) ((a ~> b) ~> (a ~> c))) 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 :: a ~> (b ~> c)) (g :: FunKind (a ~> b) (a ~> c)) 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 :: a ~> (b ~> c)) (g :: a ~> b) (x :: FunKind a c) 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 :: forall {a1} {b1} {c1} a2 (b2 :: b1 -> Type) c2 (f :: a1 ~> (b1 ~> c1)) (g :: a1 ~> b1) (x :: a1). Lam2 a2 b2 c2 f -> Lam a2 b2 g -> a2 x -> c2 (Ap f g x) Source #

apSym :: forall {a2} {b1} {b2} (a :: a2 -> Type) (b3 :: b1 -> Type) (c :: b2 -> Type). Lam3 (a :~> (b3 :~> c)) (a :~> b3) a c (ApSym :: FunKind (a2 ~> (b1 ~> b2)) ((a2 ~> b1) ~> (a2 ~> b2)) -> Type) Source #

apSym1 :: forall {a1} {b1} {c1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (f :: a1 ~> (b1 ~> c1)). Lam2 a2 b2 c2 f -> Lam2 (a2 :~> b2) a2 c2 (ApSym1 f) Source #

apSym2 :: forall {a1} {b1} {c1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (f :: a1 ~> (b1 ~> c1)) (g :: a1 ~> b1). Lam2 a2 b2 c2 f -> Lam a2 b2 g -> Lam a2 c2 (ApSym2 f g) Source #

Join, W

type family Join (f :: a ~> (a ~> b)) (x :: a) :: b where ... Source #

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

Equations

Join (f :: a ~> (a ~> k)) (x :: a) = (f @@ x) @@ x

data JoinSym (f :: FunKind (a ~> (a ~> b)) (a ~> b)) 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 :: a ~> (a ~> b)) (x :: FunKind a b) 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 :: forall {a1} {b1} a2 b2 (f :: a1 ~> (a1 ~> b1)) (x :: a1). Lam2 a2 a2 b2 f -> a2 x -> b2 (Join f x) Source #

joinSym :: forall {a1} {b1} (a :: a1 -> Type) (b2 :: b1 -> Type). Lam2 (a :~> (a :~> b2)) a b2 (JoinSym :: FunKind (a1 ~> (a1 ~> b1)) (a1 ~> b1) -> Type) Source #

joinSym1 :: forall {a1} {b1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (fun :: a1 ~> (a1 ~> b1)). Lam2 a2 a2 b2 fun -> Lam a2 b2 (JoinSym1 fun) Source #