{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
#if __GLASGOW_HASKELL__ >=704 && MIN_VERSION_base(4,9,0)
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >=702
{-# LANGUAGE Trustworthy #-}
#endif
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 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]))
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 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 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 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 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 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 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 :: 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
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
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 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 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 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 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