{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Data.Type.Dec (
    -- * Types
    Neg,
    Dec (..),
    Decidable (..),
    -- * Neg combinators
    toNegNeg,
    tripleNeg,
    contradict,
    contraposition,
    -- * Dec combinators
    decNeg,
    decShow,
    decToMaybe,
    decToBool,

    -- * Boring
    -- | @'Dec' a@ can be 'Boring' in two ways: When 'a' is 'Boring' or 'Absurd'.
    boringYes,
    absurdNo,
    ) where

import Data.Void (Void)
import Data.Boring (Absurd (..), Boring (..))

-- | Intuitionistic negation.
type Neg a = a -> Void

-- | Decidable (nullary) relations.
data Dec a
    = Yes a
    | No (Neg a)

-- | Class of decidable types.
--
-- == Law
--
-- @a@ should be a Proposition, i.e. the 'Yes' answers should be unique.
--
-- /Note:/ We'd want to have decidable equality @:~:@ here too,
-- but that seems to be a deep dive into singletons.
class Decidable a where
    decide :: Dec a

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

-- | @()@ is truth.
--
-- @since 0.0.5
instance Decidable () where
    decide :: Dec ()
decide = forall a. a -> Dec a
Yes ()

-- | 'Void' is falsehood.
--
-- @since 0.0.5
instance Decidable Void where
    decide :: Dec Void
decide = forall a. Neg a -> Dec a
No forall a. a -> a
id

-- | Products of decidable propositions are decidable
--
-- @since 0.0.5
instance (Decidable a, Decidable b) => Decidable (a, b) where
    decide :: Dec (a, b)
decide = case forall a. Decidable a => Dec a
decide :: Dec a of
        No Neg a
nx -> forall a. Neg a -> Dec a
No (\(a, b)
c -> Neg a
nx (forall a b. (a, b) -> a
fst (a, b)
c))
        Yes a
x -> case forall a. Decidable a => Dec a
decide :: Dec b of
            No Neg b
ny -> forall a. Neg a -> Dec a
No (\(a, b)
c -> Neg b
ny (forall a b. (a, b) -> b
snd (a, b)
c))
            Yes b
y -> forall a. a -> Dec a
Yes (a
x, b
y)

-------------------------------------------------------------------------------
-- Neg combinators
-------------------------------------------------------------------------------

-- | We can negate anything twice.
--
-- Double-negation elimination is inverse of 'toNegNeg' and generally
-- impossible.
toNegNeg :: a -> Neg (Neg a)
toNegNeg :: forall a. a -> Neg (Neg a)
toNegNeg a
x = (forall a b. (a -> b) -> a -> b
$ a
x)

-- | Triple negation can be reduced to a single one.
tripleNeg :: Neg (Neg (Neg a)) -> Neg a
tripleNeg :: forall a. Neg (Neg (Neg a)) -> Neg a
tripleNeg Neg (Neg (Neg a))
f a
a = Neg (Neg (Neg a))
f (forall a. a -> Neg (Neg a)
toNegNeg a
a)

-- | Weak contradiction.
contradict :: (a -> Neg b) -> b -> Neg a
contradict :: forall a b. (a -> Neg b) -> b -> Neg a
contradict a -> Neg b
f b
b a
a = a -> Neg b
f a
a b
b

-- | A variant of contraposition.
contraposition :: (a -> b) -> Neg b -> Neg a
contraposition :: forall a b. (a -> b) -> Neg b -> Neg a
contraposition a -> b
f Neg b
nb a
a = Neg b
nb (a -> b
f a
a)

-------------------------------------------------------------------------------
-- Dec combinators
-------------------------------------------------------------------------------

instance Eq a => Eq (Dec a) where
    Yes a
x == :: Dec a -> Dec a -> Bool
== Yes a
y = a
x forall a. Eq a => a -> a -> Bool
== a
y
    Yes a
_ == No Neg a
_   = Bool
False
    No Neg a
_  == Yes a
_  = Bool
False
    No Neg a
_  == No Neg a
_   = Bool
True  -- @'Not a' is a /h-Prop/ so all values are equal.

-- | 'decToBool' respects this ordering.
--
-- /Note:/ yet if you have @p :: a@ and @p :: 'Neg' a@, something is wrong.
--
instance Ord a => Ord (Dec a) where
    compare :: Dec a -> Dec a -> Ordering
compare (Yes a
a) (Yes a
b) = forall a. Ord a => a -> a -> Ordering
compare a
a a
b
    compare (No Neg a
_)  (Yes a
_) = forall a. Ord a => a -> a -> Ordering
compare Bool
False Bool
True
    compare (Yes a
_) (No Neg a
_)  = forall a. Ord a => a -> a -> Ordering
compare Bool
True Bool
False
    compare (No Neg a
_)  (No Neg a
_)  = Ordering
EQ

-- | Flip 'Dec' branches.
decNeg :: Dec a -> Dec (Neg a)
decNeg :: forall a. Dec a -> Dec (Neg a)
decNeg (Yes a
p) = forall a. Neg a -> Dec a
No (forall a. a -> Neg (Neg a)
toNegNeg a
p)
decNeg (No Neg a
np) = forall a. a -> Dec a
Yes Neg a
np

-- | Show 'Dec'.
--
-- >>> decShow $ Yes ()
-- "Yes ()"
--
-- >>> decShow $ No id
-- "No <toVoid>"
--
decShow :: Show a => Dec a -> String
decShow :: forall a. Show a => Dec a -> String
decShow (Yes a
x) = String
"Yes " forall a. [a] -> [a] -> [a]
++ forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 a
x String
""
decShow (No Neg a
_)  = String
"No <toVoid>"

-- | Convert @'Dec' a@ to @'Maybe' a@, forgetting the 'No' evidence.
decToMaybe :: Dec a -> Maybe a
decToMaybe :: forall a. Dec a -> Maybe a
decToMaybe (Yes a
p) = forall a. a -> Maybe a
Just a
p
decToMaybe (No Neg a
_)  = forall a. Maybe a
Nothing

-- | Convert 'Dec' to 'Bool', forgetting the evidence.
decToBool :: Dec a -> Bool
decToBool :: forall a. Dec a -> Bool
decToBool (Yes a
_) = Bool
True
decToBool (No Neg a
_)  = Bool
False

-------------------------------------------------------------------------------
-- Boring
-------------------------------------------------------------------------------

-- | This relies on the fact that @a@ is /proposition/ in h-Prop sense.
--
-- @since 0.0.5
instance Decidable a => Boring (Dec a) where
    boring :: Dec a
boring = forall a. Decidable a => Dec a
decide

-- | 'Yes', it's 'boring'.
--
-- @since 0.0.5
boringYes :: Boring a => Dec a
boringYes :: forall a. Boring a => Dec a
boringYes = forall a. a -> Dec a
Yes forall a. Boring a => a
boring

-- | 'No', it's 'absurd'.
--
-- @since 0.0.5
absurdNo :: Absurd a => Dec a
absurdNo :: forall a. Absurd a => Dec a
absurdNo = forall a. Neg a -> Dec a
No forall a b. Absurd a => a -> b
absurd