{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
module Data.Universe.Some (
  UniverseSome (..),
  FiniteSome (..),
  ) where

import Data.Functor.Sum (Sum (..))
import Data.List (genericLength)
import Data.Some (Some, mapSome, mkSome, foldSome)
import Data.Type.Equality ((:~:) (..))
import Data.Universe.Class (Universe (..), Finite (..))
import Data.Universe.Helpers (Tagged (..), Natural, (+++))

import qualified Data.Some.GADT as G
import qualified Data.Some.Newtype as N
import qualified Data.Some.Church as C

-------------------------------------------------------------------------------
-- Class
-------------------------------------------------------------------------------

-- | Auxiliary class to power @'Universe' ('Some' f)@ instance.
-- (There are no good reasons to use @FlexibleInstances@).
--
-- Laws are induced via @'Universe' ('Some' f)@ instance. For example:
--
-- @
-- 'elem' x 'universe' ==> 'elem' ('Some' f) 'universeSome'
-- @
--
-- As 'Data.GADT.Compare.GEq' cannot be written for phantom 'Functor's, e.g.
-- 'Control.Applicative.Const' or 'Data.Proxy.Proxy', they cannot have
-- 'UniverseSome' instance either.
--
-- /Note:/ The 'Some' type is imported from "Data.Some", i.e. maybe
-- either from "Data.Some.Newtype" (default) or "Data.Some.GADT" modules.
--
class UniverseSome f where
  universeSome :: [Some f]

class UniverseSome f => FiniteSome f where
  universeFSome :: [Some f]
  universeFSome = [Some f]
forall (f :: * -> *). UniverseSome f => [Some f]
universeSome

  cardinalitySome :: Tagged (Some f) Natural
  cardinalitySome = Natural -> Tagged (Some f) Natural
forall {k} (s :: k) b. b -> Tagged s b
Tagged ([Some f] -> Natural
forall i a. Num i => [a] -> i
genericLength ([Some f]
forall (f :: * -> *). FiniteSome f => [Some f]
universeFSome :: [Some f]))

-------------------------------------------------------------------------------
-- Instances for Some
-------------------------------------------------------------------------------

instance UniverseSome f => Universe (N.Some f) where
  universe :: [Some f]
universe = (Some f -> Some f) -> [Some f] -> [Some f]
forall a b. (a -> b) -> [a] -> [b]
map ((forall a. f a -> Some f) -> Some f -> Some f
forall {k} (tag :: k -> *) b.
(forall (a :: k). tag a -> b) -> Some tag -> b
foldSome f a -> Some f
forall a. f a -> Some f
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
N.mkSome) [Some f]
forall (f :: * -> *). UniverseSome f => [Some f]
universeSome

instance FiniteSome f => Finite (N.Some f) where
  universeF :: [Some f]
universeF   = (Some f -> Some f) -> [Some f] -> [Some f]
forall a b. (a -> b) -> [a] -> [b]
map ((forall a. f a -> Some f) -> Some f -> Some f
forall {k} (tag :: k -> *) b.
(forall (a :: k). tag a -> b) -> Some tag -> b
foldSome f a -> Some f
forall a. f a -> Some f
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
N.mkSome) [Some f]
forall (f :: * -> *). FiniteSome f => [Some f]
universeFSome
  cardinality :: Tagged (Some f) Natural
cardinality = Tagged (Some f) Natural -> Tagged (Some f) Natural
forall (f :: * -> *) (some :: (* -> *) -> *).
Tagged (Some f) Natural -> Tagged (some f) Natural
retagSome Tagged (Some f) Natural
forall (f :: * -> *). FiniteSome f => Tagged (Some f) Natural
cardinalitySome

instance UniverseSome f => Universe (G.Some f) where
  universe :: [Some f]
universe =  (Some f -> Some f) -> [Some f] -> [Some f]
forall a b. (a -> b) -> [a] -> [b]
map ((forall a. f a -> Some f) -> Some f -> Some f
forall {k} (tag :: k -> *) b.
(forall (a :: k). tag a -> b) -> Some tag -> b
foldSome f a -> Some f
forall a. f a -> Some f
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
G.mkSome) [Some f]
forall (f :: * -> *). UniverseSome f => [Some f]
universeSome

instance FiniteSome f => Finite (G.Some f) where
  universeF :: [Some f]
universeF   = (Some f -> Some f) -> [Some f] -> [Some f]
forall a b. (a -> b) -> [a] -> [b]
map ((forall a. f a -> Some f) -> Some f -> Some f
forall {k} (tag :: k -> *) b.
(forall (a :: k). tag a -> b) -> Some tag -> b
foldSome f a -> Some f
forall a. f a -> Some f
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
G.mkSome) [Some f]
forall (f :: * -> *). FiniteSome f => [Some f]
universeFSome
  cardinality :: Tagged (Some f) Natural
cardinality = Tagged (Some f) Natural -> Tagged (Some f) Natural
forall (f :: * -> *) (some :: (* -> *) -> *).
Tagged (Some f) Natural -> Tagged (some f) Natural
retagSome Tagged (Some f) Natural
forall (f :: * -> *). FiniteSome f => Tagged (Some f) Natural
cardinalitySome

instance UniverseSome f => Universe (C.Some f) where
  universe :: [Some f]
universe =  (Some f -> Some f) -> [Some f] -> [Some f]
forall a b. (a -> b) -> [a] -> [b]
map ((forall a. f a -> Some f) -> Some f -> Some f
forall {k} (tag :: k -> *) b.
(forall (a :: k). tag a -> b) -> Some tag -> b
foldSome f a -> Some f
forall a. f a -> Some f
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
C.mkSome) [Some f]
forall (f :: * -> *). UniverseSome f => [Some f]
universeSome

instance FiniteSome f => Finite (C.Some f) where
  universeF :: [Some f]
universeF   = (Some f -> Some f) -> [Some f] -> [Some f]
forall a b. (a -> b) -> [a] -> [b]
map ((forall a. f a -> Some f) -> Some f -> Some f
forall {k} (tag :: k -> *) b.
(forall (a :: k). tag a -> b) -> Some tag -> b
foldSome f a -> Some f
forall a. f a -> Some f
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
C.mkSome) [Some f]
forall (f :: * -> *). FiniteSome f => [Some f]
universeFSome
  cardinality :: Tagged (Some f) Natural
cardinality = Tagged (Some f) Natural -> Tagged (Some f) Natural
forall (f :: * -> *) (some :: (* -> *) -> *).
Tagged (Some f) Natural -> Tagged (some f) Natural
retagSome Tagged (Some f) Natural
forall (f :: * -> *). FiniteSome f => Tagged (Some f) Natural
cardinalitySome

retagSome :: Tagged (Some f) Natural -> Tagged (some f) Natural
retagSome :: forall (f :: * -> *) (some :: (* -> *) -> *).
Tagged (Some f) Natural -> Tagged (some f) Natural
retagSome (Tagged Natural
n) = Natural -> Tagged (some f) Natural
forall {k} (s :: k) b. b -> Tagged s b
Tagged Natural
n

-------------------------------------------------------------------------------
-- Type equality is singleton
-------------------------------------------------------------------------------

instance UniverseSome ((:~:) a) where
  universeSome :: [Some ((:~:) a)]
universeSome = [(a :~: a) -> Some ((:~:) a)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
mkSome a :~: a
forall {k} (a :: k). a :~: a
Refl]

instance FiniteSome ((:~:) a) where
  cardinalitySome :: Tagged (Some ((:~:) a)) Natural
cardinalitySome = Tagged (Some ((:~:) a)) Natural
1

-------------------------------------------------------------------------------
-- Functors
-------------------------------------------------------------------------------

instance (UniverseSome f, UniverseSome g) => UniverseSome (Sum f g) where
  universeSome :: [Some (Sum f g)]
universeSome = (Some f -> Some (Sum f g)) -> [Some f] -> [Some (Sum f g)]
forall a b. (a -> b) -> [a] -> [b]
map ((forall t. f t -> Sum f g t) -> Some f -> Some (Sum f g)
forall {k} (f :: k -> *) (g :: k -> *).
(forall (t :: k). f t -> g t) -> Some f -> Some g
mapSome f t -> Sum f g t
forall t. f t -> Sum f g t
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL) [Some f]
forall (f :: * -> *). UniverseSome f => [Some f]
universeSome [Some (Sum f g)] -> [Some (Sum f g)] -> [Some (Sum f g)]
forall a. [a] -> [a] -> [a]
+++ (Some g -> Some (Sum f g)) -> [Some g] -> [Some (Sum f g)]
forall a b. (a -> b) -> [a] -> [b]
map ((forall t. g t -> Sum f g t) -> Some g -> Some (Sum f g)
forall {k} (f :: k -> *) (g :: k -> *).
(forall (t :: k). f t -> g t) -> Some f -> Some g
mapSome g t -> Sum f g t
forall t. g t -> Sum f g t
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR) [Some g]
forall (f :: * -> *). UniverseSome f => [Some f]
universeSome

instance (FiniteSome f, FiniteSome g) => FiniteSome (Sum f g) where
  universeFSome :: [Some (Sum f g)]
universeFSome = (Some f -> Some (Sum f g)) -> [Some f] -> [Some (Sum f g)]
forall a b. (a -> b) -> [a] -> [b]
map ((forall t. f t -> Sum f g t) -> Some f -> Some (Sum f g)
forall {k} (f :: k -> *) (g :: k -> *).
(forall (t :: k). f t -> g t) -> Some f -> Some g
mapSome f t -> Sum f g t
forall t. f t -> Sum f g t
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL) [Some f]
forall (f :: * -> *). FiniteSome f => [Some f]
universeFSome [Some (Sum f g)] -> [Some (Sum f g)] -> [Some (Sum f g)]
forall a. [a] -> [a] -> [a]
++ (Some g -> Some (Sum f g)) -> [Some g] -> [Some (Sum f g)]
forall a b. (a -> b) -> [a] -> [b]
map ((forall t. g t -> Sum f g t) -> Some g -> Some (Sum f g)
forall {k} (f :: k -> *) (g :: k -> *).
(forall (t :: k). f t -> g t) -> Some f -> Some g
mapSome g t -> Sum f g t
forall t. g t -> Sum f g t
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR) [Some g]
forall (f :: * -> *). FiniteSome f => [Some f]
universeFSome

-- Note: Product instance is tricky, we could for special cases.
-- e.g. '(GEq f, f ~ g) => UnvierseSome (Product f g)', but this is boring
-- instance as we'd 'Pair' equal instances only.