Add functions for comparing type-level Nats and Symbols.
[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 literals
33 , type (<=), type (<=?), type (+), type (*), type (^), type (-)
34 , CmpNat, CmpSymbol
35
36 ) where
37
38 import GHC.Base(Eq(..), Ord(..), Bool(True,False), Ordering(..), otherwise)
39 import GHC.Num(Integer)
40 import GHC.Base(String)
41 import GHC.Show(Show(..))
42 import GHC.Read(Read(..))
43 import GHC.Prim(magicDict)
44 import Data.Maybe(Maybe(..))
45 import Data.Proxy(Proxy(..))
46 import Data.Type.Equality(type (==), (:~:)(Refl))
47 import Unsafe.Coerce(unsafeCoerce)
48
49 -- | (Kind) This is the kind of type-level natural numbers.
50 data Nat
51
52 -- | (Kind) This is the kind of type-level symbols.
53 data Symbol
54
55
56 --------------------------------------------------------------------------------
57
58 -- | This class gives the integer associated with a type-level natural.
59 -- There are instances of the class for every concrete literal: 0, 1, 2, etc.
60 --
61 -- /Since: 4.7.0.0/
62 class KnownNat (n :: Nat) where
63 natSing :: SNat n
64
65 -- | This class gives the integer associated with a type-level symbol.
66 -- There are instances of the class for every concrete literal: "hello", etc.
67 --
68 -- /Since: 4.7.0.0/
69 class KnownSymbol (n :: Symbol) where
70 symbolSing :: SSymbol n
71
72 -- | /Since: 4.7.0.0/
73 natVal :: forall n proxy. KnownNat n => proxy n -> Integer
74 natVal _ = case natSing :: SNat n of
75 SNat x -> x
76
77 -- | /Since: 4.7.0.0/
78 symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
79 symbolVal _ = case symbolSing :: SSymbol n of
80 SSymbol x -> x
81
82
83
84 -- | This type represents unknown type-level natural numbers.
85 data SomeNat = forall n. KnownNat n => SomeNat (Proxy n)
86 -- ^ /Since: 4.7.0.0/
87
88 -- | This type represents unknown type-level symbols.
89 data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n)
90 -- ^ /Since: 4.7.0.0/
91
92 -- | Convert an integer into an unknown type-level natural.
93 --
94 -- /Since: 4.7.0.0/
95 someNatVal :: Integer -> Maybe SomeNat
96 someNatVal n
97 | n >= 0 = Just (withSNat SomeNat (SNat n) Proxy)
98 | otherwise = Nothing
99
100 -- | Convert a string into an unknown type-level symbol.
101 --
102 -- /Since: 4.7.0.0/
103 someSymbolVal :: String -> SomeSymbol
104 someSymbolVal n = withSSymbol SomeSymbol (SSymbol n) Proxy
105
106
107
108 instance Eq SomeNat where
109 SomeNat x == SomeNat y = natVal x == natVal y
110
111 instance Ord SomeNat where
112 compare (SomeNat x) (SomeNat y) = compare (natVal x) (natVal y)
113
114 instance Show SomeNat where
115 showsPrec p (SomeNat x) = showsPrec p (natVal x)
116
117 instance Read SomeNat where
118 readsPrec p xs = do (a,ys) <- readsPrec p xs
119 case someNatVal a of
120 Nothing -> []
121 Just n -> [(n,ys)]
122
123
124 instance Eq SomeSymbol where
125 SomeSymbol x == SomeSymbol y = symbolVal x == symbolVal y
126
127 instance Ord SomeSymbol where
128 compare (SomeSymbol x) (SomeSymbol y) = compare (symbolVal x) (symbolVal y)
129
130 instance Show SomeSymbol where
131 showsPrec p (SomeSymbol x) = showsPrec p (symbolVal x)
132
133 instance Read SomeSymbol where
134 readsPrec p xs = [ (someSymbolVal a, ys) | (a,ys) <- readsPrec p xs ]
135
136 type family EqNat (a :: Nat) (b :: Nat) where
137 EqNat a a = True
138 EqNat a b = False
139 type instance a == b = EqNat a b
140
141 type family EqSymbol (a :: Symbol) (b :: Symbol) where
142 EqSymbol a a = True
143 EqSymbol a b = False
144 type instance a == b = EqSymbol a b
145
146 --------------------------------------------------------------------------------
147
148 infix 4 <=?, <=
149 infixl 6 +, -
150 infixl 7 *
151 infixr 8 ^
152
153 -- | Comparison of type-level naturals, as a constraint.
154 type x <= y = (x <=? y) ~ True
155
156 -- | Comparison of type-level naturals, as a function.
157 type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering
158
159 -- | Comparison of type-level symbols, as a function.
160 type family CmpNat (m :: Nat) (n :: Nat) :: Ordering
161
162 -- | Comparison of type-level naturals, as a function.
163 type family (m :: Nat) <=? (n :: Nat) :: Bool
164
165 -- | Addition of type-level naturals.
166 type family (m :: Nat) + (n :: Nat) :: Nat
167
168 -- | Multiplication of type-level naturals.
169 type family (m :: Nat) * (n :: Nat) :: Nat
170
171 -- | Exponentiation of type-level naturals.
172 type family (m :: Nat) ^ (n :: Nat) :: Nat
173
174 -- | Subtraction of type-level naturals.
175 --
176 -- /Since: 4.7.0.0/
177 type family (m :: Nat) - (n :: Nat) :: Nat
178
179
180 --------------------------------------------------------------------------------
181
182 -- | We either get evidence that this function was instantiated with the
183 -- same type-level numbers, or 'Nothing'.
184 --
185 -- /Since: 4.7.0.0/
186 sameNat :: (KnownNat a, KnownNat b) =>
187 Proxy a -> Proxy b -> Maybe (a :~: b)
188 sameNat x y
189 | natVal x == natVal y = Just (unsafeCoerce Refl)
190 | otherwise = Nothing
191
192 -- | We either get evidence that this function was instantiated with the
193 -- same type-level symbols, or 'Nothing'.
194 --
195 -- /Since: 4.7.0.0/
196 sameSymbol :: (KnownSymbol a, KnownSymbol b) =>
197 Proxy a -> Proxy b -> Maybe (a :~: b)
198 sameSymbol x y
199 | symbolVal x == symbolVal y = Just (unsafeCoerce Refl)
200 | otherwise = Nothing
201
202 --------------------------------------------------------------------------------
203 -- PRIVATE:
204
205 newtype SNat (n :: Nat) = SNat Integer
206 newtype SSymbol (s :: Symbol) = SSymbol String
207
208 data WrapN a b = WrapN (KnownNat a => Proxy a -> b)
209 data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)
210
211 -- See Note [magicDictId magic] in "basicType/MkId.hs"
212 withSNat :: (KnownNat a => Proxy a -> b)
213 -> SNat a -> Proxy a -> b
214 withSNat f x y = magicDict (WrapN f) x y
215
216 -- See Note [magicDictId magic] in "basicType/MkId.hs"
217 withSSymbol :: (KnownSymbol a => Proxy a -> b)
218 -> SSymbol a -> Proxy a -> b
219 withSSymbol f x y = magicDict (WrapS f) x y
220
221