{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Ten.Functor.WithIndex
( Index10
, Functor10WithIndex(..), fmap10C
) where
import Data.Kind (Type)
import GHC.Generics ((:.:)(..))
import Data.Ten.Entails (Entails, byEntailment)
import Data.Ten.Functor (Functor10(..))
type family Index10 (f :: (k -> Type) -> Type) :: k -> Type
type instance Index10 (g :.: f) = Index10 f
class Functor10 f => Functor10WithIndex f where
imap10 :: (forall a. Index10 f a -> m a -> n a) -> f m -> f n
instance (Functor g, Functor10WithIndex f) => Functor10WithIndex (g :.: f) where
imap10 :: (forall (a :: k). Index10 (g :.: f) a -> m a -> n a)
-> (:.:) g f m -> (:.:) g f n
imap10 forall (a :: k). Index10 (g :.: f) a -> m a -> n a
f (Comp1 g (f m)
gfm) = g (f n) -> (:.:) g f n
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (g (f n) -> (:.:) g f n) -> g (f n) -> (:.:) g f n
forall a b. (a -> b) -> a -> b
$ (f m -> f n) -> g (f m) -> g (f n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall (a :: k). Index10 f a -> m a -> n a) -> f m -> f n
forall k (f :: (k -> *) -> *) (m :: k -> *) (n :: k -> *).
Functor10WithIndex f =>
(forall (a :: k). Index10 f a -> m a -> n a) -> f m -> f n
imap10 forall (a :: k). Index10 f a -> m a -> n a
forall (a :: k). Index10 (g :.: f) a -> m a -> n a
f) g (f m)
gfm
fmap10C
:: forall c f m n
. (Entails (Index10 f) c, Functor10WithIndex f)
=> (forall a. c a => m a -> n a) -> f m -> f n
fmap10C :: (forall (a :: k). c a => m a -> n a) -> f m -> f n
fmap10C forall (a :: k). c a => m a -> n a
f = (forall (a :: k). Index10 f a -> m a -> n a) -> f m -> f n
forall k (f :: (k -> *) -> *) (m :: k -> *) (n :: k -> *).
Functor10WithIndex f =>
(forall (a :: k). Index10 f a -> m a -> n a) -> f m -> f n
imap10 ((c a => m a -> n a) -> Index10 f a -> m a -> n a
forall k1 (c :: k1 -> Constraint) (k2 :: k1 -> *) (a :: k1) r.
Entails k2 c =>
(c a => r) -> k2 a -> r
byEntailment @c c a => m a -> n a
forall (a :: k). c a => m a -> n a
f)