Remove all but the basic operations on type-level literals.
[packages/base.git] / GHC / TypeLits.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE KindSignatures #-}
3 {-# LANGUAGE TypeFamilies #-}
4 {-# LANGUAGE TypeOperators #-}
5 {-# LANGUAGE PolyKinds #-}
6 {-# LANGUAGE FlexibleInstances #-}
7 {-# LANGUAGE UndecidableInstances #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE ConstraintKinds #-}
10 {-# LANGUAGE ExistentialQuantification #-}
11 {-# LANGUAGE RankNTypes #-}
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(..), KnownSymbol(..)
26 , SomeNat(..), SomeSymbol(..)
27 , someNatVal, someSymVal
28
29 -- * Functions on type nats
30 , type (<=), type (<=?), type (+), type (*), type (^), type (-)
31
32 ) where
33
34 import GHC.Base(Eq(..), Ord(..), Bool(True), otherwise)
35 import GHC.Num(Integer)
36 import GHC.Base(String)
37 import GHC.Show(Show(..))
38 import GHC.Read(Read(..))
39 import GHC.Prim(magicSingI)
40 import Data.Maybe(Maybe(..))
41 import Data.Proxy(Proxy(..))
42
43 -- | (Kind) This is the kind of type-level natural numbers.
44 data Nat
45
46 -- | (Kind) This is the kind of type-level symbols.
47 data Symbol
48
49
50 --------------------------------------------------------------------------------
51
52 -- | This class gives the integer associated with a type-level natural.
53 -- There are instances of the class for every concrete literal: 0, 1, 2, etc.
54 class KnownNat (n :: Nat) where
55 natVal :: proxy n -> Integer
56
57 -- | This class gives the integer associated with a type-level symbol.
58 -- There are instances of the class for every concrete literal: "hello", etc.
59 class KnownSymbol (n :: Symbol) where
60 symbolVal :: proxy n -> String
61
62 -- | This type represents unknown type-level natural numbers.
63 data SomeNat = forall n. KnownNat n => SomeNat (Proxy n)
64
65 -- | This type represents unknown type-level symbols.
66 data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n)
67
68 instance SingI n => KnownNat n where
69 natVal _ = case sing :: Sing n of
70 SNat x -> x
71
72 instance SingI n => KnownSymbol n where
73 symbolVal _ = case sing :: Sing n of
74 SSym x -> x
75
76 -- | Convert an integer into an unknown type-level natural.
77 someNatVal :: Integer -> Maybe SomeNat
78 someNatVal n
79 | n >= 0 = Just (forgetSingNat (SNat n))
80 | otherwise = Nothing
81
82 -- | Convert a string into an unknown type-level symbol.
83 someSymVal :: String -> SomeSymbol
84 someSymVal n = forgetSingSymbol (SSym n)
85
86 instance Eq SomeNat where
87 SomeNat x == SomeNat y = natVal x == natVal y
88
89 instance Ord SomeNat where
90 compare (SomeNat x) (SomeNat y) = compare (natVal x) (natVal y)
91
92 instance Show SomeNat where
93 showsPrec p (SomeNat x) = showsPrec p (natVal x)
94
95 instance Read SomeNat where
96 readsPrec p xs = do (a,ys) <- readsPrec p xs
97 case someNatVal a of
98 Nothing -> []
99 Just n -> [(n,ys)]
100
101
102 instance Eq SomeSymbol where
103 SomeSymbol x == SomeSymbol y = symbolVal x == symbolVal y
104
105 instance Ord SomeSymbol where
106 compare (SomeSymbol x) (SomeSymbol y) = compare (symbolVal x) (symbolVal y)
107
108 instance Show SomeSymbol where
109 showsPrec p (SomeSymbol x) = showsPrec p (symbolVal x)
110
111 instance Read SomeSymbol where
112 readsPrec p xs = [ (someSymVal a, ys) | (a,ys) <- readsPrec p xs ]
113
114
115 --------------------------------------------------------------------------------
116
117 -- | Comparison of type-level naturals, as a constraint.
118 type x <= y = (x <=? y) ~ True
119
120 -- | Comparison of type-level naturals, as a function.
121 type family (m :: Nat) <=? (n :: Nat) :: Bool
122
123 -- | Addition of type-level naturals.
124 type family (m :: Nat) + (n :: Nat) :: Nat
125
126 -- | Multiplication of type-level naturals.
127 type family (m :: Nat) * (n :: Nat) :: Nat
128
129 -- | Exponentiation of type-level naturals.
130 type family (m :: Nat) ^ (n :: Nat) :: Nat
131
132 -- | Subtraction of type-level naturals.
133 --
134 -- /Since: 4.7.0.0/
135 type family (m :: Nat) - (n :: Nat) :: Nat
136
137
138
139 --------------------------------------------------------------------------------
140 -- PRIVATE:
141
142 -- | This is an internal GHC class. It has built-in instances in the compiler.
143 class SingI a where
144 sing :: Sing a
145
146 -- | This is used only in the type of the internal `SingI` class.
147 data family Sing (n :: k)
148 newtype instance Sing (n :: Nat) = SNat Integer
149 newtype instance Sing (n :: Symbol) = SSym String
150
151
152 {- PRIVATE:
153 The functions below convert a value of type `Sing n` into a dictionary
154 for `SingI` for `Nat` and `Symbol`.
155
156 NOTE: The implementation is a bit of a hack at present,
157 hence all the very special annotations. See Note [magicSingIId magic]
158 for more details.
159 -}
160 forgetSingNat :: forall n. Sing (n :: Nat) -> SomeNat
161 forgetSingNat x = withSingI x it Proxy
162 where
163 it :: SingI n => Proxy n -> SomeNat
164 it = SomeNat
165
166 forgetSingSymbol :: forall n. Sing (n :: Symbol) -> SomeSymbol
167 forgetSingSymbol x = withSingI x it Proxy
168 where
169 it :: SingI n => Proxy n -> SomeSymbol
170 it = SomeSymbol
171
172 -- | THIS IS NOT SUPPOSED TO MAKE SENSE.
173 -- See Note [magicSingIId magic]
174 {-# NOINLINE withSingI #-}
175 withSingI :: Sing n -> (SingI n => a) -> a
176 withSingI x = magicSingI x ((\f -> f) :: () -> ())
177
178
179