{-# LANGUAGE Trustworthy #-}
module DeFun.Core where
import Data.Kind (Type)
type FunKind :: Type -> Type -> Type
data FunKind :: Type -> Type -> Type
type Fun a b = FunKind a b -> Type
type (~>) a b = Fun a b
infixr 0 ~>
type family App (f :: a ~> b) (x :: a) :: b
type (@@) a b = App a b
infixl 9 @@
type Lam :: (a -> Type) -> (b -> Type) -> (a ~> b) -> Type
newtype Lam a b f = Lam { forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
Lam a b f -> LamRep a b f
appLam :: LamRep a b f }
type a :~> b = Lam a b
infixr 0 :~>
mkLam :: LamRep a b f -> Lam a b f
mkLam :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
mkLam = forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam
type LamRep :: (a -> Type) -> (b -> Type) -> (a ~> b) -> Type
type LamRep a b fun = forall x. a x -> b (fun @@ x)
(@@) :: Lam a b f -> a x -> b (f @@ x)
Lam a b f
f @@ :: forall {a} {k} (a :: a -> *) (b :: k -> *) (f :: a ~> k) (x :: a).
Lam a b f -> a x -> b (f @@ x)
@@ a x
x = forall a b (a :: a -> *) (b :: b -> *) (f :: a ~> b).
Lam a b f -> LamRep a b f
appLam Lam a b f
f a x
x
type Lam2 a b c fun = Lam a (b :~> c) fun
type Lam3 a b c d fun = Lam a (b :~> c :~> d) fun
type LamRep2 :: (a -> Type) -> (b -> Type) -> (c -> Type) -> (a ~> b ~> c) -> Type
type LamRep2 a b c fun = forall x y. a x -> b y -> c (fun @@ x @@ y)
type LamRep3 :: (a -> Type) -> (b -> Type) -> (c -> Type) -> (d -> Type) -> (a ~> b ~> c ~> d) -> Type
type LamRep3 a b c d fun = forall x y z. a x -> b y -> c z -> d (fun @@ x @@ y @@ z)
pattern Lam2 :: LamRep2 a b c fun -> Lam2 a b c fun
pattern $bLam2 :: forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (fun :: a1 ~> (b1 ~> c1)).
LamRep2 a2 b2 c2 fun -> Lam2 a2 b2 c2 fun
$mLam2 :: forall {r} {a1} {b1} {c1} {a2 :: a1 -> *} {b2 :: b1 -> *}
{c2 :: c1 -> *} {fun :: a1 ~> (b1 ~> c1)}.
Lam2 a2 b2 c2 fun
-> (LamRep2 a2 b2 c2 fun -> r) -> ((# #) -> r) -> r
Lam2 f <- (appLam2 -> f)
where Lam2 LamRep2 a2 b2 c2 fun
f = forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (fun :: a1 ~> (b1 ~> c1)).
LamRep2 a2 b2 c2 fun -> Lam2 a2 b2 c2 fun
mkLam2 LamRep2 a2 b2 c2 fun
f
pattern Lam3 :: LamRep3 a b c d fun -> Lam3 a b c d fun
pattern $bLam3 :: forall {a1} {b1} {c1} {d1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (d2 :: d1 -> *) (fun :: a1 ~> (b1 ~> (c1 ~> d1))).
LamRep3 a2 b2 c2 d2 fun -> Lam3 a2 b2 c2 d2 fun
$mLam3 :: forall {r} {a1} {b1} {c1} {d1} {a2 :: a1 -> *} {b2 :: b1 -> *}
{c2 :: c1 -> *} {d2 :: d1 -> *} {fun :: a1 ~> (b1 ~> (c1 ~> d1))}.
Lam3 a2 b2 c2 d2 fun
-> (LamRep3 a2 b2 c2 d2 fun -> r) -> ((# #) -> r) -> r
Lam3 f <- (appLam3 -> f)
where Lam3 LamRep3 a2 b2 c2 d2 fun
f = forall {a1} {b1} {c1} {d1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (d2 :: d1 -> *) (fun :: a1 ~> (b1 ~> (c1 ~> d1))).
LamRep3 a2 b2 c2 d2 fun -> Lam3 a2 b2 c2 d2 fun
mkLam3 LamRep3 a2 b2 c2 d2 fun
f
mkLam2 :: LamRep2 a b c fun -> Lam2 a b c fun
mkLam2 :: forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (fun :: a1 ~> (b1 ~> c1)).
LamRep2 a2 b2 c2 fun -> Lam2 a2 b2 c2 fun
mkLam2 LamRep2 a b c fun
f = forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam (\a x
x -> forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam (LamRep2 a b c fun
f a x
x))
appLam2 :: Lam2 a b c fun -> LamRep2 a b c fun
appLam2 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(fun :: a ~> (b ~> c)).
Lam2 a b c fun -> LamRep2 a b c fun
appLam2 Lam2 a b c fun
f a x
x b y
y = Lam2 a b c fun
f forall {a} {k} (a :: a -> *) (b :: k -> *) (f :: a ~> k) (x :: a).
Lam a b f -> a x -> b (f @@ x)
@@ a x
x forall {a} {k} (a :: a -> *) (b :: k -> *) (f :: a ~> k) (x :: a).
Lam a b f -> a x -> b (f @@ x)
@@ b y
y
mkLam3 :: LamRep3 a b c d fun -> Lam3 a b c d fun
mkLam3 :: forall {a1} {b1} {c1} {d1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (d2 :: d1 -> *) (fun :: a1 ~> (b1 ~> (c1 ~> d1))).
LamRep3 a2 b2 c2 d2 fun -> Lam3 a2 b2 c2 d2 fun
mkLam3 LamRep3 a b c d fun
f = forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
Lam (\a x
x -> forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (fun :: a1 ~> (b1 ~> c1)).
LamRep2 a2 b2 c2 fun -> Lam2 a2 b2 c2 fun
mkLam2 (LamRep3 a b c d fun
f a x
x))
appLam3 :: Lam3 a b c d fun -> LamRep3 a b c d fun
appLam3 :: forall {a} {b} {c} {d} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(d :: d -> *) (fun :: a ~> (b ~> (c ~> d))).
Lam3 a b c d fun -> LamRep3 a b c d fun
appLam3 Lam3 a b c d fun
f a x
x b y
y c z
z = Lam3 a b c d fun
f forall {a} {k} (a :: a -> *) (b :: k -> *) (f :: a ~> k) (x :: a).
Lam a b f -> a x -> b (f @@ x)
@@ a x
x forall {a} {k} (a :: a -> *) (b :: k -> *) (f :: a ~> k) (x :: a).
Lam a b f -> a x -> b (f @@ x)
@@ b y
y forall {a} {k} (a :: a -> *) (b :: k -> *) (f :: a ~> k) (x :: a).
Lam a b f -> a x -> b (f @@ x)
@@ c z
z
type Con1 :: (a -> b) -> a ~> b
data Con1 con arg
type instance App (Con1 f) x = f x
type Con2 :: (a -> b -> c) -> a ~> b ~> c
data Con2 con arg
type instance App (Con2 f) arg = Con1 (f arg)
type Con3 :: (a -> b -> c -> d) -> a ~> b ~> c ~> d
data Con3 con arg
type instance App (Con3 f) arg = Con2 (f arg)
con1 :: LamRep a b (Con1 con) -> Lam a b (Con1 con)
con1 :: forall {a} {b} (a :: a -> *) (b :: b -> *) (con :: a -> b).
LamRep a b (Con1 con) -> Lam a b (Con1 con)
con1 = forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b).
LamRep a b f -> Lam a b f
mkLam
con2 :: LamRep2 a b c (Con2 con) -> Lam2 a b c (Con2 con)
con2 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(con :: a -> b -> c).
LamRep2 a b c (Con2 con) -> Lam2 a b c (Con2 con)
con2 = forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (fun :: a1 ~> (b1 ~> c1)).
LamRep2 a2 b2 c2 fun -> Lam2 a2 b2 c2 fun
mkLam2
con3 :: LamRep3 a b c d (Con3 con) -> Lam3 a b c d (Con3 con)
con3 :: forall {a} {b} {c} {d} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(d :: d -> *) (con :: a -> b -> c -> d).
LamRep3 a b c d (Con3 con) -> Lam3 a b c d (Con3 con)
con3 = forall {a1} {b1} {c1} {d1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (d2 :: d1 -> *) (fun :: a1 ~> (b1 ~> (c1 ~> d1))).
LamRep3 a2 b2 c2 d2 fun -> Lam3 a2 b2 c2 d2 fun
mkLam3