{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE LinearTypes #-} {-# OPTIONS_GHC -Wno-orphans #-} module Proarrow.Category.Instance.Free where import Data.Kind (Constraint) import Data.Typeable (Typeable, eqT, (:~:) (..)) import Prelude (Bool (..), Eq (..), Maybe (..), Show (..), (&&)) import Prelude qualified as P import Proarrow.Core ( CAT , CategoryOf (..) , Kind , Profunctor (..) , Promonad (..) , UN , dimapDefault , type (+->) ) import Proarrow.Profunctor.Initial (InitialProfunctor) import Proarrow.Profunctor.Representable (Representable (..), withRepOb) import Data.Char (toLower) type family All (cs :: [Kind -> Constraint]) (k :: Kind) :: Constraint where All '[] k = () All (c ': cs) k = (c k, All cs k) class (All cs k => c k) => FromAll cs c k instance (All cs k => c k) => FromAll cs c k type Elem :: (Kind -> Constraint) -> [Kind -> Constraint] -> Constraint class (forall k. FromAll cs c k) => c `Elem` cs instance {-# OVERLAPPABLE #-} (c `Elem` cs) => c `Elem` (d ': cs) instance c `Elem` (c ': cs) newtype FREE (cs :: [Kind -> Constraint]) (p :: CAT j) = EMB j type instance UN EMB (EMB a) = a type Free :: CAT (FREE cs p) data Free a b where Id :: (Ob a) => Free a a Emb :: (Ob a, Ob b, Typeable a, Typeable b) => p a b %1 -> Free (i :: FREE cs p) (EMB a) %1 -> Free i (EMB b) Str :: forall {j} {cs} {p :: CAT j} (c :: Kind -> Constraint) (a :: FREE cs p) b i . (HasStructure cs p c, Ob a, Ob b) => Struct c a b %1 -> Free i a %1 -> Free i b emb :: (Ob a, Ob b, Typeable a, Typeable b, Ok cs p) => p a b %1 -> Free (EMB a :: FREE cs p) (EMB b) emb :: forall {j :: Kind} (a :: j) (b :: j) (cs :: [Kind -> Constraint]) (p :: CAT j). (Ob a, Ob b, Typeable a, Typeable b, Ok cs p) => p a b %1 -> Free ('EMB a) ('EMB b) emb p a b p = p a b -> Free ('EMB a) ('EMB a) -> Free ('EMB a) ('EMB b) forall {j :: Kind} (c :: j) (a :: j) (p :: j -> j -> Kind) (cs :: [Kind -> Constraint]) (i :: FREE cs p). (Ob c, Ob a, Typeable c, Typeable a) => p c a -> Free i ('EMB c) -> Free i ('EMB a) Emb p a b p Free ('EMB a) ('EMB a) forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j} (a :: FREE cs p). Ob a => Free a a Id class (forall x y. Eq (p x y)) => Eq2 p instance (forall x y. Eq (p x y)) => Eq2 p class (forall x y. P.Show (p x y)) => Show2 p instance (forall x y. P.Show (p x y)) => Show2 p class (Typeable p, Typeable cs, Typeable j, All cs (FREE cs p)) => Ok cs (p :: CAT j) instance (Typeable p, Typeable cs, Typeable j, All cs (FREE cs p)) => Ok cs (p :: CAT j) class (Ok c p, Eq2 p) => WithEq (a :: FREE c (p :: CAT j)) instance (Ok c p, Eq2 p) => WithEq (a :: FREE c (p :: CAT j)) instance (WithEq a) => Eq (Free a b) where Free a b Id == :: Free a b -> Free a b -> Bool == Free a b Id = Bool True Emb @al p a b p1 Free a ('EMB a) g1 == Emb @ar p a b p2 Free a ('EMB a) g2 = case forall (a :: j) (b :: j). (Typeable a, Typeable b) => Maybe (a :~: b) forall {k :: Kind} (a :: k) (b :: k). (Typeable a, Typeable b) => Maybe (a :~: b) eqT @al @ar of Just a :~: a Refl -> p a b p1 p a b -> p a b -> Bool forall (a :: Kind). Eq a => a -> a -> Bool == p a b p a b p2 Bool -> Bool -> Bool && Free a ('EMB a) g1 Free a ('EMB a) -> Free a ('EMB a) -> Bool forall (a :: Kind). Eq a => a -> a -> Bool == Free a ('EMB a) Free a ('EMB a) g2; Maybe (a :~: a) Nothing -> Bool False Str @strl @a1 Struct c a b s1 Free a a g1 == Str @strr @a2 Struct c a b s2 Free a a g2 = case (forall {k :: Kind} (a :: k) (b :: k). (Typeable a, Typeable b) => Maybe (a :~: b) forall (a :: Kind -> Constraint) (b :: Kind -> Constraint). (Typeable a, Typeable b) => Maybe (a :~: b) eqT @strl @strr, forall {k :: Kind} (a :: k) (b :: k). (Typeable a, Typeable b) => Maybe (a :~: b) forall (a :: FREE cs p) (b :: FREE cs p). (Typeable a, Typeable b) => Maybe (a :~: b) eqT @a1 @a2) of (Just c :~: c Refl, Just a :~: a Refl) -> Struct c a b s1 Struct c a b -> Struct c a b -> Bool forall (a :: Kind). Eq a => a -> a -> Bool == Struct c a b Struct c a b s2 Bool -> Bool -> Bool && Free a a g1 Free a a -> Free a a -> Bool forall (a :: Kind). Eq a => a -> a -> Bool == Free a a Free a a g2 (Maybe (c :~: c), Maybe (a :~: a)) _ -> Bool False Free a b _ == Free a b _ = Bool False class (Show2 p) => WithShow (a :: FREE c (p :: CAT j)) instance (Show2 p) => WithShow (a :: FREE c (p :: CAT j)) instance (WithShow a) => Show (Free a b) where showsPrec :: Int -> Free a b -> ShowS showsPrec Int _ Free a b Id = String -> ShowS P.showString String "id" showsPrec Int d (Emb p a b p Free a ('EMB a) g) = (Char -> Char) -> ShowS forall (a :: Kind) (b :: Kind). (a -> b) -> [a] -> [b] P.map Char -> Char toLower ShowS -> ShowS -> ShowS forall (b :: Kind) (c :: Kind) (a :: Kind). (b -> c) -> (a -> b) -> a -> c forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . Int -> p a b -> Free a ('EMB a) -> ShowS forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j} (p :: Kind) (a :: FREE cs p) (b :: FREE cs p). (Show p, WithShow a) => Int -> p -> Free a b -> ShowS showPostComp Int d p a b p Free a ('EMB a) g showsPrec Int d (Str Struct c a b s Free a a g) = (Char -> Char) -> ShowS forall (a :: Kind) (b :: Kind). (a -> b) -> [a] -> [b] P.map Char -> Char toLower ShowS -> ShowS -> ShowS forall (b :: Kind) (c :: Kind) (a :: Kind). (b -> c) -> (a -> b) -> a -> c forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . Int -> Struct c a b -> Free a a -> ShowS forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j} (p :: Kind) (a :: FREE cs p) (b :: FREE cs p). (Show p, WithShow a) => Int -> p -> Free a b -> ShowS showPostComp Int d Struct c a b s Free a a g showPostComp :: (Show p, WithShow a) => P.Int -> p -> Free a b -> P.ShowS showPostComp :: forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j} (p :: Kind) (a :: FREE cs p) (b :: FREE cs p). (Show p, WithShow a) => Int -> p -> Free a b -> ShowS showPostComp Int d p p Free a b Id = Int -> p -> ShowS forall (a :: Kind). Show a => Int -> a -> ShowS P.showsPrec Int d p p showPostComp Int d p p Free a b g = Bool -> ShowS -> ShowS P.showParen (Int d Int -> Int -> Bool forall (a :: Kind). Ord a => a -> a -> Bool P.> Int 9) (Int -> p -> ShowS forall (a :: Kind). Show a => Int -> a -> ShowS P.showsPrec Int 10 p p ShowS -> ShowS -> ShowS forall (b :: Kind) (c :: Kind) (a :: Kind). (b -> c) -> (a -> b) -> a -> c forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . String -> ShowS P.showString String " . " ShowS -> ShowS -> ShowS forall (b :: Kind) (c :: Kind) (a :: Kind). (b -> c) -> (a -> b) -> a -> c forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . Int -> Free a b -> ShowS forall (a :: Kind). Show a => Int -> a -> ShowS P.showsPrec Int 10 Free a b g) type IsFreeOb :: forall {j} {cs :: [Kind -> Constraint]} {p :: CAT j}. FREE cs p -> Constraint class IsFreeOb (a :: FREE cs (p :: CAT j)) where type Lower (f :: j +-> k) (a :: FREE cs p) :: k withLowerOb :: forall {k} (f :: j +-> k) r . (Representable f, All cs k) => ((Ob (Lower f (a :: FREE cs p))) => r) -> r instance (Ob a, Typeable a) => IsFreeOb (EMB a) where type Lower f (EMB a) = f % a withLowerOb :: forall {k :: Kind} (f :: j +-> k) (r :: Kind). (Representable f, All cs k) => (Ob (Lower f ('EMB a)) => r) -> r withLowerOb @f Ob (Lower f ('EMB a)) => r r = forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: j) (r :: Kind). (Representable p, Ob a) => (Ob (p % a) => r) -> r forall (p :: j +-> k) (a :: j) (r :: Kind). (Representable p, Ob a) => (Ob (p % a) => r) -> r withRepOb @f @a r Ob (f % a) => r Ob (Lower f ('EMB a)) => r r class ((Ok cs p, Eq2 p) => Eq2 str, (Ok cs p) => Typeable str, Show2 p => Show2 str) => CanEqShow (str :: CAT (FREE cs p)) instance ((Ok cs p, Eq2 p) => Eq2 str, (Ok cs p) => Typeable str, Show2 p => Show2 str) => CanEqShow (str :: CAT (FREE cs p)) class (Typeable c, CanEqShow (Struct c :: CAT (FREE cs p)), c `Elem` cs) => HasStructure cs (p :: CAT j) (c :: Kind -> Constraint) where data Struct c :: CAT (FREE cs p) foldStructure :: forall {k} (f :: j +-> k) (a :: FREE cs p) (b :: FREE cs p) . (All cs k, Representable f) => (forall (x :: FREE cs p) y. x ~> y -> Lower f x ~> Lower f y) -> Struct c a b -> Lower f a ~> Lower f b fold :: forall {j} {k} {p :: CAT j} (cs :: [Kind -> Constraint]) (f :: j +-> k) (a :: FREE cs p) (b :: FREE cs p) . (All cs k, Representable f) => (forall x y. p x y -> (f % x) ~> (f % y)) -> a ~> b -> Lower f a ~> Lower f b fold :: forall {j :: Kind} {k :: Kind} {p :: CAT j} (cs :: [Kind -> Constraint]) (f :: j +-> k) (a :: FREE cs p) (b :: FREE cs p). (All cs k, Representable f) => (forall (x :: j) (y :: j). p x y -> (f % x) ~> (f % y)) -> (a ~> b) -> Lower f a ~> Lower f b fold forall (x :: j) (y :: j). p x y -> (f % x) ~> (f % y) pn = (a ~> b) -> Lower f a ~> Lower f b forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y go where go :: forall (x :: FREE cs p) y. x ~> y -> Lower f x ~> Lower f y go :: forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y go x ~> y Free x y Id = forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j} (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind). (IsFreeOb a, Representable f, All cs k) => (Ob (Lower f a) => r) -> r forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind). (IsFreeOb a, Representable f, All cs k) => (Ob (Lower f a) => r) -> r withLowerOb @x @f Lower f x ~> Lower f x Ob (Lower f x) => Lower f x ~> Lower f x forall (a :: k). Ob a => a ~> a forall {k :: Kind} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a id go (Emb p a b p Free x ('EMB a) g) = p a b -> (f % a) ~> (f % b) forall (x :: j) (y :: j). p x y -> (f % x) ~> (f % y) pn p a b p ((f % a) ~> (f % b)) -> (Lower f x ~> (f % a)) -> Lower f x ~> (f % b) forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . (x ~> 'EMB a) -> Lower f x ~> Lower f ('EMB a) forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y go x ~> 'EMB a Free x ('EMB a) g go (Str Struct c a y s Free x a g) = forall (j :: Kind) (cs :: [Kind -> Constraint]) (p :: CAT j) (c :: Kind -> Constraint) {k :: Kind} (f :: j +-> k) (a :: FREE cs p) (b :: FREE cs p). (HasStructure cs p c, All cs k, Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct c a b -> Lower f a ~> Lower f b foldStructure @_ @_ @_ @_ @f (x ~> y) -> Lower f x ~> Lower f y forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y go Struct c a y s (Lower f a ~> Lower f y) -> (Lower f x ~> Lower f a) -> Lower f x ~> Lower f y forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . (x ~> a) -> Lower f x ~> Lower f a forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y go x ~> a Free x a g retract :: forall {j} {k} cs (f :: j +-> k) a b. (All cs k, Representable f) => (a :: FREE cs InitialProfunctor) ~> b -> Lower f a ~> Lower f b retract :: forall {j :: Kind} {k :: Kind} (cs :: [Kind -> Constraint]) (f :: j +-> k) (a :: FREE cs InitialProfunctor) (b :: FREE cs InitialProfunctor). (All cs k, Representable f) => (a ~> b) -> Lower f a ~> Lower f b retract = forall (cs :: [Kind -> Constraint]) (f :: j +-> k) (a :: FREE cs InitialProfunctor) (b :: FREE cs InitialProfunctor). (All cs k, Representable f) => (forall (x :: j) (y :: j). InitialProfunctor x y -> (f % x) ~> (f % y)) -> (a ~> b) -> Lower f a ~> Lower f b forall {j :: Kind} {k :: Kind} {p :: CAT j} (cs :: [Kind -> Constraint]) (f :: j +-> k) (a :: FREE cs p) (b :: FREE cs p). (All cs k, Representable f) => (forall (x :: j) (y :: j). p x y -> (f % x) ~> (f % y)) -> (a ~> b) -> Lower f a ~> Lower f b fold @cs @f (\case {}) instance (Ok cs p) => CategoryOf (FREE cs p) where type (~>) = Free type Ob a = (IsFreeOb a, Typeable a) instance (Ok cs p) => Promonad (Free :: CAT (FREE cs p)) where id :: forall (a :: FREE cs p). Ob a => Free a a id = Free a a forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j} (a :: FREE cs p). Ob a => Free a a Id Free b c Id . :: forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p). Free b c -> Free a b -> Free a c . Free a b g = Free a b Free a c g Free b c f . Free a b Id = Free b c Free a c f Emb p a b p Free b ('EMB a) f . Free a b g = p a b -> Free a ('EMB a) -> Free a ('EMB b) forall {j :: Kind} (c :: j) (a :: j) (p :: j -> j -> Kind) (cs :: [Kind -> Constraint]) (i :: FREE cs p). (Ob c, Ob a, Typeable c, Typeable a) => p c a -> Free i ('EMB c) -> Free i ('EMB a) Emb p a b p (Free b ('EMB a) f Free b ('EMB a) -> Free a b -> Free a ('EMB a) forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p). Free b c -> Free a b -> Free a c . Free a b g) Str Struct c a c s Free b a f . Free a b g = Struct c a c -> Free a a -> Free a c forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j} (c :: Kind -> Constraint) (a :: FREE cs p) (b :: FREE cs p) (i :: FREE cs p). (HasStructure cs p c, Ob a, Ob b) => Struct c a b -> Free i a -> Free i b Str Struct c a c s (Free b a f Free b a -> Free a b -> Free a a forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p). Free b c -> Free a b -> Free a c . Free a b g) instance (Ok cs p) => Profunctor (Free :: CAT (FREE cs p)) where dimap :: forall (c :: FREE cs p) (a :: FREE cs p) (b :: FREE cs p) (d :: FREE cs p). (c ~> a) -> (b ~> d) -> Free a b -> Free c d dimap = (c ~> a) -> (b ~> d) -> Free a b -> Free c d Free c a -> Free b d -> Free a b -> Free c d forall {k :: Kind} (p :: k +-> k) (c :: k) (a :: k) (b :: k) (d :: k). Promonad p => p c a -> p b d -> p a b -> p c d dimapDefault (Ob a, Ob b) => r r \\ :: forall (a :: FREE cs p) (b :: FREE cs p) (r :: Kind). ((Ob a, Ob b) => r) -> Free a b -> r \\ Free a b Id = r (Ob a, Ob b) => r r (Ob a, Ob b) => r r \\ Emb p a b _ Free a ('EMB a) f = r (Ob a, Ob b) => r (Ob a, Ob ('EMB a)) => r r ((Ob a, Ob ('EMB a)) => r) -> Free a ('EMB a) -> r forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j) (r :: Kind). Profunctor p => ((Ob a, Ob b) => r) -> p a b -> r forall (a :: FREE cs p) (b :: FREE cs p) (r :: Kind). ((Ob a, Ob b) => r) -> Free a b -> r \\ Free a ('EMB a) f (Ob a, Ob b) => r r \\ Str Struct c a b _ Free a a f = r (Ob a, Ob b) => r (Ob a, Ob a) => r r ((Ob a, Ob a) => r) -> Free a a -> r forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j) (r :: Kind). Profunctor p => ((Ob a, Ob b) => r) -> p a b -> r forall (a :: FREE cs p) (b :: FREE cs p) (r :: Kind). ((Ob a, Ob b) => r) -> Free a b -> r \\ Free a a f