HFunctorT.hs

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

class HFunctorT (e :: SigClass) where
    type HFTDict e :: ((Type -> Type) -> Type -> Type) -> Type
    type HFTDict _ = (:~:) IdentityT

    hfmapT :: (forall t. HFTDict e t -> t f ~> t g) -> e f ~> e g

newtype ViaHFunctor (e :: SigClass) f a = ViaHFunctor {unViaHFunctor :: e f a}
    deriving (HFunctor)

instance HFunctor e => HFunctorT (ViaHFunctor e) where
    hfmapT f = hfmap $ runIdentityT . f Refl . IdentityT
    {-# INLINE hfmapT #-}

instance HFunctorT (LiftIns e) where
    hfmapT _ = LiftIns . unliftIns
    {-# INLINE hfmapT #-}

instance (HFunctorT e1, HFunctorT e2) => HFunctorT (e1 :+: e2) where
    type HFTDict (e1 :+: e2) = HFTDict e1 G.:+: HFTDict e2
    hfmapT f =
        caseH
            (Inl . hfmapT \d -> f $ G.L1 d)
            (Inr . hfmapT \d -> f $ G.R1 d)
    {-# INLINE hfmapT #-}

data ((e1 :: SigClass) +# (f :: Type -> Type)) (a :: Type) where
    HeftyPlusT :: Hefty f (e1 :+: e2) a -> (e1 +# Hefty f e2) a

data RunCatch err m a where
    RunCatch :: (CatchS err +# m) a -> RunCatch err m (Either err a)

instance HFunctorT (RunCatch err) where
    type HFTDict (RunCatch err) = (:~:) ((+#) (CatchS err))
    hfmapT f (RunCatch a) = RunCatch $ f Refl a
    {-# INLINE hfmapT #-}

interpretR ::
    forall e r f c.
    (Freer c f, HFunctorT r, HFunctorT e) =>
    (forall t. HFTDict r t -> e (t (Hefty f r)) ~> t (Hefty f r)) ->
    Hefty f (r :+: e) ~> Hefty f r
interpretR i =
    overHefty $
        interpretFreer $
            caseH
                ( liftIns . hfmapT \d ->
                    error $
                        "ここで't (Hefty f (r :+: e)) ~> t (Hefty f r)'が必要になる"
                            ++ "いま手に入るのは'interpretR i :: Hefty f (r :+: e) ~> Hefty f r'であり、"
                            ++ "tが+#の場合はt ... ~> t ...のものが手に入るが"
                            ++ "そうでないtが一般の場合は自明には手に入らない。"
                )
                undefined

諦めてtが#+の場合（つまりF(Δ) = E+Δという和の場合）に絞る