-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Decidable propositions.
--   
--   This package provides a <tt>Dec</tt> type.
--   
--   <pre>
--   type Not a = a -&gt; Void
--   
--   data Dec a
--       = Yes a
--       | No (Not a)
--   </pre>
@package dec
@version 0.0.3

module Data.Type.Dec

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

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

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

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

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

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

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

-- | Flip <a>Dec</a> branches.
decNeg :: Dec a -> Dec (Neg a)

-- | Show <a>Dec</a>.
--   
--   <pre>
--   &gt;&gt;&gt; decShow $ Yes ()
--   "Yes ()"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; decShow $ No id
--   "No &lt;toVoid&gt;"
--   </pre>
decShow :: Show a => Dec a -> String

-- | Convert <tt><a>Dec</a> a</tt> to <tt><a>Maybe</a> a</tt>, forgetting
--   the <a>No</a> evidence.
decToMaybe :: Dec a -> Maybe a

-- | Convert <a>Dec</a> to <a>Bool</a>, forgetting the evidence.
decToBool :: Dec a -> Bool
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Type.Dec.Dec a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Type.Dec.Dec a)