Зачем двоеточию обозначать, что значение принадлежит типу?

19

Пирс (2002) вводит отношение типирования на странице 92, записывая:

Отношение типа для арифметических выражений, написанное «t: T», определяется набором правил вывода, назначающих типы терминам

и сноска говорит, что символ часто используется вместо:. Мой вопрос просто, почему теоретики типов предпочитают использовать: over ? Если тип является набором значений, то имеет смысл написать , никаких новых обозначений не требуется.TTT

Похоже ли это на то, что некоторые авторы cs предпочитают даже считая, что это злоупотребление нотацией и должно быть написано ?3N2знак равноО(N2)3N2О(N2)

Бьорн Линдквист
источник
7
Предикат членства ИксИкс может быть либо истинным, либо ложным, тогда как объявление типа Икс:Икс обычно интерпретируется как фактическое утверждение, которое объявляется истинным, или его истинность может быть получена чисто синтаксическими средствами. Сравните это с простым числом, для которого недостаточно синтаксического метода членства.
Муса Аль-Хасси
4
@ MusaAl-hassy: это искажение того, что происходит. Это не объявляется как истина, так как это означало бы, что я могу, например, «объявить», что « false: int». Это также не тот случай, когда суждение должно быть обязательно получено «чисто синтаксическими средствами», например, в случае теории внутренних типов категории с семействами.
Андрей Бауэр
3
Смежный вопрос по cs.se: Какова именно семантическая разница между множеством и типом?
Дискретная ящерица
2
Чтобы добавить комментарий @ MusaAl-hassy, ​​в вычислительной теории типов Боба Констебла Стюарта Аллена, Боба Харпера и др. используют для ввода суждений, потому что это больше похоже на предикат членства (см. Этот доклад, слайд 25, для примера).
xrq
3
Конечно, также является неправильным обозначением и должно действительно записываться как λ n .3 n 2O ( λ n . N 2 ) ? (Математики могут предпочесть п 3 п 2O ( п п 2 ) .)3n2O(n2)λn.3n2O(λn.n2)N3N2О(NN2)
Оскар Cunningham

Ответы:

12

Потому что то, что справа от двоеточия, не обязательно является набором, а то, что слева от двоеточия, не обязательно является членом этого множества.

Теория типов началась в начале 20-го века как подход к основанию математики. Бертран Рассел обнаружил парадокс в наивной теории множеств, и он работал над теорией типов как способом ограничить выразительную силу теории множеств, чтобы избежать этого (и любого другого) парадокса. За прошедшие годы Рассел и другие определили множество теорий типов. В некоторых теориях типов типы - это наборы с определенными свойствами, но в других - это другой тип зверя.

В частности, многие теории типов имеют синтаксическую формулировку. Есть правила, которые заставляют вещь иметь тип. Когда правила печатания используются в качестве основы для теории, важно отличать то, что говорят правила печатания, от того, что можно вывести, применяя дополнительные внешние знания. Это особенно важно, если правила типизации являются основой для теории доказательств: теоремы, которые основаны на теории множеств с классической логикой и аксиомой выбора, могут, например, быть или не быть в конструктивной логике. Одна из основополагающих работ в этой области - « Формулировка простой теории типов» Черча (1940)

Возможно, способ, которым различие между типами и наборами является наиболее очевидным, состоит в том, что самое основное правило для наборов, а именно, что два набора равны, если они имеют одинаковые элементы, обычно не применяется к типам. См . Ответ Андрея Бауэра здесь и его ответ на связанный вопрос для некоторых примеров. Эта вторая тема имеет другие ответы, которые стоит прочитать.

В типизированном исчислении сказать, что типы являются множествами, фактически дать семантику типам. Дать исчисление теоретико-типовой семантики нетривиально. Например, предположим, что вы определяете язык с помощью функций. Какой набор является типом функции? Полные функции определяются их графом, как нас учат в теории множеств 101. Но как насчет частичных функций? Хотите ли вы дать всем не завершающим функциям одинаковую семантику? Вы не можете интерпретировать типы как наборы для исчисления, которое допускает рекурсивные функции, пока вы не ответите на этот вопрос. Придание денотативной семантики языкам программирования или исчисления было трудной проблемой в начале 1970-х годов. Основным документом здесь является На пути к математической семантики для компьютерных языков (1971) поДана Скотт и Кристофер Стрейчи . В Haskell wikibook есть хорошая презентация темы.

Как я писал выше, вторая часть ответа заключается в том, что даже если вам удалось дать типам теоретико-множественную семантику, вещь слева от двоеточия не всегда является элементом множества. Значения имеют типы, но также и другие вещи, такие как выражения и переменные . Например, выражение в типизированном языке программирования имеет тип, даже если оно не заканчивается. Вы можете быть готовы приравнивать integerи Z , но (x := 0; while true; do x := x + 1; x)это не является элементом Z .

Я не знаю, когда возникли обозначения двоеточия для типов. Теперь он стандартен в семантике и распространен в языках программирования, но ни Рассел, ни Черч не использовали его. Алгол не использовал его, но в значительной степени вдохновленный Алголом язык, который Паскаль использовал в 1971 году. Я подозреваю, что он был не первым, хотя во многих теоретических работах начала 1970-х годов используется обозначение, но я не знаю ранее использовать. Интересно, что это произошло вскоре после того, как концепции типов из программирования и логики были объединены - как показывает Саймон Мартини в книге «Несколько типов типов в языках программирования» , то, что до 1960-х годов называлось «типом» в языках программирования, пришло из народного языка. Использование слова, а не из теории типов.

Жиль "ТАК - перестань быть злым"
источник
37

