TypeLits.hs 7.79 KB
Newer Older
1
{-# LANGUAGE Trustworthy #-}
2 3 4 5
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
6
{-# LANGUAGE FlexibleInstances #-}
7
{-# LANGUAGE FlexibleContexts #-}
8 9 10 11
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
12
{-# LANGUAGE UndecidableInstances #-}  -- for compiling instances of (==)
13
{-# LANGUAGE NoImplicitPrelude #-}
14
{-# LANGUAGE MagicHash #-}
15
{-# LANGUAGE PolyKinds #-}
16

17 18
{-| This module is an internal GHC module.  It declares the constants used
in the implementation of type-level natural numbers.  The programmer interface
19 20
for working with type-level naturals should be defined in a separate library.

21
@since 4.6.0.0
22
-}
23

24 25
module GHC.TypeLits
  ( -- * Kinds
26
    Nat, Symbol  -- Both declared in GHC.Types in package ghc-prim
27

28
    -- * Linking type and value level
29 30
  , KnownNat, natVal, natVal'
  , KnownSymbol, symbolVal, symbolVal'
31
  , SomeNat(..), SomeSymbol(..)
32
  , someNatVal, someSymbolVal
33 34
  , sameNat, sameSymbol

35

36
    -- * Functions on type literals
37
  , type (<=), type (<=?), type (+), type (*), type (^), type (-)
38
  , CmpNat, CmpSymbol
39

40 41 42 43
  -- * User-defined type errors
  , TypeError
  , ErrorMessage(..)

Iavor S. Diatchki's avatar
Iavor S. Diatchki committed
44 45
  ) where

46
import GHC.Base(Eq(..), Ord(..), Bool(True,False), Ordering(..), otherwise)
47
import GHC.Types( Nat, Symbol )
48
import GHC.Num(Integer)
49
import GHC.Base(String)
50
import GHC.Show(Show(..))
51
import GHC.Read(Read(..))
52
import GHC.Prim(magicDict, Proxy#)
53
import Data.Maybe(Maybe(..))
54
import Data.Proxy (Proxy(..))
55
import Data.Type.Equality(type (==), (:~:)(Refl))
56
import Unsafe.Coerce(unsafeCoerce)
57

58
--------------------------------------------------------------------------------
Iavor S. Diatchki's avatar
Iavor S. Diatchki committed
59

60 61
-- | This class gives the integer associated with a type-level natural.
-- There are instances of the class for every concrete literal: 0, 1, 2, etc.
62
--
63
-- @since 4.7.0.0
64
class KnownNat (n :: Nat) where
65
  natSing :: SNat n
66

jpm@cs.ox.ac.uk's avatar
Typo  
jpm@cs.ox.ac.uk committed
67
-- | This class gives the string associated with a type-level symbol.
68
-- There are instances of the class for every concrete literal: "hello", etc.
69
--
70
-- @since 4.7.0.0
71
class KnownSymbol (n :: Symbol) where
72 73
  symbolSing :: SSymbol n

74
-- | @since 4.7.0.0
75 76 77 78
natVal :: forall n proxy. KnownNat n => proxy n -> Integer
natVal _ = case natSing :: SNat n of
             SNat x -> x

79
-- | @since 4.7.0.0
80 81 82 83
symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
symbolVal _ = case symbolSing :: SSymbol n of
                SSymbol x -> x

84
-- | @since 4.8.0.0
85 86 87 88
natVal' :: forall n. KnownNat n => Proxy# n -> Integer
natVal' _ = case natSing :: SNat n of
             SNat x -> x

89
-- | @since 4.8.0.0
90 91 92 93
symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String
symbolVal' _ = case symbolSing :: SSymbol n of
                SSymbol x -> x

94

95

96 97
-- | This type represents unknown type-level natural numbers.
data SomeNat    = forall n. KnownNat n    => SomeNat    (Proxy n)
98
                  -- ^ @since 4.7.0.0
99

100 101
-- | This type represents unknown type-level symbols.
data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n)
102
                  -- ^ @since 4.7.0.0
Iavor S. Diatchki's avatar
Iavor S. Diatchki committed
103

104
-- | Convert an integer into an unknown type-level natural.
105
--
106
-- @since 4.7.0.0
107 108
someNatVal :: Integer -> Maybe SomeNat
someNatVal n
109
  | n >= 0        = Just (withSNat SomeNat (SNat n) Proxy)
110 111 112
  | otherwise     = Nothing

-- | Convert a string into an unknown type-level symbol.
113
--
114
-- @since 4.7.0.0
115
someSymbolVal :: String -> SomeSymbol
116 117 118
someSymbolVal n   = withSSymbol SomeSymbol (SSymbol n) Proxy


119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140

instance Eq SomeNat where
  SomeNat x == SomeNat y = natVal x == natVal y

instance Ord SomeNat where
  compare (SomeNat x) (SomeNat y) = compare (natVal x) (natVal y)

instance Show SomeNat where
  showsPrec p (SomeNat x) = showsPrec p (natVal x)

instance Read SomeNat where
  readsPrec p xs = do (a,ys) <- readsPrec p xs
                      case someNatVal a of
                        Nothing -> []
                        Just n  -> [(n,ys)]


instance Eq SomeSymbol where
  SomeSymbol x == SomeSymbol y = symbolVal x == symbolVal y

instance Ord SomeSymbol where
  compare (SomeSymbol x) (SomeSymbol y) = compare (symbolVal x) (symbolVal y)
141

142 143
instance Show SomeSymbol where
  showsPrec p (SomeSymbol x) = showsPrec p (symbolVal x)
144

145
instance Read SomeSymbol where
146
  readsPrec p xs = [ (someSymbolVal a, ys) | (a,ys) <- readsPrec p xs ]
147

148
type family EqNat (a :: Nat) (b :: Nat) where
149 150
  EqNat a a = 'True
  EqNat a b = 'False
151 152 153
type instance a == b = EqNat a b

type family EqSymbol (a :: Symbol) (b :: Symbol) where
154 155
  EqSymbol a a = 'True
  EqSymbol a b = 'False
156
type instance a == b = EqSymbol a b
157

158
--------------------------------------------------------------------------------
159

160 161 162 163 164
infix  4 <=?, <=
infixl 6 +, -
infixl 7 *
infixr 8 ^

165
-- | Comparison of type-level naturals, as a constraint.
166
type x <= y = (x <=? y) ~ 'True
167

Iavor S. Diatchki's avatar
Iavor S. Diatchki committed
168
-- | Comparison of type-level symbols, as a function.
169
--
170
-- @since 4.7.0.0
171 172
type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering

Iavor S. Diatchki's avatar
Iavor S. Diatchki committed
173
-- | Comparison of type-level naturals, as a function.
174
--
175
-- @since 4.7.0.0
176 177
type family CmpNat    (m :: Nat)    (n :: Nat)    :: Ordering

Iavor S. Diatchki's avatar
Iavor S. Diatchki committed
178 179 180 181
{- | Comparison of type-level naturals, as a function.
NOTE: The functionality for this function should be subsumed
by 'CmpNat', so this might go away in the future.
Please let us know, if you encounter discrepancies between the two. -}
182 183
type family (m :: Nat) <=? (n :: Nat) :: Bool

184 185 186 187 188 189 190 191 192
-- | Addition of type-level naturals.
type family (m :: Nat) + (n :: Nat) :: Nat

-- | Multiplication of type-level naturals.
type family (m :: Nat) * (n :: Nat) :: Nat

-- | Exponentiation of type-level naturals.
type family (m :: Nat) ^ (n :: Nat) :: Nat

193
-- | Subtraction of type-level naturals.
194
--
195
-- @since 4.7.0.0
196
type family (m :: Nat) - (n :: Nat) :: Nat
197

198

199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220
-- | A description of a custom type error.
data {-kind-} ErrorMessage = Text Symbol
                             -- ^ Show the text as is.

                           | forall t. ShowType t
                             -- ^ Pretty print the type.
                             -- @ShowType :: k -> ErrorMessage@

                           | ErrorMessage :<>: ErrorMessage
                             -- ^ Put two pieces of error message next
                             -- to each other.

                           | ErrorMessage :$$: ErrorMessage
                             -- ^ Stack two pieces of error message on top
                             -- of each other.

infixl 5 :$$:
infixl 6 :<>:

type family TypeError (a :: ErrorMessage) :: b where


221 222 223 224
--------------------------------------------------------------------------------

-- | We either get evidence that this function was instantiated with the
-- same type-level numbers, or 'Nothing'.
225
--
226
-- @since 4.7.0.0
227 228 229 230 231 232 233 234
sameNat :: (KnownNat a, KnownNat b) =>
           Proxy a -> Proxy b -> Maybe (a :~: b)
sameNat x y
  | natVal x == natVal y = Just (unsafeCoerce Refl)
  | otherwise            = Nothing

-- | We either get evidence that this function was instantiated with the
-- same type-level symbols, or 'Nothing'.
235
--
236
-- @since 4.7.0.0
237 238 239 240 241
sameSymbol :: (KnownSymbol a, KnownSymbol b) =>
              Proxy a -> Proxy b -> Maybe (a :~: b)
sameSymbol x y
  | symbolVal x == symbolVal y  = Just (unsafeCoerce Refl)
  | otherwise                   = Nothing
242

243 244
--------------------------------------------------------------------------------
-- PRIVATE:
245

246 247
newtype SNat    (n :: Nat)    = SNat    Integer
newtype SSymbol (s :: Symbol) = SSymbol String
248

249 250
data WrapN a b = WrapN (KnownNat    a => Proxy a -> b)
data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)
251

252 253 254 255
-- See Note [magicDictId magic] in "basicType/MkId.hs"
withSNat :: (KnownNat a => Proxy a -> b)
         -> SNat a      -> Proxy a -> b
withSNat f x y = magicDict (WrapN f) x y
256

257 258 259 260
-- See Note [magicDictId magic] in "basicType/MkId.hs"
withSSymbol :: (KnownSymbol a => Proxy a -> b)
            -> SSymbol a      -> Proxy a -> b
withSSymbol f x y = magicDict (WrapS f) x y
261

262