{-# LANGUAGE QuantifiedConstraints #-}

-- 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/.

{- |
Copyright   :  (c) 2023 Yamada Ryo
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp
Stability   :  experimental
Portability :  portable

A type class to abstract away the encoding details of the Freer carriers.
-}
module Control.Freer where

import Control.Applicative.Free (Ap, liftAp, runAp)
import Control.Effect.Class (type (~>))
import Data.Functor.Coyoneda (Coyoneda, hoistCoyoneda, liftCoyoneda, lowerCoyoneda)

-- | A type class to abstract away the encoding details of the Freer carrier.
class (forall ins. c (f ins)) => Freer c f | f -> c where
    {-# MINIMAL liftIns, (interpretF | retract, transformF) #-}

    -- | Lift a /instruction/ into a Freer carrier.
    liftIns :: ins a -> f ins a

    interpretF :: c m => (ins ~> m) -> f ins a -> m a
    interpretF ins ~> m
i = forall {k} (c :: (k -> *) -> Constraint) (f :: (k -> *) -> k -> *)
       (m :: k -> *) (a :: k).
(Freer c f, c m) =>
f m a -> m a
retract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (c :: (k -> *) -> Constraint) (f :: (k -> *) -> k -> *)
       (ins :: k -> *) (ins' :: k -> *) (a :: k).
Freer c f =>
(ins ~> ins') -> f ins a -> f ins' a
transformF ins ~> m
i
    {-# INLINE interpretF #-}

    retract :: c m => f m a -> m a
    retract = forall {k} (c :: (k -> *) -> Constraint) (f :: (k -> *) -> k -> *)
       (m :: k -> *) (ins :: k -> *) (a :: k).
(Freer c f, c m) =>
(ins ~> m) -> f ins a -> m a
interpretF forall a. a -> a
id
    {-# INLINE retract #-}

    -- | Translate /instruction/s embedded in a Freer carrier.
    transformF ::
        (ins ~> ins') ->
        f ins a ->
        f ins' a
    transformF ins ~> ins'
phi = forall {k} (c :: (k -> *) -> Constraint) (f :: (k -> *) -> k -> *)
       (m :: k -> *) (ins :: k -> *) (a :: k).
(Freer c f, c m) =>
(ins ~> m) -> f ins a -> m a
interpretF forall a b. (a -> b) -> a -> b
$ forall {k} (c :: (k -> *) -> Constraint) (f :: (k -> *) -> k -> *)
       (ins :: k -> *) (a :: k).
Freer c f =>
ins a -> f ins a
liftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. ins ~> ins'
phi
    {-# INLINE transformF #-}

    reinterpretF :: (ins ~> f ins) -> f ins a -> f ins a
    reinterpretF = forall {k} (c :: (k -> *) -> Constraint) (f :: (k -> *) -> k -> *)
       (m :: k -> *) (ins :: k -> *) (a :: k).
(Freer c f, c m) =>
(ins ~> m) -> f ins a -> m a
interpretF
    {-# INLINE reinterpretF #-}

instance Freer Functor Coyoneda where
    liftIns :: forall (ins :: * -> *) a. ins a -> Coyoneda ins a
liftIns = forall (ins :: * -> *) a. ins a -> Coyoneda ins a
liftCoyoneda
    interpretF :: forall (m :: * -> *) (ins :: * -> *) a.
Functor m =>
(ins ~> m) -> Coyoneda ins a -> m a
interpretF ins ~> m
i = forall (m :: * -> *) a. Functor m => Coyoneda m a -> m a
lowerCoyoneda forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (ins' :: * -> *) a.
(ins ~> ins') -> Coyoneda ins a -> Coyoneda ins' a
hoistCoyoneda ins ~> m
i
    {-# INLINE liftIns #-}
    {-# INLINE interpretF #-}

instance Freer Applicative Ap where
    liftIns :: forall (ins :: * -> *) a. ins a -> Ap ins a
liftIns = forall (ins :: * -> *) a. ins a -> Ap ins a
liftAp
    interpretF :: forall (m :: * -> *) (ins :: * -> *) a.
Applicative m =>
(ins ~> m) -> Ap ins a -> m a
interpretF = forall (m :: * -> *) (ins :: * -> *) a.
Applicative m =>
(ins ~> m) -> Ap ins a -> m a
runAp
    {-# INLINE liftIns #-}
    {-# INLINE interpretF #-}