Dec.hs

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

import Data.Void (Void)

-- | 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

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

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

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

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

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

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

instance Eq a => Eq (Dec a) where
    Yes x == Yes y = x == y
    Yes _ == No _   = False
    No _  == Yes _  = False
    No _  == No _   = 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 (Yes a) (Yes b) = compare a b
    compare (No _)  (Yes _) = compare False True
    compare (Yes _) (No _)  = compare True False
    compare (No _)  (No _)  = EQ

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

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

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

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