{-# LANGUAGE FlexibleInstances #-}

-- | An extension of 'HFunctor' for parameterized 'Hyper.Type.HyperType's

module Hyper.Class.Morph
    ( HMorph(..), HMorphWithConstraint
    , morphTraverse, (#?>)
    , HIs2, morphMapped1, morphTraverse1
    ) where

import Control.Lens (Setter, sets)
import Data.Kind (Type)
import Hyper.Class.Traversable (HTraversable(..), ContainedH(..))
import Hyper.Type (type (#), HyperType)

import Hyper.Internal.Prelude

-- | A type-varying variant of 'HFunctor' which can modify type parameters of the mapped 'HyperType'
class HMorph s t where
    type MorphConstraint s t (c :: (HyperType -> HyperType -> Constraint)) :: Constraint

    data MorphWitness s t :: HyperType -> HyperType -> Type

    morphMap ::
        (forall a b. MorphWitness s t a b -> p # a -> q # b) ->
        s # p ->
        t # q

    morphLiftConstraint ::
        MorphConstraint s t c =>
        MorphWitness s t a b ->
        Proxy c ->
        (c a b => r) ->
        r

type HMorphWithConstraint s t c = (HMorph s t, MorphConstraint s t c)

-- | 'HTraversable' extended with support of changing type parameters of the 'HyperType'
morphTraverse ::
    (Applicative f, HMorph s t, HTraversable t) =>
    (forall a b. MorphWitness s t a b -> p # a -> f (q # b)) ->
    s # p ->
    f (t # q)
morphTraverse :: (forall (a :: HyperType) (b :: HyperType).
 MorphWitness s t a b -> (p # a) -> f (q # b))
-> (s # p) -> f (t # q)
morphTraverse forall (a :: HyperType) (b :: HyperType).
MorphWitness s t a b -> (p # a) -> f (q # b)
f = (t # ContainedH f q) -> f (t # q)
forall (h :: HyperType) (f :: * -> *) (p :: HyperType).
(HTraversable h, Applicative f) =>
(h # ContainedH f p) -> f (h # p)
hsequence ((t # ContainedH f q) -> f (t # q))
-> ((s # p) -> t # ContainedH f q) -> (s # p) -> f (t # q)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: HyperType) (b :: HyperType).
 MorphWitness s t a b -> (p # a) -> ContainedH f q # b)
-> (s # p) -> t # ContainedH f q
forall (s :: HyperType) (t :: HyperType) (p :: HyperType)
       (q :: HyperType).
HMorph s t =>
(forall (a :: HyperType) (b :: HyperType).
 MorphWitness s t a b -> (p # a) -> q # b)
-> (s # p) -> t # q
morphMap ((f (q ('AHyperType b)) -> ContainedH f q ('AHyperType b))
-> ((p # a) -> f (q ('AHyperType b)))
-> (p # a)
-> ContainedH f q ('AHyperType b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (q ('AHyperType b)) -> ContainedH f q ('AHyperType b)
forall (f :: * -> *) (p :: HyperType) (h :: AHyperType).
f (p h) -> ContainedH f p h
MkContainedH (((p # a) -> f (q ('AHyperType b)))
 -> (p # a) -> ContainedH f q ('AHyperType b))
-> (MorphWitness s t a b -> (p # a) -> f (q ('AHyperType b)))
-> MorphWitness s t a b
-> (p # a)
-> ContainedH f q ('AHyperType b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MorphWitness s t a b -> (p # a) -> f (q ('AHyperType b))
forall (a :: HyperType) (b :: HyperType).
MorphWitness s t a b -> (p # a) -> f (q # b)
f)

(#?>) ::
    (HMorph s t, MorphConstraint s t c) =>
    Proxy c -> (c a b => r) -> MorphWitness s t a b -> r
#?> :: Proxy c -> (c a b => r) -> MorphWitness s t a b -> r
(#?>) Proxy c
p c a b => r
r MorphWitness s t a b
w = MorphWitness s t a b -> Proxy c -> (c a b => r) -> r
forall (s :: HyperType) (t :: HyperType)
       (c :: HyperType -> HyperType -> Constraint) (a :: HyperType)
       (b :: HyperType) r.
(HMorph s t, MorphConstraint s t c) =>
MorphWitness s t a b -> Proxy c -> (c a b => r) -> r
morphLiftConstraint MorphWitness s t a b
w Proxy c
p c a b => r
r

class (i0 ~ t0, i1 ~ t1) => HIs2 (i0 :: HyperType) (i1 :: HyperType) t0 t1
instance HIs2 a b a b

morphMapped1 ::
    forall a b s t p q.
    HMorphWithConstraint s t (HIs2 a b) =>
    Setter (s # p) (t # q) (p # a) (q # b)
morphMapped1 :: Setter (s # p) (t # q) (p # a) (q # b)
morphMapped1 = (((p # a) -> q # b) -> (s # p) -> t # q)
-> Optical (->) (->) f (s # p) (t # q) (p # a) (q # b)
forall (p :: * -> * -> *) (q :: * -> * -> *) (f :: * -> *) a b s t.
(Profunctor p, Profunctor q, Settable f) =>
(p a b -> q s t) -> Optical p q f s t a b
sets (\(p # a) -> q # b
f -> (forall (a :: HyperType) (b :: HyperType).
 MorphWitness s t a b -> (p # a) -> q # b)
-> (s # p) -> t # q
forall (s :: HyperType) (t :: HyperType) (p :: HyperType)
       (q :: HyperType).
HMorph s t =>
(forall (a :: HyperType) (b :: HyperType).
 MorphWitness s t a b -> (p # a) -> q # b)
-> (s # p) -> t # q
morphMap (Proxy (HIs2 a b)
forall k (t :: k). Proxy t
Proxy @(HIs2 a b) Proxy (HIs2 a b)
-> (HIs2 a b a b => (p # a) -> q # b)
-> MorphWitness s t a b
-> (p # a)
-> q # b
forall (s :: HyperType) (t :: HyperType)
       (c :: HyperType -> HyperType -> Constraint) (a :: HyperType)
       (b :: HyperType) r.
(HMorph s t, MorphConstraint s t c) =>
Proxy c -> (c a b => r) -> MorphWitness s t a b -> r
#?> (p # a) -> q # b
HIs2 a b a b => (p # a) -> q # b
f))

morphTraverse1 ::
    (HMorphWithConstraint s t (HIs2 a b), HTraversable t) =>
    Traversal (s # p) (t # q) (p # a) (q # b)
morphTraverse1 :: Traversal (s # p) (t # q) (p # a) (q # b)
morphTraverse1 (p # a) -> f (q # b)
f = (t # ContainedH f q) -> f (t # q)
forall (h :: HyperType) (f :: * -> *) (p :: HyperType).
(HTraversable h, Applicative f) =>
(h # ContainedH f p) -> f (h # p)
hsequence ((t # ContainedH f q) -> f (t # q))
-> ((s # p) -> t # ContainedH f q) -> (s # p) -> f (t # q)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((p # a) -> Identity (ContainedH f q # b))
-> (s # p) -> Identity (t # ContainedH f q)
forall (a :: HyperType) (b :: HyperType) (s :: HyperType)
       (t :: HyperType) (p :: HyperType) (q :: HyperType).
HMorphWithConstraint s t (HIs2 a b) =>
Setter (s # p) (t # q) (p # a) (q # b)
morphMapped1 (((p # a) -> Identity (ContainedH f q # b))
 -> (s # p) -> Identity (t # ContainedH f q))
-> ((p # a) -> ContainedH f q # b) -> (s # p) -> t # ContainedH f q
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ f (q # b) -> ContainedH f q # b
forall (f :: * -> *) (p :: HyperType) (h :: AHyperType).
f (p h) -> ContainedH f p h
MkContainedH (f (q # b) -> ContainedH f q # b)
-> ((p # a) -> f (q # b)) -> (p # a) -> ContainedH f q # b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p # a) -> f (q # b)
f)