{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE EmptyDataDeriving #-} {-# LANGUAGE Safe #-} {-# LANGUAGE StandaloneDeriving #-} ----------------------------------------------------------------------------- -- | -- Copyright : (C) 2008-2014 Edward Kmett -- License : BSD-style (see the file libraries/base/LICENSE) -- -- Maintainer : Edward Kmett <ekmett@gmail.com> -- Stability : provisional -- Portability : portable -- -- A logically uninhabited data type, used to indicate that a given -- term should not exist. -- -- @since 4.8.0.0 ---------------------------------------------------------------------------- module Data.Void ( Void , absurd , vacuous ) where import Control.Exception import Data.Data import Data.Ix import GHC.Generics import Data.Semigroup (Semigroup(..), stimesIdempotent) -- | Uninhabited data type -- -- @since 4.8.0.0 data Void deriving ( Eq -- ^ @since 4.8.0.0 , Data -- ^ @since 4.8.0.0 , Generic -- ^ @since 4.8.0.0 , Ord -- ^ @since 4.8.0.0 , Read -- ^ Reading a 'Void' value is always a parse error, considering -- 'Void' as a data type with no constructors. -- -- @since 4.8.0.0 , Show -- ^ @since 4.8.0.0 ) -- | @since 4.8.0.0 instance Ix Void where range :: (Void, Void) -> [Void] range (Void, Void) _ = [] index :: (Void, Void) -> Void -> Int index (Void, Void) _ = Void -> Int forall a. Void -> a absurd inRange :: (Void, Void) -> Void -> Bool inRange (Void, Void) _ = Void -> Bool forall a. Void -> a absurd rangeSize :: (Void, Void) -> Int rangeSize (Void, Void) _ = Int 0 -- | @since 4.8.0.0 instance Exception Void -- | @since 4.9.0.0 instance Semigroup Void where Void a <> :: Void -> Void -> Void <> Void _ = Void a stimes :: b -> Void -> Void stimes = b -> Void -> Void forall b a. Integral b => b -> a -> a stimesIdempotent -- | Since 'Void' values logically don't exist, this witnesses the -- logical reasoning tool of \"ex falso quodlibet\". -- -- >>> let x :: Either Void Int; x = Right 5 -- >>> :{ -- case x of -- Right r -> r -- Left l -> absurd l -- :} -- 5 -- -- @since 4.8.0.0 absurd :: Void -> a absurd :: Void -> a absurd Void a = case Void a of {} -- | If 'Void' is uninhabited then any 'Functor' that holds only -- values of type 'Void' is holding no values. -- -- Using @ApplicativeDo@: \'@'vacuous' theVoid@\' can be understood as the -- @do@ expression -- -- @ -- do void <- theVoid -- pure (absurd void) -- @ -- -- with an inferred @Functor@ constraint. -- -- @since 4.8.0.0 vacuous :: Functor f => f Void -> f a vacuous :: f Void -> f a vacuous = (Void -> a) -> f Void -> f a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Void -> a forall a. Void -> a absurd