module Type.Yoko.Fun
(Domain(..), Dom, Rng, applyD, apply,
YieldsArrowTSSD, DomF, RngF, eachArrow,
AsComp(..), WrapComp, WrapCompF
) where
import Type.Yoko.Type
import Type.Yoko.Universe
import Type.Yoko.Natural
import Type.Yoko.Sum
import Type.Yoko.BTree
newtype Domain fn t = AppBy (fn t -> Dom fn t -> Rng fn t)
type family Dom (fn :: * -> *) t
type family Rng (fn :: * -> *) t
applyD :: Domain fn t -> fn t -> Dom fn t -> Rng fn t
applyD (AppBy f) = f
apply :: (t ::: Domain fn) => fn t -> Dom fn t -> Rng fn t
apply = applyD inhabits
data YieldsArrowTSSD fn t where
YieldsArrowTSSD ::
(Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t
) => Domain fn t -> YieldsArrowTSSD fn t
instance (t ::: Domain fn, Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t
) => t ::: YieldsArrowTSSD fn where inhabits = YieldsArrowTSSD inhabits
type family DomF (fn :: * -> *) :: * -> *
type family RngF (fn :: * -> *) :: * -> *
yieldsArrowTSSD :: YieldsArrowTSSD fn t -> (forall t. fn t) -> DomF fn t -> RngF fn t
yieldsArrowTSSD (YieldsArrowTSSD domD) fn = applyD domD fn
eachArrow :: forall fn u.
(Finite u, Inhabitants u ::: All (YieldsArrowTSSD fn)
) => (forall t. fn t) -> NT u (ArrowTSS (DomF fn) (RngF fn))
eachArrow fn = firstNT toUni $ each [qP|YieldsArrowTSSD fn :: *->*|] $
\d -> yieldsArrowTSSD d fn
type instance Dom (fn :. f) a = Dom fn (f a)
type instance Rng (fn :. f) a = Rng fn (f a)
type instance DomF (fn :. f) = DomF fn
type instance RngF (fn :. f) = RngF fn
instance (f t ::: Domain fn) => t ::: Domain (fn :. f) where
inhabits = AppBy $ \(Compose fn) -> apply fn
type WrapComp a = WrapComp_ a
type family WrapComp_ a
type instance WrapComp_ (f (g a)) = (f :. g) a
type WrapCompF a = WrapCompF_ a
type family WrapCompF_ a :: * -> *
type instance WrapCompF_ (f (g a)) = f :. g
newtype AsComp (fn :: * -> *) t = AsComp (fn t)
type instance Unwrap (AsComp fn) t = fn t
instance Wrapper (AsComp fn) where wrap = AsComp; unwrap (AsComp x) = x
type instance Dom (AsComp fn) t = WrapComp (Dom fn t)
type instance Rng (AsComp fn) t = WrapComp (Rng fn t)
type instance DomF (AsComp fn) = WrapCompF (Dom fn ())
type instance RngF (AsComp fn) = WrapCompF (Rng fn ())
instance (t ::: Domain fn, Dom fn t ~ ex0 (ex1 ex2), Rng fn t ~ ex3 (ex4 ex5)
) => t ::: Domain (AsComp fn) where
inhabits = AppBy $ \(AsComp fn) -> wrap . apply fn . unwrap