{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}

module Data.Some.Constraint
(
  -- * Combining constraints
  AllC

  -- * Existentials
  -- ** Flat existentials
  , Somes(..), Some

  -- ** Containerized existentials
  -- *** Constrained containers
  , Somes1(..), Some1

  -- *** Fixed containers
  , SomesF, SomeF
  , mapSome, (<~$>)
  , traverseSome, (<~*>)
) where

import Data.Kind

-- | AllC ensures that a list of 'Constraint's is applied to a poly-kinded 'Type' @k@.
type AllC :: forall k. [k -> Constraint] -> k -> Constraint
type family AllC cs k :: Constraint where
  AllC '[]       k = ()
  AllC (c ': cs) k = (c k, AllC cs k)

-- | Existential with 'Constraint's.
--
-- ==== __Example__
--
-- @
-- someShowableOrd :: 'Somes' '['Show', 'Ord']
-- someShowableOrd = 'Some' ('mempty' :: ['Double'])
-- @
data Somes cs where
  Some :: forall
    (cs :: [Type -> Constraint])
    (a :: Type).
    AllC cs a => a -> Somes cs

instance {-# OVERLAPPING #-} Show (Somes (Show ': cs)) where
  showsPrec :: Int -> Somes (Show : cs) -> ShowS
showsPrec Int
d (Some a
x) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Some " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 a
x

instance {-# OVERLAPPABLE #-} Show (Somes cs) => Show (Somes (c ': cs)) where
  showsPrec :: Int -> Somes (c : cs) -> ShowS
showsPrec Int
d (Some a
x) = Int -> Somes cs -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (forall (cs :: [* -> Constraint]) f. AllC cs f => f -> Somes cs
Some @cs a
x)

-- | Alias for 'Somes' with just one 'Constraint'.
type Some c = Somes '[c]

-- | Existential for containers with 'Constraint's.
--
-- ==== __Example__
--
-- @
-- someNumFunctor :: 'Somes1' '['Functor'] '['Num']
-- someNumFunctor = 'Some1' $ [1, 2, 3 :: 'Int']
-- @
data Somes1 csf csa where
  Some1 :: forall
    k
    (csf :: [(k -> Type) -> Constraint])
    (csa :: [k -> Constraint])
    (f :: k -> Type)
    (a :: k).
    (AllC csf f, AllC csa a) => f a -> Somes1 csf csa

-- | Alias for 'Somes1' with just one 'Constraint'.
type Some1 cf ca = Somes1 '[cf] '[ca]

-- | Alias for 'Somes1' with a container @f@ and multiple 'Constraint's @csa@ for its elements.
type SomesF f csa = Somes1 '[(~) f] csa

-- | Alias for 'SomeF' with just one 'Constraint' for its elements.
type SomeF f c = SomesF f '[c]

-- | Natural transformation of one container to another.
mapSome :: (forall a. AllC csa a => f a -> g a) -> SomesF f csa -> SomesF g csa
mapSome :: forall {k} (csa :: [k -> Constraint]) (f :: k -> *) (g :: k -> *).
(forall (a :: k). AllC csa a => f a -> g a)
-> SomesF f csa -> SomesF g csa
mapSome forall (a :: k). AllC csa a => f a -> g a
f (Some1 f a
x) = g a -> Somes1 '[(~) g] csa
forall k (csf :: [(k -> *) -> Constraint])
       (csa :: [k -> Constraint]) (f :: k -> *) (a :: k).
(AllC csf f, AllC csa a) =>
f a -> Somes1 csf csa
Some1 (f a -> g a
forall (a :: k). AllC csa a => f a -> g a
f f a
f a
x)

infixl 4 <~$>
-- | Infix version of 'mapSome'.
(<~$>) :: (forall a. AllC csa a => f a -> g a) -> SomesF f csa -> SomesF g csa
<~$> :: forall {k} (csa :: [k -> Constraint]) (f :: k -> *) (g :: k -> *).
(forall (a :: k). AllC csa a => f a -> g a)
-> SomesF f csa -> SomesF g csa
(<~$>) = (forall (a :: k). AllC csa a => f a -> g a)
-> SomesF f csa -> SomesF g csa
forall {k} (csa :: [k -> Constraint]) (f :: k -> *) (g :: k -> *).
(forall (a :: k). AllC csa a => f a -> g a)
-> SomesF f csa -> SomesF g csa
mapSome

-- | Natural transformation of one container to another - with side effects in @m@.
traverseSome :: Functor m => (forall a. AllC csa a => f a -> m (g a)) -> SomesF f csa -> m (SomesF g csa)
traverseSome :: forall {k} (m :: * -> *) (csa :: [k -> Constraint]) (f :: k -> *)
       (g :: k -> *).
Functor m =>
(forall (a :: k). AllC csa a => f a -> m (g a))
-> SomesF f csa -> m (SomesF g csa)
traverseSome forall (a :: k). AllC csa a => f a -> m (g a)
f (Some1 f a
x) = g a -> Somes1 '[(~) g] csa
forall k (csf :: [(k -> *) -> Constraint])
       (csa :: [k -> Constraint]) (f :: k -> *) (a :: k).
(AllC csf f, AllC csa a) =>
f a -> Somes1 csf csa
Some1 (g a -> Somes1 '[(~) g] csa) -> m (g a) -> m (Somes1 '[(~) g] csa)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> m (g a)
forall (a :: k). AllC csa a => f a -> m (g a)
f f a
f a
x

infixl 4 <~*>
-- | Infix version of 'traverseSome'.
(<~*>) :: Functor m => (forall a. AllC csa a => f a -> m (g a)) -> SomesF f csa -> m (SomesF g csa)
<~*> :: forall {k} (m :: * -> *) (csa :: [k -> Constraint]) (f :: k -> *)
       (g :: k -> *).
Functor m =>
(forall (a :: k). AllC csa a => f a -> m (g a))
-> SomesF f csa -> m (SomesF g csa)
(<~*>) = (forall (a :: k). AllC csa a => f a -> m (g a))
-> SomesF f csa -> m (SomesF g csa)
forall {k} (m :: * -> *) (csa :: [k -> Constraint]) (f :: k -> *)
       (g :: k -> *).
Functor m =>
(forall (a :: k). AllC csa a => f a -> m (g a))
-> SomesF f csa -> m (SomesF g csa)
traverseSome

instance {-# OVERLAPPING #-} (forall a. Show a => Show (f a)) => Show (SomesF f (Show ': cs)) where
  showsPrec :: Int -> SomesF f (Show : cs) -> ShowS
showsPrec Int
d (Some1 f a
x) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Some " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 f a
x

instance {-# OVERLAPPABLE #-} Show (SomesF f cs) => Show (SomesF f (c ': cs)) where
  showsPrec :: Int -> SomesF f (c : cs) -> ShowS
showsPrec Int
d (Some1 f a
x) = Int -> SomesF f cs -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (forall k (csf :: [(k -> *) -> Constraint])
       (csa :: [k -> Constraint]) (f :: k -> *) (a :: k).
(AllC csf f, AllC csa a) =>
f a -> Somes1 csf csa
Some1 @_ @('[(~) f]) @cs f a
x)