{-# 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