Является ли Racket (и Typed Racket) сильно или мягко напечатанным?

Question

Я понимаю, что определения «строго типизированного» и «мягко типизированные» являются свободными и открытыми для интерпретации, но мне еще предстоит найти четкое определение относительно нетипизированного Racket (который из моего понимания означает динамически типизированный) и Typed Racket on это.

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

Answer 1

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

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

Итак, что такое система типа? В наши дни я утверждаю, что термин обычно относится к системе, которая исследует программу, и статически [*] выводит свойства программы. Как правило, если это называется системой типов, это означает присоединение «типа» к каждому выражению, которое сдерживает набор/класс значений, которые может оценивать выражение. Обратите внимание, что это определение в основном делает термин «динамически типизированный» бессмысленным.

Обратите внимание на гигантскую лазейку: существует «система тривиального типа», которая просто присваивает каждому выражению «тип», содержащий все значения программы. Итак, если вы хотите, вы можете рассматривать буквально любой язык, который будет статически типизирован. Или, если хотите, «единство» (обратите внимание на «i» там).

Хорошо, до латуни.

Ракетка не напечатана. Или, если хотите, «динамически типизировано» или «унифицировано» или даже «нетипизировано».

Типичная ракетка is Набрал. Он имеет систему статического типа, которая присваивает каждому выражению один тип.Его система типа «звук», что означает, что оценка программы будет соответствовать требованиям, предъявляемым системой типов: если Typed Racket (далее TR) проверяет вашу программу и назначает тип «Природный» на номер выражение, то он определенно будет оцениваться до натурального числа (при отсутствии ошибок в контролерах типа TR или в системе Racket).

Typed Racket имеет много необычных характеристик, которые позволяют коду, написанному в TR, взаимодействовать с кодом, написанным в Racket. Наиболее известным из них является «написание ввода», что позволяет программе TR обрабатывать такие типы, как (U Number String) (то есть значение либо число или строка) без взрыва, как это делали ранее аналогичные системы типов.

Это не относится к делу: ваш вопрос касался Racket и TR, и простой ответ заключается в том, что базовый язык Racket не имеет системы статического типа, а TR делает.

[*] определение термина «статические» выходит за рамки этого сообщения :).

Answer 2

Сильно типизированный и слабо типизированный не имеет ничего общего со статической или динамической типизацией. вы можете комбинировать их, чтобы у вас было 4 варианта. (сильный/статический, слабый/статический, сильный/динамический, слабый/динамический). Схема (и, следовательно, #lang racket) динамична и пробита.

> (string-append "test" 5) 
string-append: contract violation 
    expected: string? 
    given: 5 
    argument position: 2nd 
    other arguments...: 

Все значения имеют тип и функции могут потребовать тип. Если вы хотите добавить строку к номеру, вы получите ошибку типа. вам необходимо явно указать число в строку, используя number->string, чтобы удовлетворить контракт всех аргументов, являющихся строками. При использовании слабо типизированных языков, таких как JavaScript, он просто передаст число в строку, чтобы удовлетворить функцию. Меньше кода, но, возможно, больше ошибок времени выполнения.

Поскольку схема строго типизирована, #lang typed/racket определенно тоже.

Хотя динамически набирается схема/#lang racket Я не совсем уверен, что #lang typed/racket полностью статичен. The Guide называет это постепенно типизированным языком.

Answer 3

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

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

# This Perl program prints 6. 
print 3 * "2a" 

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

Так как Typed Racket не изменяет семантику времени выполнения Racket (за исключением введения дополнительной проверки контракта), она будет так же строго типизирована, как обычный Racket.

---

Кстати, обычные слова, используемые людьми, являются слабыми и сильными. Мягкая печать может относиться к one specific kind of type system, которая была создана в 90-х годах. Это не получилось так хорошо, что является одной из причин того, что люди придумывают систему Gradual Typing, которая используется на таких языках, как Typed Racket и Typcript.