Программирование на языке Scala/Строгая статическая типизация

Типы данных

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

Например, тип данных "целые числа" имеет в своем составе элементы 0, 1, 2, эти элементы могут складываться или вычитаться. А тип данных "строка" может состоять из нескольких символов, и этот тип данных может иметь операцию слияния.

Определения терминов

Строгая типизация (Strong Typing):

Это означает, что типы данных в языке строго соблюдаются, и компилятор обеспечивает выполнение опраций только с соответствующими типами. Например, если вы объявили переменную как "целые числа", то вы не сможете случайно присвоить ей значение "строка" без явного приведения типов.

Статическая типизация (Static Typing):

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

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

Математичность

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

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

Вот как строгая статическая типизация в Scala способствует математичности в программировании:

Четкие типы данных: Строгая типизация означает, что каждое значение и выражение имеют определенный тип данных. Это позволяет программистам лучше понимать, какие данные они могут использовать и какие операции доступны для каждого типа. Для каждого типа должны использоваться только свои операции. Также можно заранее определиться с областью значений для каждого типа.
Функциональные типы: В функциональном программировании, типы функций являются важным фактором. Строгая типизация позволяет точно определить типы параметров и возвращаемых значений функций, что упрощает их использование и композицию.
Статическая проверка типов: Компилятор Scala проверяет типы программы на этапе компиляции, что позволяет обнаруживать множество ошибок до запуска программы. Это помогает предотвращать некоторые ошибки времени выполнения.
Ограничения на преобразование типов: Строгая типизация в Scala не позволяет неявно преобразовывать значения между различными типами данных, что помогает избежать ошибок и неожиданного поведения.

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

Типы в физике

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

сила тяготения = гравитационная постоянная * масса первого тела * масса второго тела / расстояние между телами²

Единицы измерения:

сила тяготения - Ньютон, N = kg * m / s²
гравитационная постоянная - m³ /( kg * s²)
масса первого тела - килограмм, kg
масса второго тела - килограмм, kg
расстояние между телами - метр, m

Подставляем в формулу единицы измерения

$kg*m/s^{2}=(m^{3}/(kg*s^{2}))*kg*kg/m^{2}$

сокращаем

$kg*m/s^{2}=kg*m/s^{2}$

Типы в левой и правой части единицы измерения идентичны. Это позволяет заявить, что с формальной (математической) точки зрения данная формула корректна.

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

Проблемы строгой статической типизации

Большое количество типов: Scala может иметь довольно сложную систему типов, особенно если вы используете богатый набор библиотек и фреймворков. Это может привести к большому количеству типов, которые требуется объявлять и учитывать, что может сделать код менее читабельным.
Относительная сложность: Некоторые аспекты строгой типизации могут быть относительно сложными для понимания, особенно для новичков. Например, работа с обобщениями (generics) может вызвать затруднения.
Громоздкие объявления типов: В некоторых ситуациях, когда типы данных довольно сложны или неочевидны, программистам приходится писать длинные и громоздкие объявления типов, что может затруднить понимание кода.
Оверхед при компиляции: Строгая типизация может привести к увеличению времени компиляции, особенно для больших проектов. Компилятор Scala должен проверить согласованность типов и правильность их использования, что может занять время.
Чрезмерная абстракция: В некоторых случаях, из-за строгой типизации, программисты могут быть склонны создавать излишнюю абстракцию, что может усложнить код и затруднить его понимание.

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

Домашнее задание:

Выяснить что такое динамическая типизация и в каких языках она используется.