    {-# 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 = () -> Dec ()
    forall a. a -> Dec a
    Yes ()

    -- | 'Void' is falsehood.
    --
    -- @since 0.0.5
    instance Decidable Void where
        decide :: Dec Void
    decide = Neg Void -> Dec Void
    forall a. Neg a -> Dec a
    No Neg Void
    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 Dec a
    forall a. Decidable a => Dec a
    decide :: Dec a of
            No Neg a
    nx -> Neg (a, b) -> Dec (a, b)
    forall a. Neg a -> Dec a
    No (\(a, b)
    c -> Neg a
    nx ((a, b) -> a
    forall a b. (a, b) -> a
    fst (a, b)
    c))
            Yes a
    x -> case Dec b
    forall a. Decidable a => Dec a
    decide :: Dec b of
                No Neg b
    ny -> Neg (a, b) -> Dec (a, b)
    forall a. Neg a -> Dec a
    No (\(a, b)
    c -> Neg b
    ny ((a, b) -> b
    forall a b. (a, b) -> b
    snd (a, b)
    c))
                Yes b
    y -> (a, b) -> Dec (a, b)
    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 = ((a -> Void) -> a -> Void
    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 (a -> Neg (Neg a)
    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 a -> a -> Bool
    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) = a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    a a
    b
        compare (No Neg a
    _)  (Yes a
    _) = Bool -> Bool -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Bool
    False Bool
    True
        compare (Yes a
    _) (No Neg a
    _)  = Bool -> Bool -> Ordering
    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) = Neg (Neg a) -> Dec (Neg a)
    forall a. Neg a -> Dec a
    No (a -> Neg (Neg a)
    forall a. a -> Neg (Neg a)
    toNegNeg a
    p)
    decNeg (No Neg a
    np) = Neg a -> Dec (Neg a)
    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 " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> a -> String -> String
    forall a. Show a => Int -> a -> String -> String
    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) = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    p
    decToMaybe (No Neg a
    _)  = Maybe 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 = Dec a
    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 = a -> Dec a
    forall a. a -> Dec a
    Yes a
    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 = Neg a -> Dec a
    forall a. Neg a -> Dec a
    No Neg a
    forall b. a -> b
    forall a b. Absurd a => a -> b
    absurd