{-# LANGUAGE CPP             #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE Safe            #-}
----------------------------------------------------------------------------
-- |
-- Module      :  Algebra.Heyting
-- Copyright   :  (C) 2019 Oleg Grenrus
-- License     :  BSD-3-Clause (see the file LICENSE)
--
-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>
--
----------------------------------------------------------------------------
module Algebra.Heyting where

import Prelude ()
import Prelude.Compat

import Algebra.Lattice
import Control.Applicative   (Const (..))
import Data.Functor.Identity (Identity (..))
import Data.Hashable         (Hashable (..))
import Data.Proxy            (Proxy (..))
import Data.Semigroup        (All (..), Any (..), Endo (..))
import Data.Tagged           (Tagged (..))
import Data.Universe.Class   (Finite (..))

import qualified Data.HashSet as HS
import qualified Data.Set     as Set

#if MIN_VERSION_base(4,16,0)
import Data.Tuple (Solo (..))
#elif MIN_VERSION_base(4,15,0)
import GHC.Tuple (Solo (..))
#else
import Data.Tuple.Solo (Solo (..))
#endif

-- | A Heyting algebra is a bounded lattice equipped with a
-- binary operation \(a \to b\) of implication.
--
-- /Laws/
--
-- @
-- x '==>' x        ≡ 'top'
-- x '/\' (x '==>' y) ≡ x '/\' y
-- y '/\' (x '==>' y) ≡ y
-- x '==>' (y '/\' z) ≡ (x '==>' y) '/\' (x '==>' z)
-- @
--
class BoundedLattice a => Heyting a where
    -- | Implication.
    (==>) :: a -> a -> a

    -- | Negation.
    --
    -- @
    -- 'neg' x = x '==>' 'bottom'
    -- @
    neg :: a -> a
    neg a
x = a
x a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
forall a. BoundedJoinSemiLattice a => a
bottom

    -- | Equivalence.
    --
    -- @
    -- x '<=>' y = (x '==>' y) '/\' (y '==>' x)
    -- @
    (<=>) :: a -> a -> a
    a
x <=> a
y = (a
x a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
y) a -> a -> a
forall a. Lattice a => a -> a -> a
/\ (a
y a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
x)

infixr 5 ==>, <=>

-------------------------------------------------------------------------------
-- base
-------------------------------------------------------------------------------

instance Heyting () where
    ()
_ ==> :: () -> () -> ()
==> ()
_ = ()
    neg :: () -> ()
neg ()
_   = ()
    ()
_ <=> :: () -> () -> ()
<=> ()
_ = ()

instance Heyting Bool where
    Bool
False ==> :: Bool -> Bool -> Bool
==> Bool
_ = Bool
True
    Bool
True  ==> Bool
y = Bool
y

    neg :: Bool -> Bool
neg   = Bool -> Bool
not
    <=> :: Bool -> Bool -> Bool
(<=>) = Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==)

instance Heyting a => Heyting (b -> a) where
    b -> a
f ==> :: (b -> a) -> (b -> a) -> b -> a
==> b -> a
g = \b
x -> b -> a
f b
x a -> a -> a
forall a. Heyting a => a -> a -> a
==> b -> a
g b
x
    b -> a
f <=> :: (b -> a) -> (b -> a) -> b -> a
<=> b -> a
g = \b
x -> b -> a
f b
x a -> a -> a
forall a. Heyting a => a -> a -> a
<=> b -> a
g b
x
    neg :: (b -> a) -> b -> a
neg b -> a
f   = a -> a
forall a. Heyting a => a -> a
neg (a -> a) -> (b -> a) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
f

-------------------------------------------------------------------------------
-- All, Any, Endo
-------------------------------------------------------------------------------

instance Heyting All where
    All Bool
a ==> :: All -> All -> All
==> All Bool
b = Bool -> All
All (Bool
a Bool -> Bool -> Bool
forall a. Heyting a => a -> a -> a
==> Bool
b)
    neg :: All -> All
neg (All Bool
a)     = Bool -> All
All (Bool -> Bool
forall a. Heyting a => a -> a
neg Bool
a)
    All Bool
a <=> :: All -> All -> All
<=> All Bool
b = Bool -> All
All (Bool
a Bool -> Bool -> Bool
forall a. Heyting a => a -> a -> a
<=> Bool
b)

instance Heyting Any where
    Any Bool
a ==> :: Any -> Any -> Any
==> Any Bool
b = Bool -> Any
Any (Bool
a Bool -> Bool -> Bool
forall a. Heyting a => a -> a -> a
==> Bool
b)
    neg :: Any -> Any
neg (Any Bool
a)     = Bool -> Any
Any (Bool -> Bool
forall a. Heyting a => a -> a
neg Bool
a)
    Any Bool
a <=> :: Any -> Any -> Any
<=> Any Bool
b = Bool -> Any
Any (Bool
a Bool -> Bool -> Bool
forall a. Heyting a => a -> a -> a
<=> Bool
b)

instance Heyting a => Heyting (Endo a) where
    Endo a -> a
a ==> :: Endo a -> Endo a -> Endo a
==> Endo a -> a
b = (a -> a) -> Endo a
forall a. (a -> a) -> Endo a
Endo (a -> a
a (a -> a) -> (a -> a) -> a -> a
forall a. Heyting a => a -> a -> a
==> a -> a
b)
    neg :: Endo a -> Endo a
neg (Endo a -> a
a)      = (a -> a) -> Endo a
forall a. (a -> a) -> Endo a
Endo ((a -> a) -> a -> a
forall a. Heyting a => a -> a
neg a -> a
a)
    Endo a -> a
a <=> :: Endo a -> Endo a -> Endo a
<=> Endo a -> a
b = (a -> a) -> Endo a
forall a. (a -> a) -> Endo a
Endo (a -> a
a (a -> a) -> (a -> a) -> a -> a
forall a. Heyting a => a -> a -> a
<=> a -> a
b)

-------------------------------------------------------------------------------
-- Proxy, Tagged, Const, Identity, Solo
-------------------------------------------------------------------------------

instance Heyting (Proxy a) where
    Proxy a
_ ==> :: Proxy a -> Proxy a -> Proxy a
==> Proxy a
_ = Proxy a
forall k (t :: k). Proxy t
Proxy
    neg :: Proxy a -> Proxy a
neg Proxy a
_   = Proxy a
forall k (t :: k). Proxy t
Proxy
    Proxy a
_ <=> :: Proxy a -> Proxy a -> Proxy a
<=> Proxy a
_ = Proxy a
forall k (t :: k). Proxy t
Proxy

instance Heyting a => Heyting (Identity a) where
    Identity a
a ==> :: Identity a -> Identity a -> Identity a
==> Identity a
b = a -> Identity a
forall a. a -> Identity a
Identity (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
b)
    neg :: Identity a -> Identity a
neg (Identity a
a)          = a -> Identity a
forall a. a -> Identity a
Identity (a -> a
forall a. Heyting a => a -> a
neg a
a)
    Identity a
a <=> :: Identity a -> Identity a -> Identity a
<=> Identity a
b = a -> Identity a
forall a. a -> Identity a
Identity (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
<=> a
b)

instance Heyting a => Heyting (Tagged b a) where
    Tagged a
a ==> :: Tagged b a -> Tagged b a -> Tagged b a
==> Tagged a
b = a -> Tagged b a
forall k (s :: k) b. b -> Tagged s b
Tagged (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
b)
    neg :: Tagged b a -> Tagged b a
neg (Tagged a
a)          = a -> Tagged b a
forall k (s :: k) b. b -> Tagged s b
Tagged (a -> a
forall a. Heyting a => a -> a
neg a
a)
    Tagged a
a <=> :: Tagged b a -> Tagged b a -> Tagged b a
<=> Tagged a
b = a -> Tagged b a
forall k (s :: k) b. b -> Tagged s b
Tagged (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
<=> a
b)

instance Heyting a => Heyting (Const a b) where
    Const a
a ==> :: Const a b -> Const a b -> Const a b
==> Const a
b = a -> Const a b
forall k a (b :: k). a -> Const a b
Const (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
b)
    neg :: Const a b -> Const a b
neg (Const a
a)       = a -> Const a b
forall k a (b :: k). a -> Const a b
Const (a -> a
forall a. Heyting a => a -> a
neg a
a)
    Const a
a <=> :: Const a b -> Const a b -> Const a b
<=> Const a
b = a -> Const a b
forall k a (b :: k). a -> Const a b
Const (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
<=> a
b)

-- | @since 2.0.3
instance Heyting a => Heyting (Solo a) where
    Solo a
a ==> :: Solo a -> Solo a -> Solo a
==> Solo a
b = a -> Solo a
forall a. a -> Solo a
Solo (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
b)
    neg :: Solo a -> Solo a
neg (Solo a
a)      = a -> Solo a
forall a. a -> Solo a
Solo (a -> a
forall a. Heyting a => a -> a
neg a
a)
    Solo a
a <=> :: Solo a -> Solo a -> Solo a
<=> Solo a
b = a -> Solo a
forall a. a -> Solo a
Solo (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
<=> a
b)

-------------------------------------------------------------------------------
-- Sets
-------------------------------------------------------------------------------

instance (Ord a, Finite a) => Heyting (Set.Set a) where
    Set a
x ==> :: Set a -> Set a -> Set a
==> Set a
y = Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set a -> Set a
forall a. Heyting a => a -> a
neg Set a
x) Set a
y

    neg :: Set a -> Set a
