Сильна і слабка типізація

У комп’ютерному програмуванні це один зі способів розмовної класифікації мов програмування чи система типів мови робить її строго типізованою або слабко типізованою. Точного технічного визначення цього терміну немає. Різні автори не мають єдиної думки щодо неявного значення термінів і відносного рейтингу «сили» систем типів основних мов програмування.З тої ж причини автори, які хочуть однозначно писати про системи типів, часто уникають термінів «сильна типізація» та «слабка типізація» на користь конкретних виразів, таких як «безпека типів».

Загалом, строго типізована мова має суворіші правила типізації під час компіляції, а це означає, що помилки та відмови виникають частіше. Більшість цих правил впливає на призначення змінних, значення, що повертаються функцією, аргументи процедури та виклик функції. Динамічно типізовані мови (де перевірка типів відбувається під час виконання) також можуть бути строго типізовані. Важливо пам'ятати, що в динамічно типізованих мовах значення, мають типи,а не змінні. Слабко типізована мова має більш вільні правила типізації. Вільні правила можуть давати непередбачувані або навіть помилкові результати або може виконувати неявне перетворення типів під час виконання. Прихильники слабко типізованих мов вважають такі занепокоєння перебільшеннями та вбачають, що статична типізація створює експоненціально більший набір проблем.Іншою, але спорідненою концепцією є прихований тип.

Історія

Барбара Лісков і С.Зіллес у 1974 році дали визначення строго типізованої мови, як мови у якій: «Кожного разу, коли об’єкт передається від функції, що викликає до викликаної функції, його тип повинен бути сумісний із типом, оголошеним у викликаній функції». К. Джексон у 1977 році писав: «У строго типізованій мові кожна область даних матиме окремий тип, і кожен процес встановлюватиме свої вимоги до зв’язку в термінах цих типів».

Визначення понять «сильний» або «слабкий»

Доказами "сильної" або "слабкої" є кілька різних рішень мовного дизайну. Багато з них точніше розуміти як наявність або відсутність безпеки типу, безпеки пам’яті, статичної перевірки типу або динамічної перевірки типу . «Сильна типізація», найчастіше стосується використання типів мов програмування для того, щоб:

1. зафіксувати інваріанти коду
2. забезпечити правильність коду
3. виключити певні класи помилок програмування

Таким чином, для досягнення цих цілей використовується багато дисциплін «сильної типізації».

Неявні перетворення типів і «каламбур»

Деякі мови програмування дозволяють легко використовувати значення одного типу таким чином, ніби це значення іншого типу. Іноді це описується як "слабкий тип".Ааз Марух, наприклад, зауважує, що «приведення типів виникає, коли у вас є статично типізована мова, і ви використовуєте синтаксичні особливості мови, щоб примусово використовувати один тип, якби це був інший тип.Приведення типів зазвичай є симптомом слабкого друку.З іншого боку, перетворення, створює абсолютно новий об’єкт відповідного типу».

Інший приклад, GCC описує це як тип каламбур, та попереджає, що це порушить строгі псевдоніми. Thiago Macieira обговорює низку проблем, які можуть виникнути, коли набір текстів змушує компілятор робити невідповідні оптимізації. Прикладів мов, які дозволяють неявне приведення типів, але безпечним для типів способом є багато. До прикладу,і C++ і C# дозволяють програмам визначати оператори для перетворення значення з одного типу в інший з чітко визначеною семантикою. За умови, коли компілятор C++ стикається з таким перетворенням, він розглядає операцію так само, як виклик функції. Навпаки, перетворення значення в тип Cvoid* — небезпечна операція, невидима для компілятора.

Покажчики

Деякі мови програмування відображають вказівники, як числові значення і дозволяють користувачам виконувати арифметичні дії над ними.Іноді ці мови називають «слабко типізованими», оскільки арифметика вказівників може бути використана для обходу системи типів мови.

Об’єднання без тегів

Деякі мови програмування підтримують об’єднання без тегів, що дозволяє відображати значення одного типу у вигляді значеннь іншого типу.

Статична перевірка типу

У статті Луки Карделлі Типове програмування автор описує «сильну систему типу» як система, в якій відсутня можливості неперевіреної помилки типу виконання. В іншому тексті відсутність неперевірених помилок часу виконання визначають як безпека або безпека типу; Ранні статті Тоні Хоара називають цю властивість "безпекою .

Динамічна перевірка типу

