{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Working with objects through their identity arrows: 'Obj' @a@ is @a '~>' a@ used as a witness that
-- @a@ is an object, with 'obj', 'src' and 'tgt' to produce them and the 'Obj'\/'Objs' pattern synonyms
-- to recover 'Ob' constraints from arrows and profunctor values.
module Proarrow.Object
  ( Obj
  , pattern Obj
  , pattern Objs
  , obj
  , src
  , tgt
  , Ob'
  , VacuousOb
  , objDicts
  , ObjDict (..)

    -- * Lists of objects
  , type (++)
  , ListOf (..)
  , KnownListOf (..)
  , withKnownListOf
  , mapListOf
  , lengthListOf
  , appendListOf
  , withKnownAppend
  , withKnownAssoc
  , eqListOf

    -- * One object of many
  , SomeOf (..)
  , someOfList
  , withListOf
  , someRepOf
  ) where

import Data.Kind (Constraint, Type)
import Data.Type.Equality ((:~:) (..))
import Type.Reflection (SomeTypeRep (..), Typeable, typeRep)
import Prelude (Int, (+))
import Prelude qualified as P

import Proarrow.Core (CategoryOf (..), OB, Ob', Obj, Profunctor, VacuousOb, obj, src, tgt, (\\), type (:&&:))

type ObjDict :: forall {k}. k -> Type
data ObjDict a where
  ObjDict :: (Ob a) => ObjDict a

objDicts :: (Profunctor p) => p a a' -> (ObjDict a, ObjDict a')
objDicts :: forall {k} {k} (p :: k +-> k) (a :: k) (a' :: k).
Profunctor p =>
p a a' -> (ObjDict a, ObjDict a')
objDicts p a a'
a = (ObjDict a
(Ob a, Ob a') => ObjDict a
forall {k} (a :: k). Ob a => ObjDict a
ObjDict ((Ob a, Ob a') => ObjDict a) -> p a a' -> ObjDict a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a a'
a, ObjDict a'
(Ob a, Ob a') => ObjDict a'
forall {k} (a :: k). Ob a => ObjDict a
ObjDict ((Ob a, Ob a') => ObjDict a') -> p a a' -> ObjDict a'
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a a'
a)

pattern Obj :: (CategoryOf k) => (Ob (a :: k)) => Obj a
pattern $bObj :: forall k (a :: k). (CategoryOf k, Ob a) => Obj a
$mObj :: forall {r} {k} {a :: k}.
CategoryOf k =>
Obj a -> (Ob a => r) -> ((# #) -> r) -> r
Obj <- (objDicts -> (ObjDict, ObjDict))
  where
    Obj = Obj a
forall k (a :: k). (CategoryOf k, Ob a) => Obj a
obj

{-# COMPLETE Obj #-}

-- | Matching a profunctor value @p a b@ against 'Objs' brings @('Ob' a, 'Ob' b)@ into scope. This
-- is the pattern form of '(\\)', handy in function equations.
pattern Objs :: (Profunctor p) => (Ob a, Ob b) => p a b
pattern $mObjs :: forall {r} {j} {k} {p :: j +-> k} {a :: k} {b :: j}.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> ((# #) -> r) -> r
Objs <- (objDicts -> (ObjDict, ObjDict))

{-# COMPLETE Objs #-}

-- | A type-level list with the evidence @c@ for each element, as a value.
type ListOf :: forall {k}. OB k -> [k] -> Type
data ListOf c xs where
  Nil :: ListOf c '[]
  Cons :: forall {k} {c :: OB k} (x :: k) xs. (c x) => ListOf c xs -> ListOf c (x ': xs)

-- | A type-level list whose elements have the evidence @c@, as its 'ListOf'.
type KnownListOf :: forall {k}. OB k -> [k] -> Constraint
class KnownListOf c xs where
  listOf :: ListOf c xs

instance KnownListOf c '[] where
  listOf :: ListOf c '[]
listOf = ListOf c '[]
forall k (c :: OB k). ListOf c '[]
Nil
instance (c x, KnownListOf c xs) => KnownListOf c (x ': xs) where
  listOf :: ListOf c (x : xs)
listOf = forall (x :: a) (xs :: [a]).
c x =>
ListOf c xs -> ListOf c (x : xs)
forall {k} {c :: OB k} (x :: k) (xs :: [k]).
c x =>
ListOf c xs -> ListOf c (x : xs)
Cons @x ListOf c xs
forall {k} (c :: OB k) (xs :: [k]). KnownListOf c xs => ListOf c xs
listOf

-- | The class from the list.
withKnownListOf :: ListOf c xs -> ((KnownListOf c xs) => r) -> r
withKnownListOf :: forall {k} (c :: OB k) (xs :: [k]) r.
ListOf c xs -> (KnownListOf c xs => r) -> r
withKnownListOf ListOf c xs
Nil KnownListOf c xs => r
r = r
KnownListOf c xs => r
r
withKnownListOf (Cons ListOf c xs
rest) KnownListOf c xs => r
r = ListOf c xs -> (KnownListOf c xs => r) -> r
forall {k} (c :: OB k) (xs :: [k]) r.
ListOf c xs -> (KnownListOf c xs => r) -> r
withKnownListOf ListOf c xs
rest r
KnownListOf c xs => r
KnownListOf c xs => r
r

-- | A value for each element, in order.
mapListOf :: forall {k} (c :: OB k) xs r. (forall (x :: k). (c x) => r) -> ListOf c xs -> [r]
mapListOf :: forall {k} (c :: OB k) (xs :: [k]) r.
(forall (x :: k). c x => r) -> ListOf c xs -> [r]
mapListOf forall (x :: k). c x => r
_ ListOf c xs
Nil = []
mapListOf forall (x :: k). c x => r
f (Cons @x ListOf c xs
rest) = forall (x :: k). c x => r
f @x r -> [r] -> [r]
forall a. a -> [a] -> [a]
: forall {k} (c :: OB k) (xs :: [k]) r.
(forall (x :: k). c x => r) -> ListOf c xs -> [r]
forall (c :: OB k) (xs :: [k]) r.
(forall (x :: k). c x => r) -> ListOf c xs -> [r]
mapListOf @c (\ @y -> forall (x :: k). c x => r
f @y) ListOf c xs
rest

-- | The number of elements.
lengthListOf :: ListOf c xs -> Int
lengthListOf :: forall {k} (c :: OB k) (xs :: [k]). ListOf c xs -> Int
lengthListOf ListOf c xs
Nil = Int
0
lengthListOf (Cons ListOf c xs
rest) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ListOf c xs -> Int
forall {k} (c :: OB k) (xs :: [k]). ListOf c xs -> Int
lengthListOf ListOf c xs
rest

-- | List concatenation.
type (++) :: [k] -> [k] -> [k]
type family as ++ bs where
  '[] ++ bs = bs
  (a ': as) ++ bs = a ': (as ++ bs)

-- | Whether two lists have the same elements, given how to decide that for one element.
eqListOf
  :: forall {k} (c :: OB k) as bs
   . (forall (x :: k) (y :: k). (c x, c y) => P.Maybe (x :~: y))
  -> ListOf c as
  -> ListOf c bs
  -> P.Maybe (as :~: bs)
eqListOf :: forall {k} (c :: OB k) (as :: [k]) (bs :: [k]).
(forall (x :: k) (y :: k). (c x, c y) => Maybe (x :~: y))
-> ListOf c as -> ListOf c bs -> Maybe (as :~: bs)
eqListOf forall (x :: k) (y :: k). (c x, c y) => Maybe (x :~: y)
_ ListOf c as
Nil ListOf c bs
Nil = (as :~: bs) -> Maybe (as :~: bs)
forall a. a -> Maybe a
P.Just as :~: as
as :~: bs
forall {k} (a :: k). a :~: a
Refl
eqListOf forall (x :: k) (y :: k). (c x, c y) => Maybe (x :~: y)
eq (Cons @x ListOf c xs
xs) (Cons @y ListOf c xs
ys) = case (forall (x :: k) (y :: k). (c x, c y) => Maybe (x :~: y)
eq @x @y, forall {k} (c :: OB k) (as :: [k]) (bs :: [k]).
(forall (x :: k) (y :: k). (c x, c y) => Maybe (x :~: y))
-> ListOf c as -> ListOf c bs -> Maybe (as :~: bs)
forall (c :: OB k) (as :: [k]) (bs :: [k]).
(forall (x :: k) (y :: k). (c x, c y) => Maybe (x :~: y))
-> ListOf c as -> ListOf c bs -> Maybe (as :~: bs)
eqListOf @c Maybe (x :~: y)
forall (x :: k) (y :: k). (c x, c y) => Maybe (x :~: y)
eq ListOf c xs
xs ListOf c xs
ys) of
  (P.Just x :~: x
Refl, P.Just xs :~: xs
Refl) -> (as :~: bs) -> Maybe (as :~: bs)
forall a. a -> Maybe a
P.Just as :~: as
as :~: bs
forall {k} (a :: k). a :~: a
Refl
  (Maybe (x :~: x), Maybe (xs :~: xs))
_ -> Maybe (as :~: bs)
forall a. Maybe a
P.Nothing
eqListOf forall (x :: k) (y :: k). (c x, c y) => Maybe (x :~: y)
_ ListOf c as
_ ListOf c bs
_ = Maybe (as :~: bs)
forall a. Maybe a
P.Nothing

-- | The elements of both lists.
appendListOf :: ListOf c as -> ListOf c bs -> ListOf c (as ++ bs)
appendListOf :: forall {k} (c :: OB k) (as :: [k]) (bs :: [k]).
ListOf c as -> ListOf c bs -> ListOf c (as ++ bs)
appendListOf ListOf c as
Nil ListOf c bs
ys = ListOf c bs
ListOf c (as ++ bs)
ys
appendListOf (Cons @x ListOf c xs
xs) ListOf c bs
ys = forall (x :: k) (xs :: [k]).
c x =>
ListOf c xs -> ListOf c (x : xs)
forall {k} {c :: OB k} (x :: k) (xs :: [k]).
c x =>
ListOf c xs -> ListOf c (x : xs)
Cons @x (ListOf c xs -> ListOf c bs -> ListOf c (xs ++ bs)
forall {k} (c :: OB k) (as :: [k]) (bs :: [k]).
ListOf c as -> ListOf c bs -> ListOf c (as ++ bs)
appendListOf ListOf c xs
xs ListOf c bs
ys)

-- | The class for the elements of both lists.
withKnownAppend
  :: forall {k} (c :: OB k) as bs r. (KnownListOf c as, KnownListOf c bs) => ((KnownListOf c (as ++ bs)) => r) -> r
withKnownAppend :: forall {k} (c :: OB k) (as :: [k]) (bs :: [k]) r.
(KnownListOf c as, KnownListOf c bs) =>
(KnownListOf c (as ++ bs) => r) -> r
withKnownAppend = ListOf c (as ++ bs) -> (KnownListOf c (as ++ bs) => r) -> r
forall {k} (c :: OB k) (xs :: [k]) r.
ListOf c xs -> (KnownListOf c xs => r) -> r
withKnownListOf (ListOf c as -> ListOf c bs -> ListOf c (as ++ bs)
forall {k} (c :: OB k) (as :: [k]) (bs :: [k]).
ListOf c as -> ListOf c bs -> ListOf c (as ++ bs)
appendListOf (forall {k} (c :: OB k) (xs :: [k]). KnownListOf c xs => ListOf c xs
forall (c :: OB k) (xs :: [k]). KnownListOf c xs => ListOf c xs
listOf @c @as) (forall {k} (c :: OB k) (xs :: [k]). KnownListOf c xs => ListOf c xs
forall (c :: OB k) (xs :: [k]). KnownListOf c xs => ListOf c xs
listOf @c @bs))

-- | The class for the elements of three lists, appended either way round.
withKnownAssoc
  :: forall {k} (c :: OB k) as bs cs r
   . (KnownListOf c as, KnownListOf c bs, KnownListOf c cs)
  => ((KnownListOf c ((as ++ bs) ++ cs), KnownListOf c (as ++ (bs ++ cs))) => r) -> r
withKnownAssoc :: forall {k} (c :: OB k) (as :: [k]) (bs :: [k]) (cs :: [k]) r.
(KnownListOf c as, KnownListOf c bs, KnownListOf c cs) =>
((KnownListOf c ((as ++ bs) ++ cs),
  KnownListOf c (as ++ (bs ++ cs))) =>
 r)
-> r
withKnownAssoc (KnownListOf c ((as ++ bs) ++ cs),
 KnownListOf c (as ++ (bs ++ cs))) =>
r
r =
  forall {k} (c :: OB k) (as :: [k]) (bs :: [k]) r.
(KnownListOf c as, KnownListOf c bs) =>
(KnownListOf c (as ++ bs) => r) -> r
forall (c :: OB k) (as :: [k]) (bs :: [k]) r.
(KnownListOf c as, KnownListOf c bs) =>
(KnownListOf c (as ++ bs) => r) -> r
withKnownAppend @c @as @bs
    (forall {k} (c :: OB k) (as :: [k]) (bs :: [k]) r.
(KnownListOf c as, KnownListOf c bs) =>
(KnownListOf c (as ++ bs) => r) -> r
forall (c :: OB k) (as :: [k]) (bs :: [k]) r.
(KnownListOf c as, KnownListOf c bs) =>
(KnownListOf c (as ++ bs) => r) -> r
withKnownAppend @c @(as ++ bs) @cs (forall {k} (c :: OB k) (as :: [k]) (bs :: [k]) r.
(KnownListOf c as, KnownListOf c bs) =>
(KnownListOf c (as ++ bs) => r) -> r
forall (c :: OB k) (as :: [k]) (bs :: [k]) r.
(KnownListOf c as, KnownListOf c bs) =>
(KnownListOf c (as ++ bs) => r) -> r
withKnownAppend @c @bs @cs (forall {k} (c :: OB k) (as :: [k]) (bs :: [k]) r.
(KnownListOf c as, KnownListOf c bs) =>
(KnownListOf c (as ++ bs) => r) -> r
forall (c :: OB k) (as :: [k]) (bs :: [k]) r.
(KnownListOf c as, KnownListOf c bs) =>
(KnownListOf c (as ++ bs) => r) -> r
withKnownAppend @c @as @(bs ++ cs) r
KnownListOf c (as ++ (bs ++ cs)) => r
(KnownListOf c ((as ++ bs) ++ cs),
 KnownListOf c (as ++ (bs ++ cs))) =>
r
r)))

-- | Some type with the evidence @c@, which one known only at runtime.
type SomeOf :: forall {k}. OB k -> Type
data SomeOf c where
  Some :: forall {k} {c :: OB k} (x :: k). (c x) => SomeOf c

-- | The elements of the list, each on its own.
someOfList :: forall {k} (c :: OB k) xs. ListOf c xs -> [SomeOf c]
someOfList :: forall {k} (c :: OB k) (xs :: [k]). ListOf c xs -> [SomeOf c]
someOfList = (forall (x :: k). c x => SomeOf c) -> ListOf c xs -> [SomeOf c]
forall {k} (c :: OB k) (xs :: [k]) r.
(forall (x :: k). c x => r) -> ListOf c xs -> [r]
mapListOf (\ @x -> forall (x :: k). c x => SomeOf c
forall {k} {c :: OB k} (x :: k). c x => SomeOf c
Some @x)

-- | A list of types known at runtime as a type-level list.
withListOf :: forall {k} (c :: OB k) r. [SomeOf c] -> (forall (xs :: [k]). ListOf c xs -> r) -> r
withListOf :: forall {k} (c :: OB k) r.
[SomeOf c] -> (forall (xs :: [k]). ListOf c xs -> r) -> r
withListOf [] forall (xs :: [k]). ListOf c xs -> r
k = ListOf c '[] -> r
forall (xs :: [k]). ListOf c xs -> r
k ListOf c '[]
forall k (c :: OB k). ListOf c '[]
Nil
withListOf (Some @x : [SomeOf c]
rest) forall (xs :: [k]). ListOf c xs -> r
k = [SomeOf c] -> (forall (xs :: [k]). ListOf c xs -> r) -> r
forall {k} (c :: OB k) r.
[SomeOf c] -> (forall (xs :: [k]). ListOf c xs -> r) -> r
withListOf [SomeOf c]
rest (\ListOf c xs
l -> ListOf c (x : xs) -> r
forall (xs :: [k]). ListOf c xs -> r
k (forall (x :: k) (xs :: [k]).
c x =>
ListOf c xs -> ListOf c (x : xs)
forall {k} {c :: OB k} (x :: k) (xs :: [k]).
c x =>
ListOf c xs -> ListOf c (x : xs)
Cons @x ListOf c xs
l))

-- | The type representation of the type, which is what 'SomeOf' values are compared and shown by.
someRepOf :: SomeOf (Typeable :&&: c) -> SomeTypeRep
someRepOf :: forall {k} (c :: OB k). SomeOf (Typeable :&&: c) -> SomeTypeRep
someRepOf (Some @x) = TypeRep x -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep (forall (a :: k). Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @x)

instance P.Eq (SomeOf (Typeable :&&: c)) where
  SomeOf (Typeable :&&: c)
x == :: SomeOf (Typeable :&&: c) -> SomeOf (Typeable :&&: c) -> Bool
== SomeOf (Typeable :&&: c)
y = SomeOf (Typeable :&&: c) -> SomeTypeRep
forall {k} (c :: OB k). SomeOf (Typeable :&&: c) -> SomeTypeRep
someRepOf SomeOf (Typeable :&&: c)
x SomeTypeRep -> SomeTypeRep -> Bool
forall a. Eq a => a -> a -> Bool
P.== SomeOf (Typeable :&&: c) -> SomeTypeRep
forall {k} (c :: OB k). SomeOf (Typeable :&&: c) -> SomeTypeRep
someRepOf SomeOf (Typeable :&&: c)
y
instance P.Ord (SomeOf (Typeable :&&: c)) where
  compare :: SomeOf (Typeable :&&: c) -> SomeOf (Typeable :&&: c) -> Ordering
compare SomeOf (Typeable :&&: c)
x SomeOf (Typeable :&&: c)
y = SomeTypeRep -> SomeTypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
P.compare (SomeOf (Typeable :&&: c) -> SomeTypeRep
forall {k} (c :: OB k). SomeOf (Typeable :&&: c) -> SomeTypeRep
someRepOf SomeOf (Typeable :&&: c)
x) (SomeOf (Typeable :&&: c) -> SomeTypeRep
forall {k} (c :: OB k). SomeOf (Typeable :&&: c) -> SomeTypeRep
someRepOf SomeOf (Typeable :&&: c)
y)
instance P.Show (SomeOf (Typeable :&&: c)) where
  show :: SomeOf (Typeable :&&: c) -> String
show = SomeTypeRep -> String
forall a. Show a => a -> String
P.show (SomeTypeRep -> String)
-> (SomeOf (Typeable :&&: c) -> SomeTypeRep)
-> SomeOf (Typeable :&&: c)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
P.. SomeOf (Typeable :&&: c) -> SomeTypeRep
forall {k} (c :: OB k). SomeOf (Typeable :&&: c) -> SomeTypeRep
someRepOf