Что значит для языка быть статически типизированным?

Question

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

Моя проблема с этим заключается в следующем:

Предположим, что у нас есть два полных языка тьюринга, A и B. Предполагается, что A является «безопасным типом», а «B» - не безопасным. Предположим, мне дали программу L, чтобы проверить правильность любой программы, написанной на A. Что мешает мне перевести любую программу, написанную на B, на A, применяя L. Если P переводит с A на B, тогда почему PL не является допустимый тип проверки для любой программы, написанной на B?

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

Answer 1

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

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

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

Answer 2

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

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

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

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

Поскольку первый случай не дает ничего интересного, давайте придерживаться второго случая, который, вероятно, и имеет в виду. Рассматривает ли функция LP, определенная в программах B, что-нибудь интересное о программах B? Я говорю «нет», потому что он не является инвариантом при изменении P. Поскольку A является Тьюрингово-полным, даже во втором случае P можно было бы выбрать так, чтобы его изображение оказалось в A. Тогда LP будет постоянно True. С другой стороны, P можно выбрать так, чтобы некоторые программы отображались в дополнение к A в 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}. Я назову результирующую категорию (которая в математических терминах является локализацией C) как C '. Теперь включение A -> A 'является морфизмом в C'. Однако он не сохраняется при автоморфизмах A ', то есть морфизм A -> A' не является инвариантом A 'в C'. Другими словами: с этой абстрактной точки зрения атрибут «статически типизированный» не определим и может быть произвольно присоединен к языку.

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

Answer 3

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

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

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

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

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

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

Answer 4

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

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

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

Answer 5

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

Answer 6

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

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

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

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