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

(Эрик сейчас не в офисе, и этот пост записан предварительно. Я буду на работе после Дня труда.)

Слово тип (type) в спецификации C# 4 встречается почти пять тысяч раз, и там есть целая глава (глава 4), посвященная исключительно описанию типов. В начале спецификации сказано, что язык C# является «типобезопасным» (type safe) и имеет «унифицированную систему типов» (*). В ней сказано, что в программах «определяются» (declare) типы, и эти типы могут быть организованы в пространства имен. Очевидно, что типы являются невероятно важной частью с точки зрения дизайна языка C# и очень важны для программистов, так что более чем странно, что на восьмистах страницах спецификации на самом деле нет определения слова «тип».

Мы предполагаем, что разработчик, читающий спецификацию, уже понимает, что такое «тип»; спецификация не ставит перед собой цели быть учебником для новичков в программировании или математически точным формальным описанием языка. Но если вы спросите у десяти профессиональных разработчиков формальное определение термина «тип», то вы получите десять разных ответов. Так давайте сегодня рассмотрим следующий вопрос: что же это за штука такая, под названием «тип»?

В распространенном ответе на этот вопрос говорится, что тип содержит:

* Имя

* Набор (возможно бесконечный) значений

И, возможно содержит:

* конечный список правил, связывающий значения, не принадлежащие этому типу со значениями этого типа (т.е. приведения типов; 123.45 не является членом типа integer, но может быть приведено к значению 123).

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

Первая проблема связана с тем, что, конечно же, не каждому типу нужно имя; анонимные типы, появившиеся в C# 3, по определению не имеют имени. Является ли “string[][]” именем типа? А как насчет “List<string[][]>”? А какое имя у типа string? “string”, “String”, “System.String”, “global::System.String” или все четыре варианта? Изменяется ли имя типа, в зависимости от того, в каком месте исходного кода вы на него смотрите?

Все это становится несколько запутанным. Я предпочитаю думать о типах, будто логически они вообще не содержат имени. Фрагменты кода “12”, и “10 + 2”, и “3 * 4”, и “0x0C” не являются именами для числа 12, все они являются выражениями, результат вычисления которых дает 12. Это всего лишь числа, способ записи зависит лишь от принятой нотации, но не имеет отношение к самому числу. С типами аналогично; фрагмент кода “List<string[][]> в определенном контексте может ссылаться на определенный тип, но этот код не должен содержать имя этого типа. У него нет имени.

Концепция «набора значений» также является проблемной, особенно, если этот набор может быть бесконечным «математическим» множеством.

Для начала давайте предположим, что у нас есть некоторое значение: как вы определите, какого оно типа? Существует бесконечно большое количество наборов, содержащих это значение, и, таким образом, это значение может относиться к бесконечному количеству типов! И правда, если строка “hello” является членом типа string, она также является членом типа object. Как же мы определяем «настоящий» тип этого значения?

Все становится еще более запутанным, если подумать следующим образом: «А, я знаю, а давайте скажем, что набор значений каждого типа определяется некоторым «предикатом», отвечающим на то, относится ли некоторое значение к определенному типу или нет». Это мысль кажется разумной, но теперь нужно ответить на вопрос, а сами типы являются значениями или нет? И если это так, тогда следующий предикат кажется вполне корректным: «тип, чьи значения являются типами, не принадлежащими своему собственному множеству типов». И тогда мы получаем парадокс Рассела (**).

Более того, идея определения типа по предикату, который определяет, относится ли конкретное значение к указанному типу или нет, не похоже на типичное понимание типов в программе на языке C#. В противном случае мы могли бы определить «типы предикатов» вида «x – четное целое», или «x – простое число», или «x – это строка, являющаяся корректной программой на языке VBScript» и тому подобное. Но в системе типов языка C# подобных типов не существует.

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

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

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

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

(**) Когда Рассел понял, что его парадокс подрывает всю арифметическую теорию Фреге, он, вместе с Вайтхедом (Whitehead) разработал теорию, сегодня известную как «расширенная теория типов» (ramified theory of types) – зубодробительную теорию, свободную от подобных парадоксов. И хотя математические основы теории множеств, теории категорий и т.п. очень интересны, я их понимаю не настолько хорошо, чтобы рассматривать их здесь более подробно. Помните, мы ищем определение «типа», упрощающего практическое использование современных языках программирования.

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

Comments

• Anonymous
  July 01, 2012
  Интересно, как всегда. Спасибо!