{-# LANGUAGE Trustworthy #-}
module DeFun.Function (
Id, IdSym,
id, idSym,
Const, ConstSym, ConstSym1,
const, constSym, constSym1,
Flip, FlipSym, FlipSym1, FlipSym2,
flip, flipSym, flipSym1, flipSym2,
Comp, CompSym, CompSym1, CompSym2,
comp, compSym, compSym1, compSym2,
Ap, ApSym, ApSym1, ApSym2,
ap, apSym, apSym1, apSym2,
Join, JoinSym, JoinSym1,
join, joinSym, joinSym1,
) where
import DeFun.Core
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
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)
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)
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)
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)
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)