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