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.15.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.15.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
