Что это за штука под названием «тип»? Часть 2

  • Article

Как я и упоминал в прошлый раз, вполне предсказуемо, если вы попросите десять разработчиков дать определения «типа», то они дадут десять разных ответов. Комментарии к предыдущей статье были замечательными[1]!

Ниже представлена моя попытка описать понятия «типа» с точки зрения разработчика компилятора. Для начала я хочу рассмотреть вопрос о том, что такое тип, и не сбивать вас с толку тем, как он используется.

По сути, в языке C # тип – это математическая категория, которая следует определенным алгебраическим правилам. Так, например, натуральные или комплексные числа, кватернионы, матрицы, наборы, последовательности и т.д. являются математическими категориями, которые подчиняются определенным алгебраическим правилам.

Продолжая эту аналогию, я хочу немного отвлечься и спросить: «что такое натуральное число? » Т.е. что фундаментальным образом характеризует числа 0, 1, 2, 3, ... которые мы используем для описания позиции элемента в последовательности или размера коллекции?

Этот вопрос терзал разные умы веками; окончательный ответ, который мы используем до сих пор, дал Джузеппе Пеано в 19-м веке. Пеано дал следующее определение:

  • Нуль является натуральным числом.
  • У каждого натурального числа есть «последующее натуральное число».
  • Нуль не является последующим натуральным числом ни для одного из натуральных чисел.
  • У разных натуральных чисел разные последующие натуральные числа
  • Если начать с нуля и затем перебирать последующие элементы до бесконечности, то мы получим все натуральные числа (*).

Удивительно, но это все, что нам нужно. Любая математическая категория, отвечающая этим условиям может рассматриваться как последовательность натуральных чисел (**). Обратите внимание, что в этом определении ничего не говорится о сложении, вычитании, умножении, делении или возведении в степень натуральных чисел. Все это может быть добавлено при необходимости. Например, мы можем определить сложение следующим образом:

  • (n + 0) = n
  • (n + (successor of m)) = ((successor of n) + m)

где successor of m – это натуральное число, следующее за m.

Вот и все; мы получили рекурсивное определение сложения. Мы также просто можем дать определение «оператора меньше»:

  • (n < 0) = false
  • (0 < (successor of m)) = true
  • ((successor of n) < (successor of m)) = (n < m)

Подобным образом мы можем определить любую операцию для натуральных чисел; попробуйте, ради интереса, дать определение умножения. (Подсказка: следует отталкиваться от предположения, что оператор сложения уже определен).

Аналогичным образом мы можем дать определение «типа»:

  • Object является типом
  • «Объявленные» типы («declared» types) являются типами (такие типы, как int, uint, bool, string и т.п. можно рассматривать «объявленными» типами; они определены за нас компилятором).
  • Если T – это тип и n – это положительное целое, тогда «n-мерный массив типов T» тоже является типом.

И по большому счету, это все, что нужно для определения «безопасной» части языка C# 1.0. (Чтобы добиться той же строгости, что и аксиомы Пеано для натуральных чисел, нам нужно добавить аналогичные защитные условия; например, мы не хотим, чтобы «одномерный массив типов double» был такого же типа, что и тип int, аналогично тому, как мы не хотим, чтобы последующим натуральным числом для какого-либо числа был нуль.)

Все становится несколько сложнее при появлении обобщенных типов и указателей, но я уверен, вы понимаете, что мы можем относительно просто получить точное определение и для них. Т.е. типы параметров являются типами, обобщенные типы с правильным количеством аргументом типов являются типами и т.п.

Затем мы можем добавить алгебраические операции. Аналогично тому, как мы определили для чисел операцию «меньше» мы можем определить отношение «является подтипом».

  • T <: object возвращает true для любого типа T
  • object <: T возвращает false для любого типа T
  • Если S <: T и T <: U, тогда S <: U
  • … и т.д. …

Аналогично тому, как можно не обращать внимания на «реализацию» чисел для использования их в алгебраических операциях, можно не обращать внимания на «реализацию» типов для использования их с правилами алгебры типов. Мне нужно знать лишь аксиомы системы типов и правила, определяющие алгебраические операторы, которые я выдумал ради собственного удобства.

Итак, у нас есть определение «типа», которое ничего не говорит ни о «наборе значений», ни о «имени». Тип – это всего лишь абстрактная математическая категория, аналогичная числам, которая следует некоторым аксиомам и, таким образом, над ней можно выполнять алгебраические преобразования путем создания правил для необходимых операторов. Аналогично тому, как мы можем абстрактно манипулировать числами в соответствии с придуманными алгебраическими правилами.

Итак, мы получили набросок определения типа, и что же мы собираемся с ним делать?

Вероятно, наиболее важной целью статической проверки типов в языках программирования, таких как C#, является связывание типа с каждой возможной переменной(storage location), связывание типа с каждым (†) возможным выражением времени компиляции, и последующая гарантия того, что значение, связанное с несоответствующим типом не будет записано или прочитано ни из какой переменной. Доказательство во время компиляции безопасности типов во время выполнения ( ‡ ): вот какая стоит цель.

