{-|
Module: Topology.StoneSpace
Description: Stone duality
Maintainer: Olaf Klinke
Stability: experimental

[Stone duality](https://doi.org/10.1090/S0002-9947-1936-1501865-8)
relates Boolean algebras and Boolean homomorphisms 
to certain topological spaces, today known as Stone spaces. 
At the heart is a dual adjunction comprising 

1. the contavariant functor 'spec' that maps a Boolean algebra to the space of its ultrafilters,
2. the contravariant functor 'Predicate' that maps a space to the Boolean algebra of clopen subsets. 
-}
{-# LANGUAGE ConstraintKinds, FlexibleContexts, TypeOperators, UndecidableInstances, GADTs, ScopedTypeVariables #-}
module Topology.StoneSpace (
    -- * Ultrafilters
    Ultrafilter,
    principalUltrafilter,
    mapUF,
    -- * Stone spaces
    StoneSpace,
    spec,point,toPattern,
    -- ** Generic representations of Stone spaces
    GStoneSpace(..),
    covers,deletes
    ) where
import Data.Type.Predicate (Predicate(..),GStone(..),eval,insL,insR,mapMeta,mapRec,mapConst)
import Data.Searchable (K(..),restrict,forevery)
import GHC.Generics
import Control.Applicative (empty,(<|>))

-- * Ultrafilters

-- | An ultrafilter is a Boolean homomorphism 
-- from predicates to truth values. 
newtype Ultrafilter ty = UF (Predicate ty -> Bool)

-- | Evaluation of predicates at a single point 
-- yields the so-called principal ultrafilters. 
principalUltrafilter :: ty p -> Ultrafilter ty
principalUltrafilter :: forall (ty :: * -> *) p. ty p -> Ultrafilter ty
principalUltrafilter ty p
x = (Predicate ty -> Bool) -> Ultrafilter ty
forall (ty :: * -> *). (Predicate ty -> Bool) -> Ultrafilter ty
UF ((Predicate ty -> ty p -> Bool) -> ty p -> Predicate ty -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Predicate ty -> ty p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval ty p
x)

-- | Ultrafilters are functorial 
-- on the category 'GStone'. 
mapUF :: GStone f g -> Ultrafilter f -> Ultrafilter g
mapUF :: forall (f :: * -> *) (g :: * -> *).
GStone f g -> Ultrafilter f -> Ultrafilter g
mapUF (GStone Predicate g -> Predicate f
h) (UF Predicate f -> Bool
u) = (Predicate g -> Bool) -> Ultrafilter g
forall (ty :: * -> *). (Predicate ty -> Bool) -> Ultrafilter ty
UF (Predicate f -> Bool
u(Predicate f -> Bool)
-> (Predicate g -> Predicate f) -> Predicate g -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Predicate g -> Predicate f
h)
{-# INLINE mapUF #-}

-- | Ultrafilters on @f@ can be regarded as 'GStone' morphisms 
-- from the unit space 'U1' to @f@. 
ufStone :: Ultrafilter f -> GStone U1 f
ufStone :: forall (f :: * -> *). Ultrafilter f -> GStone U1 f
ufStone (UF Predicate f -> Bool
u) = (Predicate f -> Predicate U1) -> GStone U1 f
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone (Bool -> Predicate U1
shizophrenic(Bool -> Predicate U1)
-> (Predicate f -> Bool) -> Predicate f -> Predicate U1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Predicate f -> Bool
u) where
    -- the type 'Bool' is shizophrenic: 
    -- its both a Boolean algebra and a Stone space
    shizophrenic :: Bool -> Predicate U1
    shizophrenic :: Bool -> Predicate U1
shizophrenic Bool
True = Predicate U1
forall (a :: * -> *). Predicate a
Wildcard
    shizophrenic Bool
False = Predicate U1 -> Predicate U1
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate U1
forall (a :: * -> *). Predicate a
Wildcard

-- * Compactness

intersection :: K (f p) -> Predicate f -> K (f p)
intersection :: forall (f :: * -> *) p. K (f p) -> Predicate f -> K (f p)
intersection K (f p)
k Predicate f
p = K (f p) -> (f p -> Bool) -> K (f p)
forall a. K a -> (a -> Bool) -> K a
restrict K (f p)
k (Predicate f -> f p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate f
p) 

without :: K (f p) -> Predicate f -> K (f p)
K (f p)
k without :: forall (f :: * -> *) p. K (f p) -> Predicate f -> K (f p)
`without` Predicate f
p = K (f p) -> (f p -> Bool) -> K (f p)
forall a. K a -> (a -> Bool) -> K a
restrict K (f p)
k (Bool -> Bool
not(Bool -> Bool) -> (f p -> Bool) -> f p -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Predicate f -> f p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate f
p)

-- * Stone spaces

-- | A Stone space is isomorphic to the space of its ultrafilters. 
-- 'gpoint' is inverse to 'principalUltrafilter'. 
-- Stone spaces are totally disconnected, hence the 'Eq' superclass. 
-- Further, every Stone space is topologically compact, 
-- whence it is decidable whether the 'extent' of a predicate 
-- 'covers' the entire space. 
-- The function 'covers' is a meet-semilattice homomorphism 
-- and its logical negation 'deletes' is a join-semilattice homomorphism. 
--
-- Observe that there are types with ultrafilters 
-- that are not principal. 
-- Their existence is guaranteed by the Ultrafilter Lemma, 
-- which is a consequence of the Prime Ideal Theorem. 
-- Notably, consider total predicates @p :: 'Integer' -> 'Bool'@. 
-- Define the filter 
-- 
-- @
-- f p = ∃ n. ∀ m ≥ n. p m
-- @
--
-- This collects all predicates that are eventually true for 
-- sufficiently large numbers. Obviously for every number @n@ 
-- the predicate @p = (n ==)@ is not part of the filter @f@, 
-- whence any ultrafilter containing @f@ can not be principal 
-- at any number. But by the Ultrafilter Lemma, @f@ is indeed 
-- contained in some ultrafilter. 
class Eq (f ()) => GStoneSpace f where
    gpoint :: Ultrafilter f -> f p
    gpoint = ((U1 p -> f p) -> U1 p -> f p
forall a b. (a -> b) -> a -> b
$ U1 p
forall k (p :: k). U1 p
U1) ((U1 p -> f p) -> f p)
-> (Ultrafilter f -> U1 p -> f p) -> Ultrafilter f -> f p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GStone U1 f -> U1 p -> f p
forall (f :: * -> *) (g :: * -> *) p.
GStoneSpace f =>
GStone g f -> g p -> f p
forall (g :: * -> *) p. GStone g f -> g p -> f p
gSpec (GStone U1 f -> U1 p -> f p)
-> (Ultrafilter f -> GStone U1 f) -> Ultrafilter f -> U1 p -> f p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ultrafilter f -> GStone U1 f
forall (f :: * -> *). Ultrafilter f -> GStone U1 f
ufStone
    gSpec  :: GStone g f -> g p -> f p
    gSpec GStone g f
h = Ultrafilter f -> f p
forall p. Ultrafilter f -> f p
forall (f :: * -> *) p. GStoneSpace f => Ultrafilter f -> f p
gpoint (Ultrafilter f -> f p) -> (g p -> Ultrafilter f) -> g p -> f p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GStone g f -> Ultrafilter g -> Ultrafilter f
forall (f :: * -> *) (g :: * -> *).
GStone f g -> Ultrafilter f -> Ultrafilter g
mapUF GStone g f
h (Ultrafilter g -> Ultrafilter f)
-> (g p -> Ultrafilter g) -> g p -> Ultrafilter f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g p -> Ultrafilter g
forall (ty :: * -> *) p. ty p -> Ultrafilter ty
principalUltrafilter
    extent :: Predicate f -> K (f p)
    maybePattern :: (f () -> Bool) -> Maybe (Predicate f)
    -- ^ predicates that are pattern matches can automatically be transformed into 'Predicate's. 
    {-# MINIMAL extent, (gpoint | gSpec), maybePattern #-} 

-- | True if the predicate holds for all elements 
-- of the spectrum. 
covers :: GStoneSpace f => Predicate f -> Bool
covers :: forall (f :: * -> *). GStoneSpace f => Predicate f -> Bool
covers = (f Any -> Bool) -> Bool
forall (f :: * -> *) p. GStoneSpace f => (f p -> Bool) -> Bool
covers' ((f Any -> Bool) -> Bool)
-> (Predicate f -> f Any -> Bool) -> Predicate f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate f -> f Any -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval

covers' :: GStoneSpace f => (f p -> Bool) -> Bool
covers' :: forall (f :: * -> *) p. GStoneSpace f => (f p -> Bool) -> Bool
covers' = K (f p) -> (f p -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
forevery K (f p)
forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType

-- | True if the negation of the predicate 'covers'.
deletes :: GStoneSpace f => Predicate f -> Bool
deletes :: forall (f :: * -> *). GStoneSpace f => Predicate f -> Bool
deletes = Predicate f -> Bool
forall (f :: * -> *). GStoneSpace f => Predicate f -> Bool
covers (Predicate f -> Bool)
-> (Predicate f -> Predicate f) -> Predicate f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate f -> Predicate f
forall (a :: * -> *). Predicate a -> Predicate a
Neg

deletes' :: GStoneSpace f => (f p -> Bool) -> Bool
deletes' :: forall (f :: * -> *) p. GStoneSpace f => (f p -> Bool) -> Bool
deletes' f p -> Bool
p = (f p -> Bool) -> Bool
forall (f :: * -> *) p. GStoneSpace f => (f p -> Bool) -> Bool
covers' (Bool -> Bool
not(Bool -> Bool) -> (f p -> Bool) -> f p -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.f p -> Bool
p)

theType :: GStoneSpace f => K (f p)
theType :: forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType = Predicate f -> K (f p)
forall p. Predicate f -> K (f p)
forall (f :: * -> *) p. GStoneSpace f => Predicate f -> K (f p)
extent Predicate f
forall (a :: * -> *). Predicate a
Wildcard

-- | tries to find a witness for the fact that the predicate @p@
-- is representable by 'Fst'. 
-- It does so by searching for some @y0@ with
-- 
-- @
-- ∀ x ∀ y. p (x :*: y) == p (x :*: y0)
-- @
-- Which, if it exists, shows that p does in fact not look at the y.
isFst :: forall f g. (GStoneSpace f, GStoneSpace g) => ((f :*: g) () -> Bool) -> Maybe (g ())
isFst :: forall (f :: * -> *) (g :: * -> *).
(GStoneSpace f, GStoneSpace g) =>
((:*:) f g () -> Bool) -> Maybe (g ())
isFst (:*:) f g () -> Bool
p = case K (g ())
forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType :: K (g ()) of
    K (g ())
Emptyset -> Maybe (g ())
forall a. Maybe a
Nothing
    Nonempty (g () -> Bool) -> g ()
find -> let
        q :: g () -> f () -> g () -> Bool
        q :: g () -> f () -> g () -> Bool
q g ()
y f ()
x g ()
y' = (:*:) f g () -> Bool
p (f ()
x f () -> g () -> (:*:) f g ()
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g ()
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (:*:) f g () -> Bool
p (f ()
x f () -> g () -> (:*:) f g ()
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g ()
y')
        w :: g () -> Bool
        w :: g () -> Bool
w g ()
y = K (f ()) -> (f () -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
forevery K (f ())
forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType (\f ()
x -> K (g ()) -> (g () -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
forevery K (g ())
forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType (g () -> f () -> g () -> Bool
q g ()
y f ()
x))
        y0 :: g ()
y0 = (g () -> Bool) -> g ()
find g () -> Bool
w
        in if g () -> Bool
w g ()
y0
            then g () -> Maybe (g ())
forall a. a -> Maybe a
Just g ()
y0
            else Maybe (g ())
forall a. Maybe a
Nothing

-- | tries to find a witness for the fact that the predicate @p@
-- is representable by 'Snd'. 
isSnd :: forall f g. (GStoneSpace f, GStoneSpace g) => ((f :*: g) () -> Bool) -> Maybe (f ())
isSnd :: forall (f :: * -> *) (g :: * -> *).
(GStoneSpace f, GStoneSpace g) =>
((:*:) f g () -> Bool) -> Maybe (f ())
isSnd (:*:) f g () -> Bool
p = case K (f ())
forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType :: K (f ()) of
    K (f ())
Emptyset -> Maybe (f ())
forall a. Maybe a
Nothing
    Nonempty (f () -> Bool) -> f ()
find -> let
        q :: f () -> g () -> f () -> Bool
        q :: f () -> g () -> f () -> Bool
q f ()
x g ()
y f ()
x' = (:*:) f g () -> Bool
p (f ()
x f () -> g () -> (:*:) f g ()
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g ()
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (:*:) f g () -> Bool
p (f ()
x' f () -> g () -> (:*:) f g ()
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g ()
y)
        w :: f () -> Bool
        w :: f () -> Bool
w f ()
x = K (g ()) -> (g () -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
forevery K (g ())
forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType (\g ()
y -> K (f ()) -> (f () -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
forevery K (f ())
forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType (f () -> g () -> f () -> Bool
q f ()
x g ()
y))
        x0 :: f ()
x0 = (f () -> Bool) -> f ()
find f () -> Bool
w
        in if f () -> Bool
w f ()
x0
            then f () -> Maybe (f ())
forall a. a -> Maybe a
Just f ()
x0
            else Maybe (f ())
forall a. Maybe a
Nothing

type StoneSpace x = (Generic x, GStoneSpace (Rep x))

-- | Find the point at which the ultrafilter is fixed.
point :: StoneSpace x => Ultrafilter (Rep x) -> x
point :: forall x. StoneSpace x => Ultrafilter (Rep x) -> x
point = Rep x Any -> x
forall a x. Generic a => Rep a x -> a
forall x. Rep x x -> x
to(Rep x Any -> x)
-> (Ultrafilter (Rep x) -> Rep x Any) -> Ultrafilter (Rep x) -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Ultrafilter (Rep x) -> Rep x Any
forall p. Ultrafilter (Rep x) -> Rep x p
forall (f :: * -> *) p. GStoneSpace f => Ultrafilter f -> f p
gpoint

-- | Predicate transformers between 
-- 'Rep'resentations of Stone spaces 
-- encode ordinary functions. 
-- This mapping is the morphism part of the spectrum functor. 
spec :: (Generic x, StoneSpace y) => GStone (Rep x) (Rep y) -> x -> y
spec :: forall x y.
(Generic x, StoneSpace y) =>
GStone (Rep x) (Rep y) -> x -> y
spec GStone (Rep x) (Rep y)
h = Rep y Any -> y
forall a x. Generic a => Rep a x -> a
forall x. Rep y x -> y
to (Rep y Any -> y) -> (x -> Rep y Any) -> x -> y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GStone (Rep x) (Rep y) -> Rep x Any -> Rep y Any
forall (f :: * -> *) (g :: * -> *) p.
GStoneSpace f =>
GStone g f -> g p -> f p
forall (g :: * -> *) p. GStone g (Rep y) -> g p -> Rep y p
gSpec GStone (Rep x) (Rep y)
h (Rep x Any -> Rep y Any) -> (x -> Rep x Any) -> x -> Rep y Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Rep x Any
forall x. x -> Rep x x
forall a x. Generic a => a -> Rep a x
from

-- | Attempts to transform a predicate to a 'Predicate' representation. 
-- This will not work if the predicate inspects both parts of a tuple. 
-- For simple pattern matches, it works:
-- 
-- >>> isJust (toPattern ((either id (LT==).fst) :: (Either Bool Ordering,()) -> Bool))
-- True
toPattern :: StoneSpace x => (x -> Bool) -> Maybe (Predicate (Rep x))
toPattern :: forall x. StoneSpace x => (x -> Bool) -> Maybe (Predicate (Rep x))
toPattern x -> Bool
p = (Rep x () -> Bool) -> Maybe (Predicate (Rep x))
forall (f :: * -> *).
GStoneSpace f =>
(f () -> Bool) -> Maybe (Predicate f)
maybePattern (x -> Bool
p(x -> Bool) -> (Rep x () -> x) -> Rep x () -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Rep x () -> x
forall a x. Generic a => Rep a x -> a
forall x. Rep x x -> x
to)
 
-- | Singletons are Stone spaces
instance GStoneSpace U1 where
    gpoint :: forall p. Ultrafilter U1 -> U1 p
gpoint = U1 p -> Ultrafilter U1 -> U1 p
forall a b. a -> b -> a
const U1 p
forall k (p :: k). U1 p
U1
    extent :: forall p. Predicate U1 -> K (U1 p)
extent Predicate U1
p = if Predicate U1 -> U1 Any -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate U1
p U1 Any
forall k (p :: k). U1 p
U1 then U1 p -> K (U1 p)
forall a. a -> K a
forall (f :: * -> *) a. Applicative f => a -> f a
pure U1 p
forall k (p :: k). U1 p
U1 else K (U1 p)
forall a. K a
forall (f :: * -> *) a. Alternative f => f a
empty
    maybePattern :: (U1 () -> Bool) -> Maybe (Predicate U1)
maybePattern U1 () -> Bool
p = Predicate U1 -> Maybe (Predicate U1)
forall a. a -> Maybe a
Just (if (U1 () -> Bool) -> Bool
forall (f :: * -> *) p. GStoneSpace f => (f p -> Bool) -> Bool
covers' U1 () -> Bool
p then Predicate U1
forall (a :: * -> *). Predicate a
Wildcard else Predicate U1 -> Predicate U1
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate U1
forall (a :: * -> *). Predicate a
Wildcard)

-- | Products of Stone spaces are Stone spaces
instance (GStoneSpace f, GStoneSpace g) => GStoneSpace (f :*: g) where
    gpoint :: forall p. Ultrafilter (f :*: g) -> (:*:) f g p
gpoint Ultrafilter (f :*: g)
u = Ultrafilter f -> f p
forall p. Ultrafilter f -> f p
forall (f :: * -> *) p. GStoneSpace f => Ultrafilter f -> f p
gpoint (GStone (f :*: g) f -> Ultrafilter (f :*: g) -> Ultrafilter f
forall (f :: * -> *) (g :: * -> *).
GStone f g -> Ultrafilter f -> Ultrafilter g
mapUF ((Predicate f -> Predicate (f :*: g)) -> GStone (f :*: g) f
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone Predicate f -> Predicate (f :*: g)
forall (f :: * -> *) (g :: * -> *).
Predicate f -> Predicate (f :*: g)
Fst) Ultrafilter (f :*: g)
u) f p -> g p -> (:*:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ultrafilter g -> g p
forall p. Ultrafilter g -> g p
forall (f :: * -> *) p. GStoneSpace f => Ultrafilter f -> f p
gpoint (GStone (f :*: g) g -> Ultrafilter (f :*: g) -> Ultrafilter g
forall (f :: * -> *) (g :: * -> *).
GStone f g -> Ultrafilter f -> Ultrafilter g
mapUF ((Predicate g -> Predicate (f :*: g)) -> GStone (f :*: g) g
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone Predicate g -> Predicate (f :*: g)
forall (g :: * -> *) (f :: * -> *).
Predicate g -> Predicate (f :*: g)
Snd) Ultrafilter (f :*: g)
u)
    extent :: forall p. Predicate (f :*: g) -> K ((:*:) f g p)
extent Predicate (f :*: g)
Wildcard = f p -> g p -> (:*:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (f p -> g p -> (:*:) f g p) -> K (f p) -> K (g p -> (:*:) f g p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> K (f p)
forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType K (g p -> (:*:) f g p) -> K (g p) -> K ((:*:) f g p)
forall a b. K (a -> b) -> K a -> K b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> K (g p)
forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType
    extent (Predicate (f :*: g)
p :\/ Predicate (f :*: g)
q) = Predicate (f :*: g) -> K ((:*:) f g p)
forall p. Predicate (f :*: g) -> K ((:*:) f g p)
forall (f :: * -> *) p. GStoneSpace f => Predicate f -> K (f p)
extent Predicate (f :*: g)
p K ((:*:) f g p) -> K ((:*:) f g p) -> K ((:*:) f g p)
forall a. K a -> K a -> K a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Predicate (f :*: g) -> K ((:*:) f g p)
forall p. Predicate (f :*: g) -> K ((:*:) f g p)
forall (f :: * -> *) p. GStoneSpace f => Predicate f -> K (f p)
extent Predicate (f :*: g)
q
    extent (Predicate (f :*: g)
p :/\ Predicate (f :*: g)
q) = (Predicate (f :*: g) -> K ((:*:) f g p)
forall p. Predicate (f :*: g) -> K ((:*:) f g p)
forall (f :: * -> *) p. GStoneSpace f => Predicate f -> K (f p)
extent Predicate (f :*: g)
p) K ((:*:) f g p) -> Predicate (f :*: g) -> K ((:*:) f g p)
forall (f :: * -> *) p. K (f p) -> Predicate f -> K (f p)
`intersection` Predicate (f :*: g)
q
    extent (Fst Predicate f
p) = f p -> g p -> (:*:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (f p -> g p -> (:*:) f g p) -> K (f p) -> K (g p -> (:*:) f g p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Predicate f -> K (f p)
forall p. Predicate f -> K (f p)
forall (f :: * -> *) p. GStoneSpace f => Predicate f -> K (f p)
extent Predicate f
Predicate f
p K (g p -> (:*:) f g p) -> K (g p) -> K ((:*:) f g p)
forall a b. K (a -> b) -> K a -> K b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> K (g p)
forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType
    extent (Snd Predicate g
p) = f p -> g p -> (:*:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (f p -> g p -> (:*:) f g p) -> K (f p) -> K (g p -> (:*:) f g p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> K (f p)
forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType K (g p -> (:*:) f g p) -> K (g p) -> K ((:*:) f g p)
forall a b. K (a -> b) -> K a -> K b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Predicate g -> K (g p)
forall p. Predicate g -> K (g p)
forall (f :: * -> *) p. GStoneSpace f => Predicate f -> K (f p)
extent Predicate g
Predicate g
p
    extent (Neg Predicate (f :*: g)
p) = K ((:*:) f g p)
forall (f :: * -> *) p. GStoneSpace f => K (f p)
theType K ((:*:) f g p) -> Predicate (f :*: g) -> K ((:*:) f g p)
forall (f :: * -> *) p. K (f p) -> Predicate f -> K (f p)
`without` Predicate (f :*: g)
p
    -- | the 'Predicate' can not be derived if the predicate inspects both components.
    maybePattern :: ((:*:) f g () -> Bool) -> Maybe (Predicate (f :*: g))
maybePattern (:*:) f g () -> Bool
p = case (((:*:) f g () -> Bool) -> Bool
forall (f :: * -> *) p. GStoneSpace f => (f p -> Bool) -> Bool
covers' (:*:) f g () -> Bool
p, ((:*:) f g () -> Bool) -> Bool
forall (f :: * -> *) p. GStoneSpace f => (f p -> Bool) -> Bool
deletes' (:*:) f g () -> Bool
p, ((:*:) f g () -> Bool) -> Maybe (g ())
forall (f :: * -> *) (g :: * -> *).
(GStoneSpace f, GStoneSpace g) =>
((:*:) f g () -> Bool) -> Maybe (g ())
isFst (:*:) f g () -> Bool
p, ((:*:) f g () -> Bool) -> Maybe (f ())
forall (f :: * -> *) (g :: * -> *).
(GStoneSpace f, GStoneSpace g) =>
((:*:) f g () -> Bool) -> Maybe (f ())
isSnd (:*:) f g () -> Bool
p) of
        (Bool
True,Bool
_,Maybe (g ())
_,Maybe (f ())
_) -> Predicate (f :*: g) -> Maybe (Predicate (f :*: g))
forall a. a -> Maybe a
Just Predicate (f :*: g)
forall (a :: * -> *). Predicate a
Wildcard
        (Bool
False,Bool
True,Maybe (g ())
_,Maybe (f ())
_) -> Predicate (f :*: g) -> Maybe (Predicate (f :*: g))
forall a. a -> Maybe a
Just (Predicate (f :*: g) -> Predicate (f :*: g)
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate (f :*: g)
forall (a :: * -> *). Predicate a
Wildcard)
        (Bool
False,Bool
False,Just g ()
y,Maybe (f ())
_) -> let q :: f () -> Bool
q = (:*:) f g () -> Bool
p((:*:) f g () -> Bool) -> (f () -> (:*:) f g ()) -> f () -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(\f ()
x -> f ()
x f () -> g () -> (:*:) f g ()
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g ()
y) in (Predicate f -> Predicate (f :*: g))
-> Maybe (Predicate f) -> Maybe (Predicate (f :*: g))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Predicate f -> Predicate (f :*: g)
forall (f :: * -> *) (g :: * -> *).
Predicate f -> Predicate (f :*: g)
Fst ((f () -> Bool) -> Maybe (Predicate f)
forall (f :: * -> *).
GStoneSpace f =>
(f () -> Bool) -> Maybe (Predicate f)
maybePattern f () -> Bool
q)
        (Bool
False,Bool
False,Maybe (g ())
Nothing,Just f ()
x) -> let q :: g () -> Bool
q = (:*:) f g () -> Bool
p((:*:) f g () -> Bool) -> (g () -> (:*:) f g ()) -> g () -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(\g ()
y -> f ()
x f () -> g () -> (:*:) f g ()
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g ()
y) in (Predicate g -> Predicate (f :*: g))
-> Maybe (Predicate g) -> Maybe (Predicate (f :*: g))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Predicate g -> Predicate (f :*: g)
forall (g :: * -> *) (f :: * -> *).
Predicate g -> Predicate (f :*: g)
Snd ((g () -> Bool) -> Maybe (Predicate g)
forall (f :: * -> *).
GStoneSpace f =>
(f () -> Bool) -> Maybe (Predicate f)
maybePattern g () -> Bool
q)
        (Bool
False,Bool
False,Maybe (g ())
Nothing,Maybe (f ())
Nothing) -> Maybe (Predicate (f :*: g))
forall a. Maybe a
Nothing
        

-- | Coproducts of Stone spaces are Stone spaces. 
-- This crucially relies on the algebraic properties of ultrafilters.
instance (GStoneSpace f, GStoneSpace g) => GStoneSpace (f :+: g) where
    gpoint :: forall p. Ultrafilter (f :+: g) -> (:+:) f g p
gpoint (UF Predicate (f :+: g) -> Bool
h) = let isLeft :: Predicate (f :+: g)
isLeft = Predicate f -> Predicate g -> Predicate (f :+: g)
forall (f :: * -> *) (g :: * -> *).
Predicate f -> Predicate g -> Predicate (f :+: g)
Case Predicate f
forall (a :: * -> *). Predicate a
Wildcard (Predicate g -> Predicate g
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate g
forall (a :: * -> *). Predicate a
Wildcard)
        in if Predicate (f :+: g) -> Bool
h Predicate (f :+: g)
forall {f :: * -> *} {g :: * -> *}. Predicate (f :+: g)
isLeft
            then f p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (Ultrafilter f -> f p
forall p. Ultrafilter f -> f p
forall (f :: * -> *) p. GStoneSpace f => Ultrafilter f -> f p
gpoint ((Predicate f -> Bool) -> Ultrafilter f
forall (ty :: * -> *). (Predicate ty -> Bool) -> Ultrafilter ty
UF (\Predicate f
p -> Predicate (f :+: g) -> Bool
h (Predicate f -> Predicate g -> Predicate (f :+: g)
forall (f :: * -> *) (g :: * -> *).
Predicate f -> Predicate g -> Predicate (f :+: g)
Case Predicate f
p (Predicate g -> Predicate g
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate g
forall (a :: * -> *). Predicate a
Wildcard)))))
            else g p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Ultrafilter g -> g p
forall p. Ultrafilter g -> g p
forall (f :: * -> *) p. GStoneSpace f => Ultrafilter f -> f p
gpoint ((Predicate g -> Bool) -> Ultrafilter g
forall (ty :: * -> *). (Predicate ty -> Bool) -> Ultrafilter ty
UF (\Predicate g
p -> Predicate (f :+: g) -> Bool
h (Predicate f -> Predicate g -> Predicate (f :+: g)
forall (f :: * -> *) (g :: * -> *).
Predicate f -> Predicate g -> Predicate (f :+: g)
Case (Predicate f -> Predicate f
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate f
forall (a :: * -> *). Predicate a
Wildcard) Predicate g
p))))
    extent :: forall p. Predicate (f :+: g) -> K ((:+:) f g p)
extent Predicate (f :+: g)
p = (f p -> (:+:) f g p) -> K (f p) -> K ((:+:) f g p)
forall a b. (a -> b) -> K a -> K b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (Predicate f -> K (f p)
forall p. Predicate f -> K (f p)
forall (f :: * -> *) p. GStoneSpace f => Predicate f -> K (f p)
extent (Predicate (f :+: g) -> Predicate f
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate f
insL Predicate (f :+: g)
p)) K ((:+:) f g p) -> K ((:+:) f g p) -> K ((:+:) f g p)
forall a. K a -> K a -> K a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (g p -> (:+:) f g p) -> K (g p) -> K ((:+:) f g p)
forall a b. (a -> b) -> K a -> K b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Predicate g -> K (g p)
forall p. Predicate g -> K (g p)
forall (f :: * -> *) p. GStoneSpace f => Predicate f -> K (f p)
extent (Predicate (f :+: g) -> Predicate g
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate g
insR Predicate (f :+: g)
p))
    maybePattern :: ((:+:) f g () -> Bool) -> Maybe (Predicate (f :+: g))
maybePattern (:+:) f g () -> Bool
p = Predicate f -> Predicate g -> Predicate (f :+: g)
forall (f :: * -> *) (g :: * -> *).
Predicate f -> Predicate g -> Predicate (f :+: g)
Case (Predicate f -> Predicate g -> Predicate (f :+: g))
-> Maybe (Predicate f)
-> Maybe (Predicate g -> Predicate (f :+: g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        ((f () -> Bool) -> Maybe (Predicate f)
forall (f :: * -> *).
GStoneSpace f =>
(f () -> Bool) -> Maybe (Predicate f)
maybePattern ((:+:) f g () -> Bool
p ((:+:) f g () -> Bool) -> (f () -> (:+:) f g ()) -> f () -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f () -> (:+:) f g ()
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1)) Maybe (Predicate g -> Predicate (f :+: g))
-> Maybe (Predicate g) -> Maybe (Predicate (f :+: g))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
        ((g () -> Bool) -> Maybe (Predicate g)
forall (f :: * -> *).
GStoneSpace f =>
(f () -> Bool) -> Maybe (Predicate f)
maybePattern ((:+:) f g () -> Bool
p ((:+:) f g () -> Bool) -> (g () -> (:+:) f g ()) -> g () -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g () -> (:+:) f g ()
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1))

instance GStoneSpace f => GStoneSpace (M1 i m f) where
    gpoint :: forall p. Ultrafilter (M1 i m f) -> M1 i m f p
gpoint = f p -> M1 i m f p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f p -> M1 i m f p)
-> (Ultrafilter (M1 i m f) -> f p)
-> Ultrafilter (M1 i m f)
-> M1 i m f p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ultrafilter f -> f p
forall p. Ultrafilter f -> f p
forall (f :: * -> *) p. GStoneSpace f => Ultrafilter f -> f p
gpoint (Ultrafilter f -> f p)
-> (Ultrafilter (M1 i m f) -> Ultrafilter f)
-> Ultrafilter (M1 i m f)
-> f p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GStone (M1 i m f) f -> Ultrafilter (M1 i m f) -> Ultrafilter f
forall (f :: * -> *) (g :: * -> *).
GStone f g -> Ultrafilter f -> Ultrafilter g
mapUF ((Predicate f -> Predicate (M1 i m f)) -> GStone (M1 i m f) f
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone Predicate f -> Predicate (M1 i m f)
forall (f :: * -> *) i (m :: Meta).
Predicate f -> Predicate (M1 i m f)
MetaP)
    extent :: forall p. Predicate (M1 i m f) -> K (M1 i m f p)
extent Predicate (M1 i m f)
p = (f p -> M1 i m f p) -> K (f p) -> K (M1 i m f p)
forall a b. (a -> b) -> K a -> K b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f p -> M1 i m f p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Predicate f -> K (f p)
forall p. Predicate f -> K (f p)
forall (f :: * -> *) p. GStoneSpace f => Predicate f -> K (f p)
extent (Predicate (M1 i m f) -> Predicate f
forall i (m :: Meta) (f :: * -> *).
Predicate (M1 i m f) -> Predicate f
mapMeta Predicate (M1 i m f)
p))
    maybePattern :: (M1 i m f () -> Bool) -> Maybe (Predicate (M1 i m f))
maybePattern M1 i m f () -> Bool
p = (Predicate f -> Predicate (M1 i m f))
-> Maybe (Predicate f) -> Maybe (Predicate (M1 i m f))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Predicate f -> Predicate (M1 i m f)
forall (f :: * -> *) i (m :: Meta).
Predicate f -> Predicate (M1 i m f)
MetaP ((f () -> Bool) -> Maybe (Predicate f)
forall (f :: * -> *).
GStoneSpace f =>
(f () -> Bool) -> Maybe (Predicate f)
maybePattern (M1 i m f () -> Bool
p (M1 i m f () -> Bool) -> (f () -> M1 i m f ()) -> f () -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f () -> M1 i m f ()
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1))

instance GStoneSpace f => GStoneSpace (Rec1 f) where
    gpoint :: forall p. Ultrafilter (Rec1 f) -> Rec1 f p
gpoint = f p -> Rec1 f p
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 (f p -> Rec1 f p)
-> (Ultrafilter (Rec1 f) -> f p)
-> Ultrafilter (Rec1 f)
-> Rec1 f p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ultrafilter f -> f p
forall p. Ultrafilter f -> f p
forall (f :: * -> *) p. GStoneSpace f => Ultrafilter f -> f p
gpoint (Ultrafilter f -> f p)
-> (Ultrafilter (Rec1 f) -> Ultrafilter f)
-> Ultrafilter (Rec1 f)
-> f p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GStone (Rec1 f) f -> Ultrafilter (Rec1 f) -> Ultrafilter f
forall (f :: * -> *) (g :: * -> *).
GStone f g -> Ultrafilter f -> Ultrafilter g
mapUF ((Predicate f -> Predicate (Rec1 f)) -> GStone (Rec1 f) f
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone Predicate f -> Predicate (Rec1 f)
forall (f :: * -> *). Predicate f -> Predicate (Rec1 f)
RecP)
    extent :: forall p. Predicate (Rec1 f) -> K (Rec1 f p)
extent Predicate (Rec1 f)
p = (f p -> Rec1 f p) -> K (f p) -> K (Rec1 f p)
forall a b. (a -> b) -> K a -> K b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f p -> Rec1 f p
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 (Predicate f -> K (f p)
forall p. Predicate f -> K (f p)
forall (f :: * -> *) p. GStoneSpace f => Predicate f -> K (f p)
extent (Predicate (Rec1 f) -> Predicate f
forall (f :: * -> *). Predicate (Rec1 f) -> Predicate f
mapRec Predicate (Rec1 f)
p))
    maybePattern :: (Rec1 f () -> Bool) -> Maybe (Predicate (Rec1 f))
maybePattern Rec1 f () -> Bool
p = (Predicate f -> Predicate (Rec1 f))
-> Maybe (Predicate f) -> Maybe (Predicate (Rec1 f))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Predicate f -> Predicate (Rec1 f)
forall (f :: * -> *). Predicate f -> Predicate (Rec1 f)
RecP ((f () -> Bool) -> Maybe (Predicate f)
forall (f :: * -> *).
GStoneSpace f =>
(f () -> Bool) -> Maybe (Predicate f)
maybePattern (Rec1 f () -> Bool
p (Rec1 f () -> Bool) -> (f () -> Rec1 f ()) -> f () -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f () -> Rec1 f ()
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1))

instance (Generic c, Eq c, Rep c ~ f, GStoneSpace f) => GStoneSpace (K1 i c) where
    gpoint :: forall p. Ultrafilter (K1 i c) -> K1 i c p
gpoint = c -> K1 i c p
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c p)
-> (Ultrafilter (K1 i c) -> c) -> Ultrafilter (K1 i c) -> K1 i c p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ultrafilter f -> c
Ultrafilter (Rep c) -> c
forall x. StoneSpace x => Ultrafilter (Rep x) -> x
point (Ultrafilter f -> c)
-> (Ultrafilter (K1 i c) -> Ultrafilter f)
-> Ultrafilter (K1 i c)
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GStone (K1 i c) f -> Ultrafilter (K1 i c) -> Ultrafilter f
forall (f :: * -> *) (g :: * -> *).
GStone f g -> Ultrafilter f -> Ultrafilter g
mapUF ((Predicate f -> Predicate (K1 i c)) -> GStone (K1 i c) f
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone Predicate f -> Predicate (K1 i c)
forall c (f :: * -> *) i.
(Generic c, Rep c ~ f) =>
Predicate f -> Predicate (K1 i c)
ConstP)
    extent :: forall p. Predicate (K1 i c) -> K (K1 i c p)
extent = (f Any -> K1 i c p) -> K (f Any) -> K (K1 i c p)
forall a b. (a -> b) -> K a -> K b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (c -> K1 i c p
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c p) -> (f Any -> c) -> f Any -> K1 i c p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Any -> c
Rep c Any -> c
forall a x. Generic a => Rep a x -> a
forall x. Rep c x -> c
to) (K (f Any) -> K (K1 i c p))
-> (Predicate (K1 i c) -> K (f Any))
-> Predicate (K1 i c)
-> K (K1 i c p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate f -> K (f Any)
forall p. Predicate f -> K (f p)
forall (f :: * -> *) p. GStoneSpace f => Predicate f -> K (f p)
extent (Predicate f -> K (f Any))
-> (Predicate (K1 i c) -> Predicate f)
-> Predicate (K1 i c)
-> K (f Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate (K1 i c) -> Predicate f
Predicate (K1 i c) -> Predicate (Rep c)
forall c i. Generic c => Predicate (K1 i c) -> Predicate (Rep c)
mapConst
    maybePattern :: (K1 i c () -> Bool) -> Maybe (Predicate (K1 i c))
maybePattern K1 i c () -> Bool
p = (Predicate f -> Predicate (K1 i c))
-> Maybe (Predicate f) -> Maybe (Predicate (K1 i c))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Predicate f -> Predicate (K1 i c)
forall c (f :: * -> *) i.
(Generic c, Rep c ~ f) =>
Predicate f -> Predicate (K1 i c)
ConstP ((f () -> Bool) -> Maybe (Predicate f)
forall (f :: * -> *).
GStoneSpace f =>
(f () -> Bool) -> Maybe (Predicate f)
maybePattern (K1 i c () -> Bool
p (K1 i c () -> Bool) -> (f () -> K1 i c ()) -> f () -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> K1 i c ()
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c ()) -> (f () -> c) -> f () -> K1 i c ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f () -> c
Rep c () -> c
forall a x. Generic a => Rep a x -> a
forall x. Rep c x -> c
to))
    -- needs UndecidableInstances