1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
{-# LANGUAGE TypeFamilyDependencies, Safe, PolyKinds #-}
{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module : Data.Type.Bool
-- License : BSD-style (see the LICENSE file in the distribution)
--
-- Maintainer : libraries@haskell.org
-- Stability : experimental
-- Portability : not portable
--
-- Basic operations on type-level Booleans.
--
-- @since 4.7.0.0
-----------------------------------------------------------------------------
module Data.Type.Bool (
If, type (&&), type (||), Not
) where
import Data.Bool
-- This needs to be in base because (&&) is used in Data.Type.Equality.
-- The other functions do not need to be in base, but seemed to be appropriate
-- here.
-- | Type-level "If". @If True a b@ ==> @a@; @If False a b@ ==> @b@
type family If cond tru fls where
If 'True tru fls = tru
If 'False tru fls = fls
-- | Type-level "and"
type family a && b where
'False && a = 'False
'True && a = a
a && 'False = 'False
a && 'True = a
a && a = a
infixr 3 &&
-- | Type-level "or"
type family a || b where
'False || a = a
'True || a = 'True
a || 'False = a
a || 'True = 'True
a || a = a
infixr 2 ||
-- | Type-level "not". An injective type family since @4.10.0.0@.
--
-- @since 4.7.0.0
type family Not a = res | res -> a where
Not 'False = 'True
Not 'True = 'False
|
