Обсудим основы дисциплины типов в рамках .NET. Напомним, что история развития математических формализаций для типовых теорий изложена во вступительной лекции, а основа теории типов - в лекции 6.
Обобщим те преимущества, которые отличают языки программирования и формальные теории с типами.
Прежде всего, отметим то бесспорное преимущество типизированных исчислений, что при таком подходе моделируемая предметная область лучше структурирована, чем в том случае, если отсутствует сегментация на типы. Типизация структурирует предметную область по иерархическому принципу.
Введение типизации облегчает и упорядочивает не только восприятие, но и управление предметной областью. Манипулирование типизированными элементами носит более целенаправленный характер, причем появляется возможность обрабатывать разнородные сущности предметной области различным образом, а однородные (или, точнее, однотипные) - единообразно.
Перейдем к языкам программирования и практике проектирования и реализации программных систем. В случае построения языка программирования по принципу строгой типизации несоответствия типов фиксируются до начала этапа выполнения программы (на этапе контроля соответствия типов в ходе трансляции), что гарантирует отсутствие семантических (смысловых) и логических ошибок и безопасность программного кода.
Напомним классификацию систем типизации в языках программирования.
Исторически наиболее распространенной для языков программирования является строгая типизация. При таком формировании системы типов в языке в любой момент существования любого языкового объекта существует однозначное соответствие между объектом и его типом. Другими словами, можно запрограммировать функцию, определяющую тип объекта, подобную ранее рассмотренной нами функции typeof языка программирования C#. Строго типизированными являются классические императивные языки программирования Pascal, FORTRAN, PL/I и др. Отметим, что классический вариант языка программирования C не является строго типизированным.
Сильная типизация необходима для обеспечения корректности связывания переменных со значениями до выполнения программы.