Является ли статическая типизация подмножеством динамической типизации?

Question

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

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

Answer 1

Технически, на самом деле все наоборот: «динамически типизированный» язык - это особый случай статически типизированного языка, а именно тот, который имеет только один тип (в математическом смысле). По крайней мере, такова точка зрения многих в сообществе систем типов.

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

Answer 2

статическая типизация происходит во время компиляции, а не во время выполнения! И это различие существенно !!

Подробнее см. Книгу Б. Пирса Типы и языки программирования .