Add Haddock `/Since: 4.7.0.0/` comments to new symbols
[packages/base.git] / GHC / TypeLits.hs
1 {-# LANGUAGE DataKinds #-} -- to declare the kinds
2 {-# LANGUAGE KindSignatures #-} -- (used all over)
3 {-# LANGUAGE TypeFamilies #-} -- for declaring operators + sing family
4 {-# LANGUAGE TypeOperators #-} -- for declaring operator
5 {-# LANGUAGE EmptyDataDecls #-} -- for declaring the kinds
6 {-# LANGUAGE GADTs #-} -- for examining type nats
7 {-# LANGUAGE PolyKinds #-} -- for Sing family
8 {-# LANGUAGE FlexibleContexts #-}
9 {-# LANGUAGE FlexibleInstances #-}
10 {-# LANGUAGE UndecidableInstances #-}
11 {-# LANGUAGE RankNTypes #-} -- for SingI magic
12 {-# LANGUAGE ScopedTypeVariables #-} -- for SingI magic
13 {-# LANGUAGE ConstraintKinds #-} -- for <=
14 {-# OPTIONS_GHC -XNoImplicitPrelude #-}
15 {-| This module is an internal GHC module. It declares the constants used
16 in the implementation of type-level natural numbers. The programmer interface
17 for working with type-level naturals should be defined in a separate library. -}
18
19 module GHC.TypeLits
20 ( -- * Kinds
21 Nat, Symbol
22
23 -- * Linking type and value level
24 , Sing, SingI, SingE, SingRep, sing, singByProxy, fromSing
25 , SomeSing(..), ToSing(..), SomeNat, SomeSymbol
26
27 -- * Working with singletons
28 , withSing, singThat
29
30 -- * Functions on type nats
31 , type (<=), type (<=?), type (+), type (*), type (^)
32
33 -- * Comparing for equality
34 , type (:~:) (..), eqSingNat, eqSingSym, eqSingBool
35
36 -- * Destructing type-nat singletons.
37 , isZero, IsZero(..)
38
39 -- Commented out; see definition below; SLPJ Jan 13
40 -- , isEven, IsEven(..)
41
42
43 -- * Matching on type-nats
44 , Nat1(..), FromNat1
45
46 -- * Kind parameters
47 , KindIs(..), Demote, DemoteRep
48 , KindOf
49 ) where
50
51 import GHC.Base(Eq((==)), Ord((>=)), Bool(..), ($), otherwise, (.){-, seq)-})
52 import GHC.Num(Integer, (-))
53 import GHC.Base(String)
54 import GHC.Read(Read(..))
55 import GHC.Show(Show(..))
56 import GHC.Prim(magicSingI)
57 import Unsafe.Coerce(unsafeCoerce)
58 -- import Data.Bits(testBit,shiftR)
59 import Data.Maybe(Maybe(..))
60 import Data.List((++))
61
62 -- | (Kind) A kind useful for passing kinds as parameters.
63 data KindIs (a :: *) = KindParam
64
65 {- | A shortcut for naming the kind parameter corresponding to the
66 kind of a some type. For example, @KindOf Int ~ (KindParam :: KindIs *)@,
67 but @KindOf 2 ~ (KindParam :: KindIs Nat)@. -}
68 type KindOf (a :: k) = (KindParam :: KindIs k)
69
70
71 -- | (Kind) This is the kind of type-level natural numbers.
72 data Nat
73
74 -- | (Kind) This is the kind of type-level symbols.
75 data Symbol
76
77
78 --------------------------------------------------------------------------------
79 data family Sing (n :: k)
80
81 newtype instance Sing (n :: Nat) = SNat Integer
82
83 newtype instance Sing (n :: Symbol) = SSym String
84
85 data instance Sing (n :: Bool) where
86 SFalse :: Sing False
87 STrue :: Sing True
88
89 --------------------------------------------------------------------------------
90
91 -- | The class 'SingI' provides a \"smart\" constructor for singleton types.
92 -- There are built-in instances for the singleton types corresponding
93 -- to type literals.
94
95 class SingI a where
96
97 -- | The only value of type @Sing a@
98 sing :: Sing a
99
100 -- | A convenience function to create a singleton value, when
101 -- we have a proxy argument in scope.
102 singByProxy :: SingI n => proxy n -> Sing n
103 singByProxy _ = sing
104
105 instance SingI False where sing = SFalse
106 instance SingI True where sing = STrue
107
108
109 --------------------------------------------------------------------------------
110 -- | Comparison of type-level naturals.
111 type x <= y = (x <=? y) ~ True
112
113 type family (m :: Nat) <=? (n :: Nat) :: Bool
114
115 -- | Addition of type-level naturals.
116 type family (m :: Nat) + (n :: Nat) :: Nat
117
118 -- | Multiplication of type-level naturals.
119 type family (m :: Nat) * (n :: Nat) :: Nat
120
121 -- | Exponentiation of type-level naturals.
122 type family (m :: Nat) ^ (n :: Nat) :: Nat
123
124
125
126
127 --------------------------------------------------------------------------------
128
129 {- | A class that converts singletons of a given kind into values of some
130 representation type (i.e., we "forget" the extra information carried
131 by the singletons, and convert them to ordinary values).
132
133 Note that 'fromSing' is overloaded based on the /kind/ of the values
134 and not their type---all types of a given kind are processed by the
135 same instances.
136 -}
137
138 class (kparam ~ KindParam) => SingE (kparam :: KindIs k) where
139 type DemoteRep kparam :: *
140 fromSing :: Sing (a :: k) -> DemoteRep kparam
141
142 instance SingE (KindParam :: KindIs Nat) where
143 type DemoteRep (KindParam :: KindIs Nat) = Integer
144 fromSing (SNat n) = n
145
146 instance SingE (KindParam :: KindIs Symbol) where
147 type DemoteRep (KindParam :: KindIs Symbol) = String
148 fromSing (SSym s) = s
149
150
151 instance SingE (KindParam :: KindIs Bool) where
152 type DemoteRep (KindParam :: KindIs Bool) = Bool
153 fromSing SFalse = False
154 fromSing STrue = True
155
156
157 {- | A convenient name for the type used to representing the values
158 for a particular singleton family. For example, @Demote 2 ~ Integer@,
159 and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String@. -}
160 type Demote a = DemoteRep (KindOf a)
161
162 {- | A convenience class, useful when we need to both introduce and eliminate
163 a given singleton value. Users should never need to define instances of
164 this classes. -}
165 class (SingI a, SingE (KindOf a)) => SingRep (a :: k)
166 instance (SingI a, SingE (KindOf a)) => SingRep (a :: k)
167
168
169 -- The type of an unknown singletons of a given kind.
170 -- Note that the "type" parameter on this type is really
171 -- a *kind* parameter (this is similar to the trick used in `SingE`).
172 data SomeSing :: KindIs k -> * where
173 SomeSing :: SingI (n::k) => proxy n -> SomeSing (kp :: KindIs k)
174
175 -- | A definition of natural numbers in terms of singletons.
176 type SomeNat = SomeSing (KindParam :: KindIs Nat)
177
178 -- | A definition of strings in terms of singletons.
179 type SomeSymbol = SomeSing (KindParam :: KindIs Symbol)
180
181 -- | The class of function that can promote a representation value
182 -- into a singleton. Like `SingE`, this class overloads based
183 -- on a *kind*.
184 -- The method returns `Maybe` because sometimes
185 -- the representation type contains more values than are supported
186 -- by the singletons.
187 class (kp ~ KindParam) => ToSing (kp :: KindIs k) where
188 toSing :: DemoteRep kp -> Maybe (SomeSing kp)
189
190 instance ToSing (KindParam :: KindIs Nat) where
191 toSing n
192 | n >= 0 = Just (incoherentForgetSing (SNat n))
193 | otherwise = Nothing
194
195 instance ToSing (KindParam :: KindIs Symbol) where
196 toSing n = Just (incoherentForgetSing (SSym n))
197
198 instance ToSing (KindParam :: KindIs Bool) where
199 toSing False = Just (SomeSing SFalse)
200 toSing True = Just (SomeSing STrue)
201
202
203 {- PRIVATE:
204 WARNING: This function has the scary name because,
205 in general, it could lead to incoherent behavior of the `sing` method.
206
207 The reason is that it converts the provided `Sing n` value,
208 into the the evidence for the `SingI` class hidden in `SomeSing`.
209
210 Now, for proper singleton types this should not happen,
211 because if there is only one value of type `Sing n`,
212 then the parameter must be the same as the value of `sing`.
213 However, we have no guarantees about the definition of `Sing a`,
214 or, indeed, the instance of `Sing`.
215
216 We use the function in the instances for `ToSing` for
217 kind `Nat` and `Symbol`, where the use is guaranteed to be safe.
218
219 NOTE: The implementation is a bit of a hack at present,
220 hence all the very special annotation.
221 -}
222 incoherentForgetSing :: forall (n :: k) (kp :: KindIs k). Sing n -> SomeSing kp
223 incoherentForgetSing x = withSingI x it LocalProxy
224 where
225 it :: SingI n => LocalProxy n -> SomeSing kp
226 it = SomeSing
227
228 {-# NOINLINE withSingI #-}
229 withSingI :: Sing n -> (SingI n => a) -> a
230 withSingI x = magicSingI x ((\f -> f) :: () -> ())
231
232
233
234 -- PRIVATE
235 data LocalProxy n = LocalProxy
236
237
238
239
240
241 {- | A convenience function useful when we need to name a singleton value
242 multiple times. Without this function, each use of 'sing' could potentially
243 refer to a different singleton, and one has to use type signatures to
244 ensure that they are the same. -}
245
246 withSing :: SingI a => (Sing a -> b) -> b
247 withSing f = f sing
248
249
250
251 {- | A convenience function that names a singleton satisfying a certain
252 property. If the singleton does not satisfy the property, then the function
253 returns 'Nothing'. The property is expressed in terms of the underlying
254 representation of the singleton. -}
255
256 singThat :: SingRep a => (Demote a -> Bool) -> Maybe (Sing a)
257 singThat p = withSing $ \x -> if p (fromSing x) then Just x else Nothing
258
259
260 instance (SingE (KindOf a), Show (Demote a)) => Show (Sing a) where
261 showsPrec p = showsPrec p . fromSing
262
263 instance (SingRep a, Read (Demote a), Eq (Demote a)) => Read (Sing a) where
264 readsPrec p cs = do (x,ys) <- readsPrec p cs
265 case singThat (== x) of
266 Just y -> [(y,ys)]
267 Nothing -> []
268
269
270
271 --------------------------------------------------------------------------------
272 data IsZero :: Nat -> * where
273 IsZero :: IsZero 0
274 IsSucc :: !(Sing n) -> IsZero (n + 1)
275
276 isZero :: Sing n -> IsZero n
277 isZero (SNat n) | n == 0 = unsafeCoerce IsZero
278 | otherwise = unsafeCoerce (IsSucc (SNat (n-1)))
279
280 instance Show (IsZero n) where
281 show IsZero = "0"
282 show (IsSucc n) = "(" ++ show n ++ " + 1)"
283
284 {- ----------------------------------------------------------------------------
285
286 This IsEven code is commented out for now. The trouble is that the
287 IsEven constructor has an ambiguous type, at least until (+) becomes
288 suitably injective.
289
290 data IsEven :: Nat -> * where
291 IsEvenZero :: IsEven 0
292 IsEven :: !(Sing (n+1)) -> IsEven (2 * n + 2)
293 IsEven :: !(Sing (n)) -> IsEven (2 * n + 1)
294 IsOdd :: !(Sing n) -> IsEven (2 * n + 1)
295
296 isEven :: Sing n -> IsEven n
297 isEven (SNat n) | n == 0 = unsafeCoerce IsEvenZero
298 | testBit n 0 = unsafeCoerce (IsOdd (SNat (n `shiftR` 1)))
299 | otherwise = unsafeCoerce (IsEven (SNat (n `shiftR` 1)))
300
301 instance Show (IsEven n) where
302 show IsEvenZero = "0"
303 show (IsEven x) = "(2 * " ++ show x ++ ")"
304 show (IsOdd x) = "(2 * " ++ show x ++ " + 1)"
305
306 ------------------------------------------------------------------------------ -}
307
308 -- | Unary implementation of natural numbers.
309 -- Used both at the type and at the value level.
310 data Nat1 = Zero | Succ Nat1
311
312 type family FromNat1 (n :: Nat1) :: Nat
313 type instance FromNat1 Zero = 0
314 type instance FromNat1 (Succ n) = 1 + FromNat1 n
315
316 --------------------------------------------------------------------------------
317
318 -- | A type that provides evidence for equality between two types.
319 --
320 -- /Since: 4.7.0.0/
321 data (:~:) :: k -> k -> * where
322 Refl :: a :~: a
323
324 instance Show (a :~: b) where
325 show Refl = "Refl"
326
327 {- | Check if two type-natural singletons of potentially different types
328 are indeed the same, by comparing their runtime representations.
329 -}
330
331 eqSingNat :: Sing (m :: Nat) -> Sing (n :: Nat) -> Maybe (m :~: n)
332 eqSingNat x y
333 | fromSing x == fromSing y = Just (unsafeCoerce Refl)
334 | otherwise = Nothing
335
336
337 {- | Check if two symbol singletons of potentially different types
338 are indeed the same, by comparing their runtime representations.
339 -}
340
341 eqSingSym:: Sing (m :: Symbol) -> Sing (n :: Symbol) -> Maybe (m :~: n)
342 eqSingSym x y
343 | fromSing x == fromSing y = Just (unsafeCoerce Refl)
344 | otherwise = Nothing
345
346
347 eqSingBool :: Sing (m :: Bool) -> Sing (n :: Bool) -> Maybe (m :~: n)
348 eqSingBool STrue STrue = Just Refl
349 eqSingBool SFalse SFalse = Just Refl
350 eqSingBool _ _ = Nothing
351
352
353