Основная причина предпочтения записи двоеточия t:T отношению членства tT состоит в том, что отношение членства может вводить в заблуждение, поскольку типы не являются (просто) коллекциями .

[ Дополнительно: я должен отметить, что исторически теория типов была написана с использованием . Концепция типа Мартина-Лёфа предназначалась для конструктивного захвата множеств, и уже Рассел и Уайтхед использовали ϵ для членства в классе. Было бы интересно отследить момент, когда : стало более распространенным, чем .]

Тип описывает определенный тип конструкции, т. Е. Как создавать объекты с определенной структурой, как их использовать и какие уравнения в них содержатся.

Например типа продукта × B есть правила вводных , которые объясняют , как сделать упорядоченные пары, а также правила элиминации объясняющих , что мы можем спроектировать первые и вторую компоненту из любого элемента A × B . Определение A × B вовсе не начинать со слов «совокупность всех ...» и ни делает это сказать где - нибудь что - нибудь вроде «все элементы A × B являются пары» (но это следует из определения , что каждый элемент × B является propositionallyA×BA×BA×BA×BA×Bравно пару). В Контрасте, теоретико-множественное определение X×Y является указано как «множество всех упорядоченных пар ...».

Обозначения t:T означает тот факт , что t имеет структуру , описанную T .

Тип T не следует путать с его расширением , что совокупность всех объектов типа T . Тип не определяется его расширением, так же как группа не определяется его набором несущих. Кроме того, может случиться так, что два типа имеют одинаковое расширение, но различаются, например:

  1. Тип всех четных простых чисел, больших двух: Σ(n:N).isprime(n)×iseven(n)×(n>2) .
  2. Тип всех нечетных простых чисел, меньших двух: Σ(n:N).isprime(n)×isodd(n)×(n<2) .

Расширение обоих пусто, но они не одного типа.

Существуют и другие различия между теоретикой типов : и теорией . Объект a в теории множеств существует независимо от того, к каким наборам он принадлежит, и он может принадлежать нескольким множествам. В отличие от этого , большинство теорий типа удовлетворяют уникальность ввода: если t:T и t:U то TU . Иными словами, теоретико-типовая конструкция t имеет ровно один тип T , и на самом деле нет способа иметь только объект t без его (однозначно определенного) типа.

Другим отличием является то, что в теории множеств , мы можем отрицать тот факт , что aA , написав ¬(aA) или aA . Это невозможно в теории типов, потому что t:T - это суждение, которое может быть получено с использованием правил теории типов, но в теории типов нет ничего, что позволило бы нам утверждать, что что-то не было получено. Когда ребенок делает что-то из блоков LEGO, они с гордостью бегут к родителям, чтобы показать им конструкцию, но они никогда не бегут к родителям, чтобы показать им, что они не сделали.

Андрей Бауэр
источник
1
Андрей, отличный ответ. Вы случайно не знаете историческое происхождение обозначения толстой кишки?
Андреас Россберг
Увы, нет. Теория типа Черча использовала индексы, т. Е. для переменной типа α . Рассел и Уайтхед использовали ϵ для отношения принадлежности к классу. Алгол 68 ставит типы перед именами переменных. Теория типов Мартина-Лёфа 1972 года использует , так же как и версия 1984 года , но [версия 1994 года] использует двоеточие. Иксααε
Андрей Бауэр
1
Итак, ваш аргумент в том, что тип подобен группе? Это имеет смысл, но обозначение является общим в абстрактной алгебре. граммграмм
Бьорн Линдквист
2
@ BjörnLindqvist: я не думаю, что этот ответ является полной историей. Даже в стандартной математике мы используем « » , чтобы обозначить , что п является функцией от S до T . Почему мы не использовали « f ( S T ) » или что-то подобное? Ну, мы просто не сделали. Конечно, есть веская причина избегать использования « » в представлении определенных типов теорий типов, просто потому, что мы не хотим, чтобы люди, обученные ZFC, думали, что это как ZFC-множества, что, очевидно, не является кейс. Но это не значит , что двоеточие не имеет ужее:STеSTf(ST)широко использовались задолго до того, как теория типов стала популярной.
user21820
1
@ user21820 "Почему мы не использовали ?" Просто размышляю: потому что математики никогда не думали о S T как о множестве. Для истории этой записи см. Здесь . Я сомневаюсь, что двоеточие от f : S T было вдохновением для теоретиков типа. Более вероятно, что двоеточие теоретиков типа связано с тем фактом, что не является символом ASCII. f(ST)STе:ST
Майкл
5

Бьорн,

Возможно, есть более ранняя ссылка, но, с одной стороны, двоеточие использовалось в языке программирования Pascal:

Первый гугл хит для Паскаля

Бьёрн Кьос-Хансен
источник
2
Разве не было более ранних языков программирования, которые использовали :?
Андрей Бауэр
@ AndrejBauer, действительно, я написал «Возможно, есть более ранняя ссылка, но ...», чтобы защититься от этого вероятного факта.
Бьёрн Кьос-Хансен
@AndrejBauer Algol этого не сделал. Был :использован в теоретических статьях , прежде чем 1970?
Жиль "ТАК - прекрати быть злым"
1
У Фортрана есть, REAL :: xно я не знаю, было ли это раньше Паскаля.
Майкл
1
@ Майкл Фортран появился раньше, чем Паскаль (около 1955 г. против 1970 г.), но я думаю, что этот специфический синтаксис был введен только в Фортране-90, намного позже, чем Паскаль. См., Например, здесь: fortranwiki.org/fortran/show/Modernizing+Old+Fortran
Федерико Полони