neg Set a
xs = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [ a
x | a
x <- [a]
forall a. Finite a => [a]
universeF, a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember a
x Set a
xs]

    Set a
x <=> :: Set a -> Set a -> Set a
<=> Set a
y = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList
        [ a
z
        | a
z <- [a]
forall a. Finite a => [a]
universeF
        , a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member a
z Set a
x Bool -> Bool -> Bool
forall a. Heyting a => a -> a -> a
<=> a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member a
z Set a
y
        ]

instance (Eq a, Hashable a, Finite a) => Heyting (HS.HashSet a) where
    HashSet a
x ==> :: HashSet a -> HashSet a -> HashSet a
==> HashSet a
y = HashSet a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HS.union (HashSet a -> HashSet a
forall a. Heyting a => a -> a
neg HashSet a
x) HashSet a
y

    neg :: HashSet a -> HashSet a
neg HashSet a
xs = [a] -> HashSet a
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HS.fromList [ a
x | a
x <- [a]
forall a. Finite a => [a]
universeF, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a -> HashSet a -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HS.member a
x HashSet a
xs]

    HashSet a
x <=> :: HashSet a -> HashSet a -> HashSet a
<=> HashSet a
y = [a] -> HashSet a
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HS.fromList
        [ a
z
        | a
z <- [a]
forall a. Finite a => [a]
universeF
        , a -> HashSet a -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HS.member a
z HashSet a
x Bool -> Bool -> Bool
forall a. Heyting a => a -> a -> a
<=> a -> HashSet a -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HS.member a
z HashSet a
y
        ]