Сегодня мы поговорим о таких штуках, как kind’ы типов (иногда в русскоязычной литературе их называют “типажами”, но мне не особо нравится такой перевод).

Начнём с самых азов. В любом языке (надеюсь на это) программирования есть понятие значений, например (все примеры кода в этом посте - Haskell):

1           -- число
[1, 2, 3]   -- список
(1, "abc")  -- кортеж

В расово верных типизированных языках у этих значений есть типы:

1           :: Int
[1, 2, 3]   :: [Int]
(1, "abc")  :: (Int, String)

Можно переписать эти типы иначе, не пользуясь синтаксическим сахаром для имён типов в Haskell:

1           :: Int              -- в C-подобных языках:
[1, 2, 3]   :: List Int         -- List<Int>
(1, "abc")  :: Pair Int String  -- Pair<Int, String>

Тут мы замечаем, что типы бывают совсем примитивными и сложными, синтезированными из применений параметризованных типов к различным другим типам. Такие параметризованные типы обычно встречаются в языках с поддержкой параметрического полиморфизма. Параметров-типов может быть несколько (например, в кортежах или словарях - Map key value). Такие полиморфные типы данных позволяют писать обобщённый код работы с экземплярами таких типов данных, не имеющий знания о реальных типах подставляемых в качестве типов-параметров - например, функция map работает поверх списков с элементами любого типа.

После того, как к параметризованный тип примененён к типам-параметрам, параметризованный тип становится полноправным типом - точно таким же, как и примитивные (не параметризованные типы), и может выступать как тип-параметр других параметризованных типов.

Возникает вопрос: что есть List, что есть Pair и другие параметризованные типы, до применения к типам-параметрам? Эти штуки называются конструкторами типов (type constructors), так как они очень похожи на конструкторам данных (декларации data). Именно поэтому я употреблял выше слово “применить”, так как применение конструктора типов к типу-параметру (List Int) выглядит аналогично применению к конструктору данных параметра-значения (Just 1). То есть List, например, можно трактовать как функцию, причём функцию над типами, которая получает некоторый тип (тип-параметр) и возвращает некоторый тип (параметризованный тип с подставленным типом-параметром).

