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