{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
module Data.Universe.Some (
UniverseSome (..),
FiniteSome (..),
) where
import Data.Functor.Sum (Sum (..))
import Data.List (genericLength)
import Data.Some (Some (..))
import Data.Universe.Class (Universe (..), Finite (..))
import Data.Universe.Helpers (Tagged (..), Natural, (+++))
#if MIN_VERSION_base(4,7,0)
import Data.Type.Equality ((:~:) (..))
#else
import Data.GADT.Compare ((:=) (..))
#endif
-------------------------------------------------------------------------------
-- 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.
--
class UniverseSome f where
universeSome :: [Some f]
class UniverseSome f => FiniteSome f where
universeFSome :: [Some f]
universeFSome = universeSome
cardinalitySome :: Tagged (Some f) Natural
cardinalitySome = Tagged (genericLength (universeFSome :: [Some f]))
-------------------------------------------------------------------------------
-- Helpers
-------------------------------------------------------------------------------
#if MIN_VERSION_dependent_sum(0,5,0)
mkSome :: f a -> Some f
mkSome = Some
mapSome :: (forall x. f x -> g x) -> Some f -> Some g
mapSome nt (Some f) = Some (nt f)
#else
mkSome :: f a -> Some f
mkSome = This
mapSome :: (forall x. f x -> g x) -> Some f -> Some g
mapSome nt (This f) = This (nt f)
#endif
-------------------------------------------------------------------------------
-- Instances for Some
-------------------------------------------------------------------------------
instance UniverseSome f => Universe (Some f) where
universe = universeSome
instance FiniteSome f => Finite (Some f) where
universeF = universeFSome
cardinality = cardinalitySome
-------------------------------------------------------------------------------
-- Type equality is singleton
-------------------------------------------------------------------------------
#if MIN_VERSION_base(4,7,0)
instance UniverseSome ((:~:) a) where
universeSome = [mkSome Refl]
instance FiniteSome ((:~:) a) where
cardinalitySome = 1
#else
instance UniverseSome ((:=) a) where
universeSome = [mkSome Refl]
instance FiniteSome ((:=) a) where
cardinalitySome = 1
#endif
-------------------------------------------------------------------------------
-- Functors
-------------------------------------------------------------------------------
instance (UniverseSome f, UniverseSome g) => UniverseSome (Sum f g) where
universeSome = map (mapSome InL) universeSome +++ map (mapSome InR) universeSome
instance (FiniteSome f, FiniteSome g) => FiniteSome (Sum f g) where
universeFSome = map (mapSome InL) universeFSome ++ map (mapSome InR) 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.