Если параметрический тип имет более одного типа-параметра, то конструктор такого типа можно трактовать как функцию над типами с каррированными аргументами. Например, конструктор типа Map при применении к одному типу-аргументу (тип ключа Map‘а) на самом деле порождает в Haskell другой конструктор типа (!), применив который к другому типу-параметру (тип значений Map‘а), мы получим нормальный тип. Именно поэтому в Haskell запись Map Int String аналогична ((Map Int) String). Более того, так же как и на уровне функций и значений, на уровне типов тоже можно исполльзовать частичное применение! Однако во многих других языках (типа C#, например), конструктор типа применяется сразу к нескольким типам-параметрам одновременно. Тогда такие конструкторы типов можно трактовать как функции, принимающие кортеж из типов-параметров.

Подведём небольшой итог: существуют несколько разновидностей типов - простые типы и функции над типами. Эти разновидности играют роль типов типов! Далее такой тип типа будет называться kind’ом. Введём обозначения для kind’ов - простые типы будем обозначать звёздочкой *, а функции над типами - привычной функциональной стрелочкой →. Теперь мы можем типизировать типы!

Int           :: *
List Int      :: *
(Int, String) :: *
List          :: * → *
Map           :: * → * → *

Обратите внимание на то, что → здесь обладает правой ассоциативностью, поэтому последний kind можно записать вот так: * → (* → *). То есть на самом деле всё просто, kind’ы - есть типы над элементами системы типов.

Большинство времени, даже в Haskell, программисты имеют дело только с простыми типами, имеющими kind *. Однако уже очень давно в Haskell могут существовать типы-параметры (да, типы-параметры тоже имеют kind, так как сами, конечно же, являются типами), имеющие нетривиальные kind’ы, например:

fmap :: Functor f => (a → b) → f a → f b

В этой сигнатуре к типу-параметру f применяются другие типы-параметры a и b, что заставляет компилятор Haskell для типа-параметра f вывести kind * → *. То есть вызывая fmap в качестве типа-параметра должен будет выступать некоторый параметризованный тип с одним типом-параметром (+ для которого определен экземпляр класса типов Functor). Таким образом функция fmap умеет отображать любой контейнер типа f в другой контейнер типа f, потенциально изменяя тип, которым параметризован монадический тип (например, отобразить [Int] в [String] или Maybe Int в Maybe String).

Языки, допускающие существование типов с kind’ом, отличным от *, называют языками с поддержкой higher-kinded types. Существует ещё одно понятие - higher-kinded polymorphism (его ещё называют полиморфизмом конструктора типов - type constructor polymorphism), подразумевающее под собой параметрически полиморфизм, при котором типы-параметры могут иметь kind, отличный от * (как тип-параметр m из примера выше). Помимо Haskell, известным языком с поддержкой полиморфизма конструктора типов является Scala (что совсем не удивительно).

В большинстве мэйнстримных языков типа C#/Java так или иначе существует возможность использовать/определять типы с kind’ами, отличными от *. Например, такие типы в .NET даже имеют представление во время выполнения - typeof(Dictionary<,>). Однако, они не являются первоклассными сущностями в системе типов - нельзя передать такие типы в качестве типов-параметров, не указывая им собственных типов-параметров. А значит нет и поддержки higher-kinded polymorphism - абсолютно все типы-параметры всегда обладают kind’ом *, нельзя применить тип к типу-параметру как-то так: T<int>.

Существуют множество других нетривиальных случаев типов, обладающих необычными kind’ами, например в этом определении типа данных:

data Foo m a = Foo (m a)

Тип-параметр m будет иметь kind * → * (так как к нему применяется тип-параметр a), а вот уже сам тип Foo будет иметь kind (* → *) → *→ *. То есть после применения конструктора типа Foo к другому конструктору типа с kind’ом * → * и последующему применению к ещё одному обычному типу, мы получим обычный тип с kind’ом *, такой как, например, Foo List Int (важно понимать приоритет применений конструкторов типов к типам-параметрам - (Foo List) Int).

Интересно, что Haskell по-умолчанию не даёт возможности указывать kind’ы типов явно (так же как указывать значениям типы), а выводит kind из использования. Из-за этого людям иногда приходится изгаляться, например, добавляя фиктивные конструкторы типа:

data Set cxt a = Set [a]
               | Unused (cxt a → ())

В декларации выше конструктор Unused используется лишь для того, чтобы задать типу-параметру kind * → *, что выглядит чрезвычайно ущербно. Однако в GHC существует языковое расширение explicitly-kinded quantification, включаемое флагом -XKindSignatures, которое добавляет поддержку явных аннотаций kind’ов, что может быть очень и очень удобно:

-- в декларациях типов данных
data Set (cxt :: * → *) a = Set [a]

-- в определениях синонимов типов
type T (f :: * → *) = f Int

-- в определениях классов типов
class (Eq a) => C (f :: * → *) a where ...

Мне лень и не хватает знаний Haskell и теории типов чтобы достойно осветить тему kind’ов глубже, поэтому я просто оставлю здесь несколько интересных ссылочек:

  • Расширение constraint kinds для GHC - добавляет новую разновидность kind’ов - Contstraint, что позволяет параметризовать ограничения на типы-параметры полиморфных типов и функций (параметризовать constraints).
  • В системах kind’ов может встречаться и такие типы kind’ов, как распакованные типы (обычно обозначаются символом #). Более того, между kind’ами может существовать отношение, аналогичное вложению/включению типов - subkinding.
  • KindSystem и PolymorphicKinds для GHC - предлагаемые расширения языка, позволяющие добавить аналог параметрического полиморфизма на уровень kind’ов (!) и определять собственные kind’ы (!!). Самый известный пример всего этого безобразия - списки, параметризованные собственной длинной:
data kind Nat = Zero | Succ Nat

data List :: * -> Nat -> * where
  Nil  :: List a Zero
  Cons :: a -> List a n -> List a (Succ n)

Тип List невозможно сконструировать, не используя для второго типа-параметра тип, не соответствующий kind’у Nat. который включает в себя тип Zero и тип Suсс, параметризованный типом, обладающим kind’ом Nat. Всё это очень похоже на работу со значениями, только ровно одним уровнем выше. Без определения kind’а Nat можно было бы создать не имеющий особого смысла тип List Int Int.