{-# LANGUAGE Trustworthy #-}
-- | Defunctionalized function combinators,
-- from [SKI](https://en.wikipedia.org/wiki/SKI_combinator_calculus)
-- and [BCKW](https://en.wikipedia.org/wiki/B,_C,_K,_W_system) 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. t'DeFun.List.Map2' for an example).
--
module DeFun.Function (
    -- * Id, I
    Id, IdSym,
    id, idSym,
    -- * Const, K
    Const, ConstSym, ConstSym1,
    const, constSym, constSym1,
    -- * Flip, C
    Flip, FlipSym, FlipSym1, FlipSym2,
    flip, flipSym, flipSym1, flipSym2,
    -- * Comp, B
    Comp, CompSym, CompSym1, CompSym2,
    comp, compSym, compSym1, compSym2,
    -- * Ap, S
    Ap, ApSym, ApSym1, ApSym2,
    ap, apSym, apSym1, apSym2,
    -- * Join, W
    Join, JoinSym, JoinSym1,
    join, joinSym, joinSym1,
) where

import DeFun.Core

-- $setup
-- >>> import Prelude (Bool (..))
-- >>> import Data.Singletons.Bool (SBool (..))
-- >>> import DeFun

-- | Identity function. Combinator @I@ in https://en.wikipedia.org/wiki/SKI_combinator_calculus.
type Id :: a -> a
type family Id x where
    Id x = x

type IdSym :: a ~> a
data IdSym x
type instance App IdSym x = Id x

id :: a x -> a (Id x)
id :: forall {a} (a :: a -> *) (x :: a). a x -> a (Id x)
id a x
x = a x
x

idSym :: Lam a a IdSym
idSym :: forall {b} (a :: b -> *). Lam a a IdSym
idSym = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam forall {a} (a :: a -> *) (x :: a). a x -> a (Id x)
id

--

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

type Const :: a -> b -> a
type family Const x y where
    Const x y = x

type ConstSym :: a ~> b ~> a
data ConstSym x
type instance App ConstSym x = ConstSym1 x

type ConstSym1 :: a -> b ~> a
data ConstSym1 x y
type instance App (ConstSym1 x) y = Const x y

const :: a x -> b y -> a x
const :: forall {k} {k} (a :: k -> *) (x :: k) (b :: k -> *) (y :: k).
a x -> b y -> a x
const a x
x b y
_ = a x
x

constSym :: Lam2 a b a ConstSym
constSym :: forall {b} {a} (a :: b -> *) (b :: a -> *). Lam2 a b a ConstSym
constSym = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam forall {a} {a} (a :: a -> *) (x :: a) (b :: a -> *).
a x -> Lam b a (ConstSym1 x)
constSym1

constSym1 :: a x -> Lam b a (ConstSym1 x)
constSym1 :: forall {a} {a} (a :: a -> *) (x :: a) (b :: a -> *).
a x -> Lam b a (ConstSym1 x)
constSym1 a x
x = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam (forall {k} {k} (a :: k -> *) (x :: k) (b :: k -> *) (y :: k).
a x -> b y -> a x
const a x
x)

-- | Function flip. Combinator @C@ in https://en.wikipedia.org/wiki/B,_C,_K,_W_system.
type Flip :: (a ~> b ~> c) -> b -> a -> c
type family Flip f b a where
    Flip f b a = f @@ a @@ b

type FlipSym :: (a ~> b ~> c) ~> b ~> a ~> c
data FlipSym f
type instance App FlipSym f = FlipSym1 f

type FlipSym1 :: (a ~> b ~> c) -> b ~> a ~> c
data FlipSym1 f x
type instance App (FlipSym1 f) x = FlipSym2 f x

type FlipSym2 :: (a ~> b ~> c) -> b -> a ~> c
data FlipSym2 f b a
type instance App (FlipSym2 f b) a = Flip f b a

flip :: Lam2 a b c f -> b x -> a y -> c (Flip f x y)
flip :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (x :: b) (y :: a).
Lam2 a b c f -> b x -> a y -> c (Flip f x y)
flip Lam2 a b c f
f b x
b a y
a = Lam2 a b c f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a y
a forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ b x
b

flipSym :: Lam (a :~> b :~> c) (b :~> a :~> c) FlipSym
flipSym :: forall {a} {a} {b} (a :: a -> *) (b :: a -> *) (c :: b -> *).
Lam (a :~> (b :~> c)) (b :~> (a :~> c)) FlipSym
flipSym = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)).
Lam2 a b c f -> Lam2 b a c (FlipSym1 f)
flipSym1

flipSym1 :: Lam2 a b c f -> Lam2 b a c (FlipSym1 f)
flipSym1 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)).
Lam2 a b c f -> Lam2 b a c (FlipSym1 f)
flipSym1 Lam2 a b c f
f = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam (forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (x :: b).
Lam2 a b c f -> b x -> Lam a c (FlipSym2 f x)
flipSym2 Lam2 a b c f
f)

