62b0241d13b77321c1c4ee732efd4f714eff1e03
[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 -----------------------------------------------------------------------------
23
24
25
26 module Data.Type.Equality where
27
28 import Data.Maybe
29 import GHC.Enum
30 import GHC.Show
31 import GHC.Read
32 import GHC.Base
33
34 infix 4 :=:
35
36 -- | Propositional equality. If @a :=: b@ is inhabited by some terminating
37 -- value, then the type @a@ is the same as the type @b@. To use this equality
38 -- in practice, pattern-match on the @a :=: b@ to get out the @Refl@ constructor;
39 -- in the body of the pattern-match, the compiler knows that @a ~ b@.
40 data a :=: b where
41 Refl :: a :=: a
42
43 -- with credit to Conal Elliott for 'ty', Erik Hesselink & Martijn van
44 -- Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif
45 -- for 'type-eq'
46
47 -- | Symmetry of equality
48 sym :: (a :=: b) -> (b :=: a)
49 sym Refl = Refl
50
51 -- | Transitivity of equality
52 trans :: (a :=: b) -> (b :=: c) -> (a :=: c)
53 trans Refl Refl = Refl
54
55 -- | Type-safe cast, using propositional equality
56 coerce :: (a :=: b) -> a -> b
57 coerce Refl x = x
58
59 -- | Lift equality into a unary type constructor
60 liftEq :: (a :=: b) -> (f a :=: f b)
61 liftEq Refl = Refl
62
63 -- | Lift equality into a binary type constructor
64 liftEq2 :: (a :=: a') -> (b :=: b') -> (f a b :=: f a' b')
65 liftEq2 Refl Refl = Refl
66
67 -- | Lift equality into a ternary type constructor
68 liftEq3 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> (f a b c :=: f a' b' c')
69 liftEq3 Refl Refl Refl = Refl
70
71 -- | Lift equality into a quaternary type constructor
72 liftEq4 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> (d :=: d')
73 -> (f a b c d :=: f a' b' c' d')
74 liftEq4 Refl Refl Refl Refl = Refl
75
76 -- | Lower equality from a parameterized type into the parameters
77 lower :: (f a :=: f b) -> a :=: b
78 lower Refl = Refl
79
80 deriving instance Eq (a :=: b)
81 deriving instance Show (a :=: b)
82 deriving instance Ord (a :=: b)
83
84 instance Read (a :=: a) where
85 readsPrec d = readParen (d > 10) (\r -> [(Refl, s) | ("Refl",s) <- lex r ])
86
87 instance Enum (a :=: a) where
88 toEnum 0 = Refl
89 toEnum _ = error "Data.Type.Equality.toEnum: bad argument"
90
91 fromEnum Refl = 0
92
93 instance Bounded (a :=: a) where
94 minBound = Refl
95 maxBound = Refl
96
97 -- | This class contains types where you can learn the equality of two types
98 -- from information contained in /terms/. Typically, only singleton types should
99 -- inhabit this class.
100 class EqualityT f where
101 -- | Conditionally prove the equality of @a@ and @b@.
102 equalsT :: f a -> f b -> Maybe (a :=: b)
103
104 instance EqualityT ((:=:) a) where
105 equalsT Refl Refl = Just Refl
106