e85b36cce51614af1ea536c29b99de3b8e681555
[packages/base.git] / GHC / TypeLits.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE KindSignatures #-}
3 {-# LANGUAGE TypeFamilies #-}
4 {-# LANGUAGE TypeOperators #-}
5 {-# LANGUAGE FlexibleInstances #-}
6 {-# LANGUAGE FlexibleContexts #-}
7 {-# LANGUAGE ScopedTypeVariables #-}
8 {-# LANGUAGE ConstraintKinds #-}
9 {-# LANGUAGE ExistentialQuantification #-}
10 {-# LANGUAGE RankNTypes #-}
11 {-# LANGUAGE UndecidableInstances #-} -- for compiling instances of (==)
12 {-# OPTIONS_GHC -XNoImplicitPrelude #-}
13 {-| This module is an internal GHC module. It declares the constants used
14 in the implementation of type-level natural numbers. The programmer interface
15 for working with type-level naturals should be defined in a separate library.
16
17 /Since: 4.6.0.0/
18 -}
19
20 module GHC.TypeLits
21 ( -- * Kinds
22 Nat, Symbol
23
24 -- * Linking type and value level
25 , KnownNat, natVal
26 , KnownSymbol, symbolVal
27 , SomeNat(..), SomeSymbol(..)
28 , someNatVal, someSymbolVal
29 , sameNat, sameSymbol
30
31
32 -- * Functions on type nats
33 , type (<=), type (<=?), type (+), type (*), type (^), type (-)
34
35 ) where
36
37 import GHC.Base(Eq(..), Ord(..), Bool(True,False), otherwise)
38 import GHC.Num(Integer)
39 import GHC.Base(String)
40 import GHC.Show(Show(..))
41 import GHC.Read(Read(..))
42 import GHC.Prim(magicDict)
43 import Data.Maybe(Maybe(..))
44 import Data.Proxy(Proxy(..))
45 import Data.Type.Equality(type (==), (:~:)(Refl))
46 import Unsafe.Coerce(unsafeCoerce)
47
48 -- | (Kind) This is the kind of type-level natural numbers.
49 data Nat
50
51 -- | (Kind) This is the kind of type-level symbols.
52 data Symbol
53
54
55 --------------------------------------------------------------------------------
56
57 -- | This class gives the integer associated with a type-level natural.
58 -- There are instances of the class for every concrete literal: 0, 1, 2, etc.
59 --
60 -- /Since: 4.7.0.0/
61 class KnownNat (n :: Nat) where
62 natSing :: SNat n
63
64 -- | This class gives the integer associated with a type-level symbol.
65 -- There are instances of the class for every concrete literal: "hello", etc.
66 --
67 -- /Since: 4.7.0.0/
68 class KnownSymbol (n :: Symbol) where
69 symbolSing :: SSymbol n
70
71 -- | /Since: 4.7.0.0/
72 natVal :: forall n proxy. KnownNat n => proxy n -> Integer
73 natVal _ = case natSing :: SNat n of
74 SNat x -> x
75
76 -- | /Since: 4.7.0.0/
77 symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
78 symbolVal _ = case symbolSing :: SSymbol n of
79 SSymbol x -> x
80
81
82
83 -- | This type represents unknown type-level natural numbers.
84 data SomeNat = forall n. KnownNat n => SomeNat (Proxy n)
85 -- ^ /Since: 4.7.0.0/
86
87 -- | This type represents unknown type-level symbols.
88 data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n)
89 -- ^ /Since: 4.7.0.0/
90
91 -- | Convert an integer into an unknown type-level natural.
92 --
93 -- /Since: 4.7.0.0/
94 someNatVal :: Integer -> Maybe SomeNat
95 someNatVal n
96 | n >= 0 = Just (withSNat SomeNat (SNat n) Proxy)
97 | otherwise = Nothing
98
99 -- | Convert a string into an unknown type-level symbol.
100 --
101 -- /Since: 4.7.0.0/
102 someSymbolVal :: String -> SomeSymbol
103 someSymbolVal n = withSSymbol SomeSymbol (SSymbol n) Proxy
104
105
106
107 instance Eq SomeNat where
108 SomeNat x == SomeNat y = natVal x == natVal y
109
110 instance Ord SomeNat where
111 compare (SomeNat x) (SomeNat y) = compare (natVal x) (natVal y)
112
113 instance Show SomeNat where
114 showsPrec p (SomeNat x) = showsPrec p (natVal x)
115
116 instance Read SomeNat where
117 readsPrec p xs = do (a,ys) <- readsPrec p xs
118 case someNatVal a of
119 Nothing -> []
120 Just n -> [(n,ys)]
121
122
123 instance Eq SomeSymbol where
124 SomeSymbol x == SomeSymbol y = symbolVal x == symbolVal y
125
126 instance Ord SomeSymbol where
127 compare (SomeSymbol x) (SomeSymbol y) = compare (symbolVal x) (symbolVal y)
128
129 instance Show SomeSymbol where
130 showsPrec p (SomeSymbol x) = showsPrec p (symbolVal x)
131
132 instance Read SomeSymbol where
133 readsPrec p xs = [ (someSymbolVal a, ys) | (a,ys) <- readsPrec p xs ]
134
135 type family EqNat (a :: Nat) (b :: Nat) where
136 EqNat a a = True
137 EqNat a b = False
138 type instance a == b = EqNat a b
139
140 type family EqSymbol (a :: Symbol) (b :: Symbol) where
141 EqSymbol a a = True
142 EqSymbol a b = False
143 type instance a == b = EqSymbol a b
144
145 --------------------------------------------------------------------------------
146
147 infix 4 <=?, <=
148 infixl 6 +, -
149 infixl 7 *
150 infixr 8 ^
151
152 -- | Comparison of type-level naturals, as a constraint.
153 type x <= y = (x <=? y) ~ True
154
155 -- | Comparison of type-level naturals, as a function.
156 type family (m :: Nat) <=? (n :: Nat) :: Bool
157
158 -- | Addition of type-level naturals.
159 type family (m :: Nat) + (n :: Nat) :: Nat
160
161 -- | Multiplication of type-level naturals.
162 type family (m :: Nat) * (n :: Nat) :: Nat
163
164 -- | Exponentiation of type-level naturals.
165 type family (m :: Nat) ^ (n :: Nat) :: Nat
166
167 -- | Subtraction of type-level naturals.
168 --
169 -- /Since: 4.7.0.0/
170 type family (m :: Nat) - (n :: Nat) :: Nat
171
172
173 --------------------------------------------------------------------------------
174
175 -- | We either get evidence that this function was instantiated with the
176 -- same type-level numbers, or 'Nothing'.
177 --
178 -- /Since: 4.7.0.0/
179 sameNat :: (KnownNat a, KnownNat b) =>
180 Proxy a -> Proxy b -> Maybe (a :~: b)
181 sameNat x y
182 | natVal x == natVal y = Just (unsafeCoerce Refl)
183 | otherwise = Nothing
184
185 -- | We either get evidence that this function was instantiated with the
186 -- same type-level symbols, or 'Nothing'.
187 --
188 -- /Since: 4.7.0.0/
189 sameSymbol :: (KnownSymbol a, KnownSymbol b) =>
190 Proxy a -> Proxy b -> Maybe (a :~: b)
191 sameSymbol x y
192 | symbolVal x == symbolVal y = Just (unsafeCoerce Refl)
193 | otherwise = Nothing
194
195 --------------------------------------------------------------------------------
196 -- PRIVATE:
197
198 newtype SNat (n :: Nat) = SNat Integer
199 newtype SSymbol (s :: Symbol) = SSymbol String
200
201 data WrapN a b = WrapN (KnownNat a => Proxy a -> b)
202 data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)
203
204 -- See Note [magicDictId magic] in "basicType/MkId.hs"
205 withSNat :: (KnownNat a => Proxy a -> b)
206 -> SNat a -> Proxy a -> b
207 withSNat f x y = magicDict (WrapN f) x y
208
209 -- See Note [magicDictId magic] in "basicType/MkId.hs"
210 withSSymbol :: (KnownSymbol a => Proxy a -> b)
211 -> SSymbol a -> Proxy a -> b
212 withSSymbol f x y = magicDict (WrapS f) x y
213
214