{-# 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 forall a. Heyting 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 forall a. Heyting a => a -> a -> a
==> a
y) forall a. Lattice a => a -> a -> a
/\ (a
y 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
(<=>) = 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 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 forall a. Heyting a => a -> a -> a
<=> b -> a
g b
x
    neg :: (b -> a) -> b -> a
neg b -> a
f   = forall a. Heyting a => a -> a
neg 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 forall a. Heyting a => a -> a -> a
==> Bool
b)
    neg :: All -> All
neg (All Bool
a)     = Bool -> All
All (forall a. Heyting a => a -> a
neg Bool
a)
    All Bool
a <=> :: All -> All -> All
<=> All Bool
b = Bool -> All
All (Bool
a 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 forall a. Heyting a => a -> a -> a
==> Bool
b)
    neg :: Any -> Any
neg (Any Bool
a)     = Bool -> Any
Any (forall a. Heyting a => a -> a
neg Bool
a)
    Any Bool
a <=> :: Any -> Any -> Any
<=> Any Bool
b = Bool -> Any
Any (Bool
a 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 = forall a. (a -> a) -> Endo a
Endo (a -> a
a forall a. Heyting a => a -> a -> a
==> a -> a
b)
    neg :: Endo a -> Endo a
neg (Endo a -> a
a)      = forall a. (a -> a) -> Endo a
Endo (forall a. Heyting a => a -> a
neg a -> a
a)
    Endo a -> a
a <=> :: Endo a -> Endo a -> Endo a
<=> Endo a -> a
b = forall a. (a -> a) -> Endo a
Endo (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
_ = forall {k} (t :: k). Proxy t
Proxy
    neg :: Proxy a -> Proxy a
neg Proxy a
_   = forall {k} (t :: k). Proxy t
Proxy
    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 = forall a. a -> Identity a
Identity (a
a forall a. Heyting a => a -> a -> a
==> a
b)
    neg :: Identity a -> Identity a
neg (Identity a
a)          = forall a. a -> Identity a
Identity (forall a. Heyting a => a -> a
neg a
a)
    Identity a
a <=> :: Identity a -> Identity a -> Identity a
<=> Identity a
b = forall a. a -> Identity a
Identity (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 = forall {k} (s :: k) b. b -> Tagged s b
Tagged (a
a forall a. Heyting a => a -> a -> a
==> a
b)
    neg :: Tagged b a -> Tagged b a
neg (Tagged a
a)          = forall {k} (s :: k) b. b -> Tagged s b
Tagged (forall a. Heyting a => a -> a
neg a
a)
    Tagged a
a <=> :: Tagged b a -> Tagged b a -> Tagged b a
<=> Tagged a
b = forall {k} (s :: k) b. b -> Tagged s b
Tagged (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 = forall {k} a (b :: k). a -> Const a b
Const (a
a forall a. Heyting a => a -> a -> a
==> a
b)
    neg :: Const a b -> Const a b
neg (Const a
a)       = forall {k} a (b :: k). a -> Const a b
Const (forall a. Heyting a => a -> a
neg a
a)
    Const a
a <=> :: Const a b -> Const a b -> Const a b
<=> Const a
b = forall {k} a (b :: k). a -> Const a b
Const (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 = forall a. a -> Solo a
Solo (a
a forall a. Heyting a => a -> a -> a
==> a
b)
    neg :: Solo a -> Solo a
neg (Solo a
a)      = forall a. a -> Solo a
Solo (forall a. Heyting a => a -> a
neg a
a)
    Solo a
a <=> :: Solo a -> Solo a -> Solo a
<=> Solo a
b = forall a. a -> Solo a
Solo (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 = forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall a. Heyting a => a -> a
neg Set a
x) Set a
y

    neg :: Set a -> Set a
neg Set a
xs = forall a. Ord a => [a] -> Set a
Set.fromList [ a
x | a
x <- forall a. Finite a => [a]
universeF, 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 = forall a. Ord a => [a] -> Set a
Set.fromList
        [ a
z
        | a
z <- forall a. Finite a => [a]
universeF
        , forall a. Ord a => a -> Set a -> Bool
Set.member a
z Set a
x forall a. Heyting a => a -> a -> a
<=> 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 = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HS.union (forall a. Heyting a => a -> a
neg HashSet a
x) HashSet a
y

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