Что означает программирование на уровне типов во время выполнения?

Как вы правильно сказали, Haskell [без странных расширений] имеет полное стирание типов. Это означает, что все, что вычислено исключительно на уровне типа, стирается во время выполнения.

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

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

Без программирования на уровне типов ваши варианты:

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

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

К этому моменту все типы были стерты, но вы по-прежнему можете гарантировать, что ваш код не вылетит / не вернет тарабарщину, потому что компилятор проверил, что этого не может произойти.

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

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

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