flipSym2 :: Lam2 a b c f -> b x -> Lam a c (FlipSym2 f x)
flipSym2 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (x :: b).
Lam2 a b c f -> b x -> Lam a c (FlipSym2 f x)
flipSym2 Lam2 a b c f
f b x
b = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam (forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (x :: b) (y :: a).
Lam2 a b c f -> b x -> a y -> c (Flip f x y)
flip Lam2 a b c f
f b x
b)


--

-- | Function composition. Combinator @B@ in https://en.wikipedia.org/wiki/B,_C,_K,_W_system.
type Comp :: (b ~> c) -> (a ~> b) -> a -> c
type family Comp f g x where
    Comp f g x = f @@ (g @@ x)

type CompSym :: (b ~> c) ~> (a ~> b) ~> a ~> c
data CompSym f
type instance App CompSym f = CompSym1 f

type CompSym1 :: (b ~> c) -> (a ~> b) ~> a ~> c
data CompSym1 f g
type instance App (CompSym1 f) g = CompSym2 f g

type CompSym2 :: (b ~> c) -> (a ~> b) -> a ~> c
data CompSym2 f g x
type instance App (CompSym2 f g) x = Comp f g x

comp :: Lam b c f -> Lam a b g -> a x -> c (Comp f g x)
comp :: forall {b} {c} {a} (b :: b -> *) (c :: c -> *) (f :: b ~> c)
       (a :: a -> *) (g :: a ~> b) (x :: a).
Lam b c f -> Lam a b g -> a x -> c (Comp f g x)
comp Lam b c f
f Lam a b g
g a x
x = Lam b c f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ (Lam a b g
g forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x)

compSym :: Lam (b :~> c) (Lam a b :~> Lam a c) CompSym
compSym :: forall {b} {b} {a} (b :: b -> *) (c :: b -> *) (a :: a -> *).
Lam (b :~> c) (Lam a b :~> Lam a c) CompSym
compSym = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam forall {b} {c} {a} (b :: b -> *) (c :: c -> *) (f :: b ~> c)
       (a :: a -> *).
Lam b c f -> Lam (a :~> b) (a :~> c) (CompSym1 f)
compSym1

compSym1 :: Lam b c f -> Lam (a :~> b) (a :~> c) (CompSym1 f)
compSym1 :: forall {b} {c} {a} (b :: b -> *) (c :: c -> *) (f :: b ~> c)
       (a :: a -> *).
Lam b c f -> Lam (a :~> b) (a :~> c) (CompSym1 f)
compSym1 Lam b c f
f = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam (forall {b} {c} {a} (b :: b -> *) (c :: c -> *) (f :: b ~> c)
       (a :: a -> *) (g :: a ~> b).
Lam b c f -> Lam a b g -> Lam a c (CompSym2 f g)
compSym2 Lam b c f
f)

compSym2 :: Lam b c f -> Lam a b g -> Lam a c (CompSym2 f g)
compSym2 :: forall {b} {c} {a} (b :: b -> *) (c :: c -> *) (f :: b ~> c)
       (a :: a -> *) (g :: a ~> b).
Lam b c f -> Lam a b g -> Lam a c (CompSym2 f g)
compSym2 Lam b c f
f Lam a b g
g = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam (forall {b} {c} {a} (b :: b -> *) (c :: c -> *) (f :: b ~> c)
       (a :: a -> *) (g :: a ~> b) (x :: a).
Lam b c f -> Lam a b g -> a x -> c (Comp f g x)
comp Lam b c f
f Lam a b g
g)