В деяких мовах програмування відсутні статичні перевірки типів. У багатьох таких мовах легко писати програми, які були б відхилені більшістю статичних перевірок типів. Наприклад, змінна може зберігати або число, або логічне значення "false".Важливо звернути увагу на те, що деякі з цих визначень є суперечливими, інші - концептуально незалежними, а треті є окремими випадками (з додатковими обмеженнями) інших, більш «ліберальних» (менш сильних) визначень. Через велику розбіжність між цими визначеннями можна спиратимсь на твердження щодо більшості мов програмування, що вони або сильно, або слабко типізовані. Наприклад:

• Java, Pascal, Ada та C вимагають, щоб усі змінні мали оголошений тип і підтримують використання явних приведення арифметичних значень до інших арифметичних типів. Інколи кажуть, що Java, C#, Ada та Pascal мають більш сувору типізацію, ніж C, це твердження, ймовірно, ґрунтується на тому факті, що C підтримує більше типів неявних перетворень, а C також дозволяє явно наводити значення вказівників, тоді як Java та Pascal не. Саму Java можна вважати більш жорстко типізованою, ніж Pascal, оскільки методи ухилення від статичної системи типів у Java контролюються системою типів віртуальної машини Java . C# і VB. NET у цьому відношенні подібні до Java, хоча вони дозволяють вимкнути динамічну перевірку типів шляхом явного розміщення сегментів коду в "небезпечному контексті". Система типів Паскаля була описана як «надто сильна», оскільки розмір масиву або рядка є частиною його типу, що робить деякі завдання програмування дуже складними.
• Smalltalk, Ruby, Python і Self усі «строго типізовані» в тому сенсі, що помилки введення запобігають під час виконання, і вони не виконують неявного перетворення типів, але ці мови не використовують статичну перевірку типів: компілятор не перевіряє та не виконує правила обмеження типу. Термін «качиний тип» тепер використовується для опису парадигми динамічного друку, що використовується мовами цієї групи.
• Всі мови сімейства Lisp є "строго типізованими" в тому сенсі, що помилки введення запобігаються під час виконання. Деякі діалекти Lisp, такі як Common Lisp або Clojure, підтримують різні форми декларацій типів , а деякі компілятори (CMUCL і подібні) використовують ці декларації разом із виведенням типу, щоб уможливити різні оптимізації, а також обмежені форми перевірки типу під час компіляції.
• Standard ML, F#, OCaml, Haskell, Go та Rust статично перевіряються типами, але компілятор автоматично визначає точний тип для більшості значень.
• Мова асемблера і Forth можна охарактеризувати як нетипізовану.Немає перевірки типу; Програміст повинен переконатися, що дані, надані функціям, належного типу. Будь-яке перетворення типу є явним.

Дивіться також

• Порівняння мов програмування
• Тип даних включає більш детальне обговорення питань типізації
• Проектування за контрактом (строга типізація як неявна форма контракту)
• Латентне типування
• Безпека пам'яті
• Тип безпеки
• Тип системи

Список літератури

1. . Cornell University, Department of Computer Science. 2005. Архів оригіналу за 23 листопада 2015. Процитовано 23 листопада 2015. 
2. The Unreasonable Effectiveness of Dynamic Typing for Practical Programs. Vimeo. 12 вересня 2013. Процитовано 21 березня 2021. 
3. Liskov, B; Zilles, S (1974). Programming with abstract data types. ACM SIGPLAN Notices 9 (4): 50–59. doi:10.1145/942572.807045.  Проігноровано невідомий параметр |citeseerx= (довідка)
4. Jackson, K. (1977). Parallel processing and modular software construction. Design and Implementation of Programming Languages. Lecture Notes in Computer Science 54: 436–443. ISBN 3-540-08360-X. doi:10.1007/BFb0021435. 
5. Aahz. Typing: Strong vs. Weak, Static vs. Dynamic. Процитовано 16 серпня 2015. 
6. Type-punning and strict-aliasing - Qt Blog. Qt Blog. Процитовано 18 лютого 2020. 
7. Luca Cardelli, "Typeful programming"
8. Hoare, C. A. R. 1974. Hints on Programming Language Design. In Computer Systems Reliability, ed. C. Bunyan. Vol. 20 pp. 505–534.
9. InfoWorld. 25 квітня 1983. Процитовано 16 серпня 2015. 
10. Kernighan, Brian (1981). . Архів оригіналу за 6 квітня 2012. Процитовано 22 жовтня 2011. 
11. CLHS: Chapter 4. Процитовано 16 серпня 2015. 
12. . Архів оригіналу за 8 March 2016. Процитовано 16 серпня 2015.