Add Haddock `/Since: 4.7.0.0/` comments to new symbols
[packages/base.git] / Data / Type / Equality.hs
1 {-# LANGUAGE DeriveGeneric #-}
2 {-# LANGUAGE TypeOperators #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE EmptyDataDecls #-}
5 {-# LANGUAGE FlexibleInstances #-}
6 {-# LANGUAGE StandaloneDeriving #-}
7 {-# LANGUAGE NoImplicitPrelude #-}
8 {-# LANGUAGE PolyKinds #-}
9
10 -----------------------------------------------------------------------------
11 -- |
12 -- Module : Data.Type.Equality
13 -- License : BSD-style (see the LICENSE file in the distribution)
14 --
15 -- Maintainer : libraries@haskell.org
16 -- Stability : experimental
17 -- Portability : not portable
18 --
19 -- Definition of propositional equality @(:=:)@. Pattern-matching on a variable
20 -- of type @(a :=: b)@ produces a proof that @a ~ b@.
21 --
22 -- /Since: 4.7.0.0/
23 -----------------------------------------------------------------------------
24
25
26
27 module Data.Type.Equality where
28
29 import Data.Maybe
30 import GHC.Enum
31 import GHC.Show
32 import GHC.Read
33 import GHC.Base
34
35 infix 4 :=:
36
37 -- | Propositional equality. If @a :=: b@ is inhabited by some terminating
38 -- value, then the type @a@ is the same as the type @b@. To use this equality
39 -- in practice, pattern-match on the @a :=: b@ to get out the @Refl@ constructor;
40 -- in the body of the pattern-match, the compiler knows that @a ~ b@.
41 --
42 -- /Since: 4.7.0.0/
43 data a :=: b where
44 Refl :: a :=: a
45
46 -- with credit to Conal Elliott for 'ty', Erik Hesselink & Martijn van
47 -- Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif
48 -- for 'type-eq'
49
50 -- | Symmetry of equality
51 sym :: (a :=: b) -> (b :=: a)
52 sym Refl = Refl
53
54 -- | Transitivity of equality
55 trans :: (a :=: b) -> (b :=: c) -> (a :=: c)
56 trans Refl Refl = Refl
57
58 -- | Type-safe cast, using propositional equality
59 coerce :: (a :=: b) -> a -> b
60 coerce Refl x = x
61
62 -- | Lift equality into a unary type constructor
63 liftEq :: (a :=: b) -> (f a :=: f b)
64 liftEq Refl = Refl
65
66 -- | Lift equality into a binary type constructor
67 liftEq2 :: (a :=: a') -> (b :=: b') -> (f a b :=: f a' b')
68 liftEq2 Refl Refl = Refl
69
70 -- | Lift equality into a ternary type constructor
71 liftEq3 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> (f a b c :=: f a' b' c')
72 liftEq3 Refl Refl Refl = Refl
73
74 -- | Lift equality into a quaternary type constructor
75 liftEq4 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> (d :=: d')
76 -> (f a b c d :=: f a' b' c' d')
77 liftEq4 Refl Refl Refl Refl = Refl
78
79 -- | Lower equality from a parameterized type into the parameters
80 lower :: (f a :=: f b) -> a :=: b
81 lower Refl = Refl
82
83 deriving instance Eq (a :=: b)
84 deriving instance Show (a :=: b)
85 deriving instance Ord (a :=: b)
86
87 instance Read (a :=: a) where
88 readsPrec d = readParen (d > 10) (\r -> [(Refl, s) | ("Refl",s) <- lex r ])
89
90 instance Enum (a :=: a) where
91 toEnum 0 = Refl
92 toEnum _ = error "Data.Type.Equality.toEnum: bad argument"
93
94 fromEnum Refl = 0
95
96 instance Bounded (a :=: a) where
97 minBound = Refl
98 maxBound = Refl
99
100 -- | This class contains types where you can learn the equality of two types
101 -- from information contained in /terms/. Typically, only singleton types should
102 -- inhabit this class.
103 class EqualityT f where
104 -- | Conditionally prove the equality of @a@ and @b@.
105 equalsT :: f a -> f b -> Maybe (a :=: b)
106
107 instance EqualityT ((:=:) a) where
108 equalsT Refl Refl = Just Refl
109