Ключевым словом в этом определении является «доказательство»; теперь, когда мы получили определение «типа» мы можем начать создавать доказательства на основе этого определения. Спецификация языка C# определяет:

  • тип, связанный с каждым выражением времени компиляции; конечно, выражения, чей тип невозможно определить, являются ошибками
  • тип, связанный с каждой переменной
  • перечень доступных операций присваивания выражения некоторого типа ( ‡‡ ) некоторой переменной

Разработчик компилятора должен выполнить три эти задачи спецификации: связать тип с каждым выражением, связать тип со всеми переменными, и, затем, получить доказательства того, что все присваивания соответствуют определенным правилам. Если компилятор может доказать это, значит присваивание допустимо. Но сложность заключается в следующем: обычно спецификация дает лишь правила системы типов, а не подробный алгоритм, описывающий получение доказательства на основании этих правил. Если существует некоторое правило, то компилятор требует, чтобы ему следовали. И наоборот, если правила не существует, компилятор должен это понять и выдать подходящую ошибку во время компиляции.

Но, к сожалению, как выясняется, в общем случае это невозможно. Система, в которой для каждого выражения можно точно сказать, является ли оно «типобезопасным» или нет, за конечное количество логических шагов называется «разрешимой» (decidable). Как гласит знаменитое доказательство Гёделя, арифметика натуральных чисел, в том виде, в котором она определена выше, является неразрешимой (undecidable); в формальной арифметике существуют высказывания, которые не могут быть ни доказаны, ни опровергнуты за конечное число логических шагов. Проверка возможности присваивания также является неразрешимой в языках, поддерживающих именное наследование (nominal subtyping) ( ‡‡‡ ) или вариантность обобщений (generic variance). Как я уже говорил, можно добавить дополнительные ограничения при объявлении типа, чтобы именное наследование стало разрешимым, но в языке C# такой возможности пока нет. Вместо этого, если компилятор сталкивается с ситуацией, когда доказательство корректности становится бесконечно долгим, он просто падает с ошибкой «выражение слишком сложное для анализа». Я надеюсь исправить это в одной из будущих версий компилятора, но это низкоприоритетная задача, поскольку такие ситуации слишком редкие.

К счастью, ситуации, когда анализ типов невозможен или чрезвычайно ресурсоемок, встречаются редко в реальных приложениях на языке C#; они встречаются достаточно редко, чтобы мы относились к ним разумно и создавали быстрый компилятор.

Заключение: Тип является абстрактной математической категорией, определенной несколькими простыми аксиомами. Для языка C# существуют правила ассоциации типов с выражениями времени компиляции и переменными, а также правила, гарантирующие согласованность типов выражений и переменных. Задачей разработчика компилятора является использование этих идиом и алгебраических правил для доказательства или опровержения того, что тип каждого выражения является корректным и что каждое присваивание следует правилам совместимости присваивания.

И хотя аксиомы, определяющие тип являются простыми, но правила, связывающие типы и выражения, а также определение совместимости присваивания являются чрезвычайно сложными; вот почему слово «тип» в спецификации встречается 5000 раз. По большому счету, язык C# определен на основе этих правил.

------------------------------

(*) Конечно, это очень упрощенное определение; более формально, в настоящей аксиоме говорится о том, что для натуральных чисел применимо доказательство по индукции. Т.е. если некоторое свойство истинно для нуля и если из истинности свойства для некоторого числа следует истинность для последующего числа, то из этого следует, что это свойство выполняется для всех чисел.

(**) Важно понять, почему третий, четвертый и пятый пункты являются необходимыми. Без третьего пункта нам было бы достаточно иметь лишь одно число: нуль, который бы являлся последующим числом для самого себя! Без четвертого пункта мы бы могли сказать, что нам достаточно лишь два числа: единица, как число, следующее за нулем и единица, как последующее число за единицей. Без пятого пункта у нас могло бы быть *два* нуля: «красный» нуль и «синий нуль». И числом, следующим за красным нулем была бы красная единица, а последующим числом для синего нуля – синяя единица. В каждом случае, система без одного из этих правил, удовлетворяла бы остальным четырем, но при этом противоречила бы нашему интуитивному понятию «натурального числа».

(†) Конечно, в языке C# это не так; null-литералы, анонимные функции, а также группы методов (method groups) говоря формально являются «выражениями без типа». Однако в корректной программе они должны встречаться только там, где тип выражения может быть выведен из окружающего контекста.

( ‡ ) Конечно же, операторы преобразования типов этому не соответствуют; оператор преобразования типа может означать следующее: «безопасность типов времени компиляции не может быть доказана; я утверждаю, что это выражение типобезопасно, поэтому сгенерируй код, проверяющий мое утверждение во время выполнения». Кроме того, небезопасная ковариантность массивов делает эту цель недостижимой.

( ‡‡ ) Это опять-таки, не всегда выполняется. Например, переменной типа short нельзя присвоить выражение типа int, если выражение типа intне является константой времени компиляции, размер которого гарантированно не превосходит размер типа short.

( ‡‡‡ ) Т.е. язык, в котором базовый тип указывается при объявлении нового типа. Например, при объявлении «interface IFoo<T> : IBar<T>» используется именное наследование.

Оригинал статьи

[1] Речь идет об оригинальной версии статьи, опубликованной по адресу: https://blogs.msdn.com/b/ericlippert/archive/2011/08/29/what-is-this-thing-you-call-a-quot-type-quot-part-one.aspx