-- | Combinator 'S' in https://en.wikipedia.org/wiki/SKI_combinator_calculus.
type Ap :: (a ~> b ~> c) -> (a ~> b) -> a -> c
type family Ap f g x where
    Ap f g x = f @@ x @@ (g @@ x)

type ApSym :: (a ~> b ~> c) ~> (a ~> b) ~> a ~> c
data ApSym f
type instance App ApSym f = ApSym1 f

type ApSym1 :: (a ~> b ~> c) -> (a ~> b) ~> a ~> c
data ApSym1 f g
type instance App (ApSym1 f) g = ApSym2 f g

type ApSym2 :: (a ~> b ~> c) -> (a ~> b) -> a ~> c
data ApSym2 f g x
type instance App (ApSym2 f g) x = Ap f g x

ap :: Lam2 a b c f -> Lam a b g -> a x -> c (Ap f g x)
ap :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (g :: a ~> b) (x :: a).
Lam2 a b c f -> Lam a b g -> a x -> c (Ap f g x)
ap Lam2 a b c f
f Lam a b g
g a x
x = Lam2 a b c f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ (Lam a b g
g forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x)

apSym :: Lam3 (a :~> b :~> c) (a :~> b) a c ApSym
apSym :: forall {a} {b} {b} (a :: a -> *) (b :: b -> *) (c :: b -> *).
Lam3 (a :~> (b :~> c)) (a :~> b) a c ApSym
apSym = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)).
Lam2 a b c f -> Lam2 (a :~> b) a c (ApSym1 f)
apSym1

apSym1 :: Lam2 a b c f -> Lam2 (a :~> b) a c (ApSym1 f)
apSym1 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)).
Lam2 a b c f -> Lam2 (a :~> b) a c (ApSym1 f)
apSym1 Lam2 a b c f
f = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam (forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (g :: a ~> b).
Lam2 a b c f -> Lam a b g -> Lam a c (ApSym2 f g)
apSym2 Lam2 a b c f
f)

apSym2 :: Lam2 a b c f -> Lam a b g -> Lam a c (ApSym2 f g)
apSym2 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (g :: a ~> b).
Lam2 a b c f -> Lam a b g -> Lam a c (ApSym2 f g)
apSym2 Lam2 a b c f
f Lam a b g
g = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam (forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (g :: a ~> b) (x :: a).
Lam2 a b c f -> Lam a b g -> a x -> c (Ap f g x)
ap Lam2 a b c f
f Lam a b g
g) 

-- | Combinator 'W' in https://en.wikipedia.org/wiki/B,_C,_K,_W_system
type Join :: (a ~> a ~> b) -> a -> b
type family Join f x where
    Join f x = f @@ x @@ x

type JoinSym :: (a ~> a ~> b) ~> a ~> b
data JoinSym f
type instance App JoinSym f = JoinSym1 f

type JoinSym1 :: (a ~> a ~> b) -> a ~> b
data JoinSym1 f x
type instance App (JoinSym1 f) x = Join f x

join :: Lam2 a a b f -> a x -> b (Join f x)
join :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (a ~> b))
       (x :: a).
Lam2 a a b f -> a x -> b (Join f x)
join Lam2 a a b f
f a x
x = Lam2 a a b f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x

joinSym :: Lam2 (a :~> a :~> b) a b JoinSym
joinSym :: forall {a} {b} (a :: a -> *) (b :: b -> *).
Lam2 (a :~> (a :~> b)) a b JoinSym
joinSym = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam forall {a} {b} (a :: a -> *) (b :: b -> *) (fun :: a ~> (a ~> b)).
Lam2 a a b fun -> Lam a b (JoinSym1 fun)
joinSym1

joinSym1 :: Lam2 a a b fun -> Lam a b (JoinSym1 fun)
joinSym1 :: forall {a} {b} (a :: a -> *) (b :: b -> *) (fun :: a ~> (a ~> b)).
Lam2 a a b fun -> Lam a b (JoinSym1 fun)
joinSym1 Lam2 a a b fun
f = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (a ~> b))
       (x :: a).
Lam2 a a b f -> a x -> b (Join f x)
join Lam2 a a b fun
f)