Что означает, что язык статически типизирован?

Ответ 1

Пусть A - ваш Turing-полный язык, который должен быть статически типизирован, и пусть A '- это язык, который вы получаете от A, когда вы удаляете проверку типов (но не аннотации типа, поскольку они также служат другим целям). Принятые программы A будут подмножеством принятых программ A '. Так, в частности, A 'также будет завершающим Turing.

С учетом вашего переводчика P от B до A (и наоборот). Что он должен делать? Это может сделать одно из двух:

• Во-первых, он может переводить каждую программу y из B в программу A. В этом случае LPy всегда будет возвращать True, поскольку программы A по определению корректно напечатаны.

• Во-вторых, P может перевести каждую программу y из B в программу A '. В этом случае LPy вернет True, если Py будет программой A и False, если нет.

Поскольку первый случай не дает ничего интересного, давайте придерживаться второго случая, который, вероятно, вы имеете в виду. Означает ли функция LP, определенная в программах B, что-нибудь интересное о программах B? Я говорю "нет", потому что он не является инвариантным при изменении P. Поскольку A является полным Тьюринга, даже во втором случае P можно выбрать так, чтобы его изображение находилось в A. Тогда LP было бы постоянно True. С другой стороны, P можно выбрать так, чтобы некоторые программы отображались в дополнение к A в '. В этом случае LP выскальзывает False для некоторых (возможно, всех) программ B. Как вы можете видеть, вы не получаете ничего, что зависит только от y.

Я также могу сделать это более математически следующим образом: существует категория C языков программирования, объекты которой являются языками программирования и морфизмы которых являются переводчиками с одного языка программирования на другой. В частности, если существует морфизм P: X → Y, то Y, по крайней мере, такой же выразительный, как X. Между каждой парой языковых языков Тьюринга существуют морфизмы в обоих направлениях. Для каждого объекта X из C (т.е. Для каждого языка программирования) мы имеем ассоциированное множество, например {X} (плохая нотация, я знаю) тех частично определенных функций, которые могут быть вычислены с помощью программ из X. Каждый морфизм P: X → Y тогда индуцирует включение {X} → {Y} множеств. Формально инвертируем все морфизмы P: X → Y, которые индуцируют тождество {X} → {Y}. Я назову итоговую категорию (которая, в математическом смысле, является локализацией С) через С '. Теперь включение A → A 'является морфизмом в C'. Однако он не сохраняется при автоморфизмах А ', т.е. Морфизм А → А' не является инвариантом А 'в С'. Другими словами: из этой абстрактной точки зрения атрибут "статически типизированный" не является определяемым и может быть произвольно привязан к языку.

Чтобы яснее указать, вы также можете представить C 'как категорию, скажем, геометрических фигур в трехмерном пространстве вместе с евклидовыми движениями как морфизмы. A 'и B являются затем двумя геометрическими фигурами, а P и Q - евклидовыми движениями, переводящими B в A' и наоборот. Например, A 'и B могут быть двумя сферами. Зафиксируем теперь точку на A ', которая будет стоять за подмножество A из A'. Назовем этот пункт "статически типизированным". Мы хотим знать, является ли точка B статически типизированной. Итак, мы берем такую ​​точку y, сопоставляем ее через P в 'и проверяем, является ли это нашей отмеченной точкой на A'. Как легко видеть, это зависит от выбранного отображения P или, говоря другими словами: отмеченная точка на сфере не сохраняется автоморфизмами (которые представляют собой евклидовы движения, отображающие сферу на себя) этой сферы.

Ответ 2

Если, вы можете перевести каждый B '(программу, написанную в B) в эквивалентную A' (что верно, если B '), тогда язык B обладает таким же "типом безопасности" "как язык А (в теоретическом смысле, конечно;-) - в основном это означало бы, что B таков, что вы можете делать идеальный вывод. Но это крайне ограничено для динамического языка - например, рассмотрим:

if userinput() = 'bah':
    thefun(23)
else:
    thefun('gotcha')

где thefun (пусть предположим) является typeafe для аргумента int, но не для аргумента str. Теперь - как вы переводите это на язык A во-первых...?

Ответ 3

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

• A не может быть сопоставлен с B
• тип безопасности не является лексическим свойством языка

или и то, и другое. Моя интуиция говорит, что последнее, вероятно, является точкой отсчета: этот тип безопасности является металингвистическим свойством.

Ответ 4

Там нет ничего "подозрительного".;)

Множество Turing-полных языков, которые являются безопасными по типу относительно любой нетривиальной системы типа [ 1] T, является строгим подмножеством языков Turing-complete. Таким образом, в общем случае не существует транслятор P ^-1 от B до A; поэтому ни один из переводчиков-переводчиков типа LP ^-1 не использует.

Реакция на коленный рефлекс на такое требование может быть: ерунда! Оба A и B являются Turing-complete, поэтому я могу выразить любую вычислимую функцию на любом языке! И действительно, это правильно - вы можете выразить любую вычислимую функцию на любом языке; однако, довольно часто, вы также можете выразить немного больше. В частности, вы можете построить выражения, чья денотационная семантика не определена корректно, например, те, которые могут с радостью попытаться взять арифметическую сумму строк символов "foo" и "bar" (это суть Chubsdad Алекс Мартелли ответ). Эти типы выражений могут быть "в" языке B, но могут просто не выражаться в языке A, поскольку денотационная семантика undefined, поэтому нет разумного способа их перевода.

Это одна из сильных сторон статической типизации: если ваша система типов не может во время компиляции доказать, что вышеупомянутая функция получит какие-либо параметры, но те, для которых результат операции арифметического сложения определен корректно, он может быть отклонен как не типичный.

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

[ 1] Нетривиальным я имею в виду то, что не все возможные выражения хорошо типизированы.

Ответ 5

Я понимаю, что это связано с временем компиляции и временем выполнения. В статически типизированном языке большинство проверок типов выполняется во время компиляции. На динамически типизированном языке большая часть проверки типа выполняется во время выполнения.

Ответ 6

Позвольте мне ответить на это наоборот:

Существует два разных типа "динамического" программирования.

Один из них "динамически типизирован", что означает, что у вас есть какая-то оболочка, в которой вы можете программировать, введя определения в эту оболочку, подумайте об этом как о оболочке Python IDLE.

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