{-|
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 x = UF (flip eval x)

-- | Ultrafilters are functorial 
-- on the category 'GStone'. 
mapUF :: GStone f g -> Ultrafilter f -> Ultrafilter g
mapUF (GStone h) (UF u) = UF (u.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 (UF u) = GStone (shizophrenic.u) where
    -- the type 'Bool' is shizophrenic: 
    -- its both a Boolean algebra and a Stone space
    shizophrenic :: Bool -> Predicate U1
    shizophrenic True = Wildcard
    shizophrenic False = Neg Wildcard

-- * Compactness

intersection :: K (f p) -> Predicate f -> K (f p)
intersection k p = restrict k (eval p) 

without :: K (f p) -> Predicate f -> K (f p)
k `without` p = restrict k (not.eval 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) . gSpec . ufStone
    gSpec  :: GStone g f -> g p -> f p
    gSpec h = gpoint . mapUF h . 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 = covers' . eval

covers' :: GStoneSpace f => (f p -> Bool) -> Bool
covers' = forevery theType

-- | True if the negation of the predicate 'covers'.
deletes :: GStoneSpace f => Predicate f -> Bool
deletes = covers . Neg

deletes' :: GStoneSpace f => (f p -> Bool) -> Bool
deletes' p = covers' (not.p)

theType :: GStoneSpace f => K (f p)
theType = extent 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 p = case theType :: K (g ()) of
    Emptyset -> Nothing
    Nonempty find -> let
        q :: g () -> f () -> g () -> Bool
        q y x y' = p (x :*: y) == p (x :*: y')
        w :: g () -> Bool
        w y = forevery theType (\x -> forevery theType (q y x))
        y0 = find w
        in if w y0
            then Just y0
            else 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 p = case theType :: K (f ()) of
    Emptyset -> Nothing
    Nonempty find -> let
        q :: f () -> g () -> f () -> Bool
        q x y x' = p (x :*: y) == p (x' :*: y)
        w :: f () -> Bool
        w x = forevery theType (\y -> forevery theType (q x y))
        x0 = find w
        in if w x0
            then Just x0
            else 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 = to.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 h = to . gSpec h . 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 p = maybePattern (p.to)
 
-- | Singletons are Stone spaces
instance GStoneSpace U1 where
    gpoint = const U1
    extent p = if eval p U1 then pure U1 else empty
    maybePattern p = Just (if covers' p then Wildcard else Neg Wildcard)

-- | Products of Stone spaces are Stone spaces
instance (GStoneSpace f, GStoneSpace g) => GStoneSpace (f :*: g) where
    gpoint u = gpoint (mapUF (GStone Fst) u) :*: gpoint (mapUF (GStone Snd) u)
    extent Wildcard = (:*:) <$> theType <*> theType
    extent (p :\/ q) = extent p <|> extent q
    extent (p :/\ q) = (extent p) `intersection` q
    extent (Fst p) = (:*:) <$> extent p <*> theType
    extent (Snd p) = (:*:) <$> theType <*> extent p
    extent (Neg p) = theType `without` p
    -- | the 'Predicate' can not be derived if the predicate inspects both components.
    maybePattern p = case (covers' p, deletes' p, isFst p, isSnd p) of
        (True,_,_,_) -> Just Wildcard
        (False,True,_,_) -> Just (Neg Wildcard)
        (False,False,Just y,_) -> let q = p.(\x -> x :*: y) in fmap Fst (maybePattern q)
        (False,False,Nothing,Just x) -> let q = p.(\y -> x :*: y) in fmap Snd (maybePattern q)
        (False,False,Nothing,Nothing) -> 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 (UF h) = let isLeft = Case Wildcard (Neg Wildcard)
        in if h isLeft
            then L1 (gpoint (UF (\p -> h (Case p (Neg Wildcard)))))
            else R1 (gpoint (UF (\p -> h (Case (Neg Wildcard) p))))
    extent p = fmap L1 (extent (insL p)) <|> fmap R1 (extent (insR p))
    maybePattern p = Case <$>
        (maybePattern (p . L1)) <*>
        (maybePattern (p . R1))

instance GStoneSpace f => GStoneSpace (M1 i m f) where
    gpoint = M1 . gpoint . mapUF (GStone MetaP)
    extent p = fmap M1 (extent (mapMeta p))
    maybePattern p = fmap MetaP (maybePattern (p . M1))

instance GStoneSpace f => GStoneSpace (Rec1 f) where
    gpoint = Rec1 . gpoint . mapUF (GStone RecP)
    extent p = fmap Rec1 (extent (mapRec p))
    maybePattern p = fmap RecP (maybePattern (p . Rec1))

instance (Generic c, Eq c, Rep c ~ f, GStoneSpace f) => GStoneSpace (K1 i c) where
    gpoint = K1 . point . mapUF (GStone ConstP)
    extent = fmap (K1 . to) . extent . mapConst
    maybePattern p = fmap ConstP (maybePattern (p . K1 . to))
    -- needs UndecidableInstances