GHC поддерживает числовые, строковые и символьные литералы на уровне типов, обеспечивая удобный доступ к большому числу предопределённых констант уровня типов. Числовые литералы имеют вид Natural, строковые литералы — вид Symbol, а символьные литералы — вид Char. Эта возможность включается языковым расширением DataKinds.
Виды литералов и все остальные низкоуровневые операции для этой возможности определены в модулях GHC.TypeLits и GHC.TypeNats. Обратите внимание, что в этих модулях определены некоторые операторы уровня типов, конфликтующие со своими аналогами уровня значений (например, (+)). В объявлениях импорта и экспорта, ссылающихся на эти операторы, требуется явная аннотация пространства имён (см. Явные пространства имён в импорте/экспорте).
Пример использования числовых литералов уровня типов для создания безопасного интерфейса к низкоуровневой функции:
import GHC.TypeLits import Data.Word import Foreign newtype ArrPtr (n :: Natural) a = ArrPtr (Ptr a) clearPage :: ArrPtr 4096 Word8 -> IO () clearPage (ArrPtr p) = ...
Кроме того, натуральные числа уровня типов можно продвигать из типа данных Natural с помощью DataKinds, например:
data Point = MkPoint Natural Natural type MyCoordinates = MkPoint 95 101
Пример использования строковых литералов уровня типов для имитации простых операций с записями:
data Label (l :: Symbol) = Get class Has a l b | a l -> b where from :: a -> Label l -> b data Point = Point Int Int deriving Show instance Has Point "x" Int where from (Point x _) _ = x instance Has Point "y" Int where from (Point _ y) _ = y example = from (Point 1 2) (Get :: Label "x")
6.4.16.1. Значения времени выполнения для литералов уровня типов
Иногда полезно получить значение уровня значений, связанное с литералом уровня типов. Для этого используются функции natVal и symbolVal. Например:
GHC.TypeLits> natVal (Proxy :: Proxy 2) 2
Эти функции перегружены, поскольку должны возвращать разные результаты в зависимости от типа, для которого они инстанцированы.
natVal :: KnownNat n => proxy n -> Natural -- from GHC.TypeNats natVal :: KnownNat n => proxy n -> Integer -- from GHC.TypeLits -- instance KnownNat 0 -- instance KnownNat 1 -- instance KnownNat 2 -- ...
GHC снимает ограничение, как только узнаёт, какой конкретный литерал уровня типов используется в программе. Обратите внимание, что это работает только для литералов, а не для произвольных выражений типов. Например, ограничение вида KnownNat (a + b) не будет упрощено до (KnownNat a, KnownNat b); вместо этого GHC сохранит ограничение без изменений, пока не сможет упростить a + b до константного значения.
Также можно преобразовать целочисленное или строковое значение времени выполнения в соответствующий литерал уровня типов. Разумеется, полученный литерал типа будет неизвестен во время компиляции, поэтому он скрывается в экзистенциальном типе. Для целых чисел преобразование можно выполнить с помощью someNatVal, а для строк — с помощью someSymbolVal:
someNatVal :: Natural -> Maybe SomeNat -- from GHC.TypeNats someNatVal :: Integer -> Maybe SomeNat -- from GHC.TypeLits SomeNat :: KnownNat n => Proxy n -> SomeNat
Операции над строками аналогичны.
6.4.16.2. Вычисления с натуральными числами уровня типов
GHC 7.8 умеет вычислять арифметические выражения с натуральными числами уровня типов. Такие выражения можно строить с помощью семейств типов (+), (*), (^) для сложения, умножения и возведения в степень. Числа можно сравнивать с помощью (<=?), возвращающего продвинутое булево значение, или (<=), выполняющего сравнение чисел как ограничение. Например:
GHC.TypeLits> natVal (Proxy :: Proxy (2 + 3)) 5
В настоящее время возможности GHC рассуждать об арифметике довольно ограничены: он только вычисляет арифметические функции типов и сравнивает результаты — так же, как и для любой другой функции типов. В частности, ему неизвестны более общие свойства арифметики, например коммутативность и ассоциативность (+).
Однако можно выполнять некоторые вычисления «в обратном направлении». Например, вот как можно заставить GHC вычислять произвольные логарифмы на уровне типов:
lg :: Proxy base -> Proxy (base ^ pow) -> Proxy pow lg _ _ = Proxy GHC.TypeLits> natVal (lg (Proxy :: Proxy 2) (Proxy :: Proxy 8)) 3
