module Type.Yoko.Natural where
import Type.Yoko.Type
import Type.Yoko.Universe
type NT_ u f = forall t. u t -> f t
newtype NT u f = NT (forall t. u t -> Unwrap f t)
nt_ :: [qP|f :: *->*|] -> (forall t. u t -> Unwrap f t) -> NT u f
nt_ p f = NT f
appNT :: NT u f -> u t -> Unwrap f t
appNT (NT f) x = f x
appNTF :: Wrapper f => NT u f -> NT_ u f
appNTF (NT f) x = wrap (f x)
orNT :: NT u f -> NT v f -> NT (u :|| v) f
orNT (NT f) (NT g) = NT $ \uv -> case uv of
LeftU u -> f u
RightU v -> g v
constNT :: Unwrap f t -> NT ((:=:) t) f
constNT = constNT_ Proxy
constNT_ :: [qP|f :: *->*|] -> Unwrap f t -> NT ((:=:) t) f
constNT_ p x = nt_ p $ \Refl -> x
constNTF :: Wrapper f => f t -> NT ((:=:) t) f
constNTF x = NT $ \Refl -> unwrap x
firstNT :: NT_ u g -> NT g f -> NT u f
firstNT g (NT f) = NT $ f . g
data NP u f = forall t. NP (u t) (Unwrap f t)
firstNP :: NT_ u v -> NP u f -> NP v f
firstNP f (NP u x) = NP (f u) x
newtype ArrowTSS f g a = ArrowTSS (f a -> g a)
type instance Unwrap (ArrowTSS f g) a = f a -> g a
instance Wrapper (ArrowTSS f g) where wrap = ArrowTSS; unwrap (ArrowTSS f) = f
appNTtoNP :: (Wrapper f, Wrapper g) => NT u (ArrowTSS f g) -> NP u f -> NP u g
appNTtoNP (NT f) (NP u x) = NP u $ unwrap $ f u $ wrap x