У комп’ютерному програмуванні це один зі способів розмовної класифікації мов програмування чи система типів мови робить її строго типізованою або слабко типізованою. Точного технічного визначення цього терміну немає. Різні автори не мають єдиної думки щодо неявного значення термінів і відносного рейтингу «сили» систем типів основних мов програмування.З тої ж причини автори, які хочуть однозначно писати про системи типів, часто уникають термінів «сильна типізація» та «слабка типізація» на користь конкретних виразів, таких як «безпека типів».
Загалом, строго типізована мова має суворіші правила типізації під час компіляції, а це означає, що помилки та відмови виникають частіше. Більшість цих правил впливає на призначення змінних, значення, що повертаються функцією, аргументи процедури та виклик функції. Динамічно типізовані мови (де перевірка типів відбувається під час виконання) також можуть бути строго типізовані. Важливо пам'ятати, що в динамічно типізованих мовах значення, мають типи,а не змінні. Слабко типізована мова має більш вільні правила типізації. Вільні правила можуть давати непередбачувані або навіть помилкові результати або може виконувати неявне перетворення типів під час виконання. Прихильники слабко типізованих мов вважають такі занепокоєння перебільшеннями та вбачають, що статична типізація створює експоненціально більший набір проблем.Іншою, але спорідненою концепцією є прихований тип.
Історія
Барбара Лісков і С.Зіллес у 1974 році дали визначення строго типізованої мови, як мови у якій: «Кожного разу, коли об’єкт передається від функції, що викликає до викликаної функції, його тип повинен бути сумісний із типом, оголошеним у викликаній функції». К. Джексон у 1977 році писав: «У строго типізованій мові кожна область даних матиме окремий тип, і кожен процес встановлюватиме свої вимоги до зв’язку в термінах цих типів».
Визначення понять «сильний» або «слабкий»
Доказами "сильної" або "слабкої" є кілька різних рішень мовного дизайну. Багато з них точніше розуміти як наявність або відсутність безпеки типу, безпеки пам’яті, статичної перевірки типу або динамічної перевірки типу . «Сильна типізація», найчастіше стосується використання типів мов програмування для того, щоб:
- зафіксувати інваріанти коду
- забезпечити правильність коду
- виключити певні класи помилок програмування
Таким чином, для досягнення цих цілей використовується багато дисциплін «сильної типізації».
Неявні перетворення типів і «каламбур»
Деякі мови програмування дозволяють легко використовувати значення одного типу таким чином, ніби це значення іншого типу. Іноді це описується як "слабкий тип". Ааз Марух, наприклад, зауважує, що «приведення типів виникає, коли у вас є статично типізована мова, і ви використовуєте синтаксичні особливості мови, щоб примусово використовувати один тип, якби це був інший тип.Приведення типів зазвичай є симптомом .З іншого боку, перетворення, створює абсолютно новий об’єкт відповідного типу».
Інший приклад, GCC описує це як каламбур типізації, та попереджає, що це порушить строгі псевдоніми. Thiago Macieira обговорює низку проблем, які можуть виникнути, коли набір текстів змушує компілятор робити невідповідні оптимізації. Прикладів мов, які дозволяють неявне приведення типів, але безпечним для типів способом є багато. До прикладу, і і C# дозволяють програмам визначати оператори для перетворення значення з одного типу в інший з чітко визначеною семантикою. За умови, коли компілятор стикається з таким перетворенням, він розглядає операцію так само, як виклик функції. Навпаки, перетворення значення в тип C void* — небезпечна операція, невидима для компілятора.
Покажчики
Деякі мови програмування відображають вказівники, як числові значення і дозволяють користувачам виконувати арифметичні дії над ними.Іноді ці мови називають «слабко типізованими», оскільки арифметика вказівників може бути використана для обходу системи типів мови.
Об’єднання без тегів
Деякі мови програмування підтримують об’єднання без тегів, що дозволяє відображати значення одного типу у вигляді значень іншого типу.
Статична перевірка типу
У статті Луки Карделлі Типове програмування автор описує «сильну систему типу» як система, в якій відсутня можливості неперевіреної помилки типу виконання. В іншому тексті відсутність неперевірених помилок часу виконання визначають як безпека або безпека типу; Ранні статті Тоні Хоара називають цю властивість "безпекою .
Динамічна перевірка типу
В деяких мовах програмування відсутні статичні перевірки типів. У багатьох таких мовах легко писати програми, які були б відхилені більшістю статичних перевірок типів. Наприклад, змінна може зберігати або число, або логічне значення "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 можна схарактеризувати як нетипізовану. Не має перевірки типів; програміст повинен переконатися, що дані, надані функціям, мають належні типи. Будь-яке перетворення типу є явним.
Див. також
- Порівняння мов програмування
- Тип даних включає більш детальне обговорення питань типізації
- Проєктування за контрактом (строга типізація як неявна форма контракту)
- Латентне типування
- Безпека пам'яті
- Типобезпечність
- Система типізації
Примітки
- . Cornell University, Department of Computer Science. 2005. Архів оригіналу за 23 листопада 2015. Процитовано 23 листопада 2015.
- The Unreasonable Effectiveness of Dynamic Typing for Practical Programs. Vimeo. 12 вересня 2013. Процитовано 21 березня 2021.
{{}}
: Обслуговування CS1: Сторінки з параметром url-status, але без параметра archive-url () - Liskov, B; Zilles, S (1974). Programming with abstract data types. ACM SIGPLAN Notices. 9 (4): 50—59. CiteSeerX 10.1.1.136.3043. doi:10.1145/942572.807045.
- Jackson, K. (1977). Parallel processing and modular software construction. Design and Implementation of Programming Languages. Lecture Notes in Computer Science. 54: 436—443. doi:10.1007/BFb0021435. ISBN .
- Aahz. Typing: Strong vs. Weak, Static vs. Dynamic. Процитовано 16 серпня 2015.
- Type-punning and strict-aliasing - Qt Blog. Qt Blog. Процитовано 18 лютого 2020.
- Luca Cardelli, "Typeful programming"
- Hoare, C. A. R. 1974. Hints on Programming Language Design. In Computer Systems Reliability, ed. C. Bunyan. Vol. 20 pp. 505–534.
- InfoWorld. 25 квітня 1983. Процитовано 16 серпня 2015.
- Kernighan, Brian (1981). . Архів оригіналу за 6 квітня 2012. Процитовано 22 жовтня 2011.
- CLHS: Chapter 4. Процитовано 16 серпня 2015.
- . Архів оригіналу за 8 March 2016. Процитовано 16 серпня 2015.
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
U komp yuternomu programuvanni ce odin zi sposobiv rozmovnoyi klasifikaciyi mov programuvannya chi sistema tipiv movi robit yiyi strogo tipizovanoyu abo slabko tipizovanoyu Tochnogo tehnichnogo viznachennya cogo terminu nemaye Rizni avtori ne mayut yedinoyi dumki shodo neyavnogo znachennya terminiv i vidnosnogo rejtingu sili sistem tipiv osnovnih mov programuvannya Z toyi zh prichini avtori yaki hochut odnoznachno pisati pro sistemi tipiv chasto unikayut terminiv silna tipizaciya ta slabka tipizaciya na korist konkretnih viraziv takih yak bezpeka tipiv Zagalom strogo tipizovana mova maye suvorishi pravila tipizaciyi pid chas kompilyaciyi a ce oznachaye sho pomilki ta vidmovi vinikayut chastishe Bilshist cih pravil vplivaye na priznachennya zminnih znachennya sho povertayutsya funkciyeyu argumenti proceduri ta viklik funkciyi Dinamichno tipizovani movi de perevirka tipiv vidbuvayetsya pid chas vikonannya takozh mozhut buti strogo tipizovani Vazhlivo pam yatati sho v dinamichno tipizovanih movah znachennya mayut tipi a ne zminni Slabko tipizovana mova maye bilsh vilni pravila tipizaciyi Vilni pravila mozhut davati neperedbachuvani abo navit pomilkovi rezultati abo mozhe vikonuvati neyavne peretvorennya tipiv pid chas vikonannya Prihilniki slabko tipizovanih mov vvazhayut taki zanepokoyennya perebilshennyami ta vbachayut sho statichna tipizaciya stvoryuye eksponencialno bilshij nabir problem Inshoyu ale sporidnenoyu koncepciyeyu ye prihovanij tip IstoriyaBarbara Liskov i S Zilles u 1974 roci dali viznachennya strogo tipizovanoyi movi yak movi u yakij Kozhnogo razu koli ob yekt peredayetsya vid funkciyi sho viklikaye do viklikanoyi funkciyi jogo tip povinen buti sumisnij iz tipom ogoloshenim u viklikanij funkciyi K Dzhekson u 1977 roci pisav U strogo tipizovanij movi kozhna oblast danih matime okremij tip i kozhen proces vstanovlyuvatime svoyi vimogi do zv yazku v terminah cih tipiv Viznachennya ponyat silnij abo slabkij Dokazami silnoyi abo slabkoyi ye kilka riznih rishen movnogo dizajnu Bagato z nih tochnishe rozumiti yak nayavnist abo vidsutnist bezpeki tipu bezpeki pam yati statichnoyi perevirki tipu abo dinamichnoyi perevirki tipu Silna tipizaciya najchastishe stosuyetsya vikoristannya tipiv mov programuvannya dlya togo shob zafiksuvati invarianti kodu zabezpechiti pravilnist kodu viklyuchiti pevni klasi pomilok programuvannya Takim chinom dlya dosyagnennya cih cilej vikoristovuyetsya bagato disciplin silnoyi tipizaciyi Neyavni peretvorennya tipiv i kalambur Div takozh Kalambur tipizaciyi Deyaki movi programuvannya dozvolyayut legko vikoristovuvati znachennya odnogo tipu takim chinom nibi ce znachennya inshogo tipu Inodi ce opisuyetsya yak slabkij tip Aaz Maruh napriklad zauvazhuye sho privedennya tipiv vinikaye koli u vas ye statichno tipizovana mova i vi vikoristovuyete sintaksichni osoblivosti movi shob primusovo vikoristovuvati odin tip yakbi ce buv inshij tip Privedennya tipiv zazvichaj ye simptomom Z inshogo boku peretvorennya stvoryuye absolyutno novij ob yekt vidpovidnogo tipu Inshij priklad GCC opisuye ce yak kalambur tipizaciyi ta poperedzhaye sho ce porushit strogi psevdonimi Thiago Macieira obgovoryuye nizku problem yaki mozhut viniknuti koli nabir tekstiv zmushuye kompilyator robiti nevidpovidni optimizaciyi Prikladiv mov yaki dozvolyayut neyavne privedennya tipiv ale bezpechnim dlya tipiv sposobom ye bagato Do prikladu i C i C dozvolyayut programam viznachati operatori dlya peretvorennya znachennya z odnogo tipu v inshij z chitko viznachenoyu semantikoyu Za umovi koli kompilyator C stikayetsya z takim peretvorennyam vin rozglyadaye operaciyu tak samo yak viklik funkciyi Navpaki peretvorennya znachennya v tip C void nebezpechna operaciya nevidima dlya kompilyatora Pokazhchiki Deyaki movi programuvannya vidobrazhayut vkazivniki yak chislovi znachennya i dozvolyayut koristuvacham vikonuvati arifmetichni diyi nad nimi Inodi ci movi nazivayut slabko tipizovanimi oskilki arifmetika vkazivnikiv mozhe buti vikoristana dlya obhodu sistemi tipiv movi Ob yednannya bez tegiv Dokladnishe Ob yednannya struktura danih Deyaki movi programuvannya pidtrimuyut ob yednannya bez tegiv sho dozvolyaye vidobrazhati znachennya odnogo tipu u viglyadi znachen inshogo tipu Statichna perevirka tipu U statti Luki Kardelli Tipove programuvannya avtor opisuye silnu sistemu tipu yak sistema v yakij vidsutnya mozhlivosti neperevirenoyi pomilki tipu vikonannya V inshomu teksti vidsutnist neperevirenih pomilok chasu vikonannya viznachayut yak bezpeka abo bezpeka tipu Ranni statti Toni Hoara nazivayut cyu vlastivist bezpekoyu Dinamichna perevirka tipu V deyakih movah programuvannya vidsutni statichni perevirki tipiv U bagatoh takih movah legko pisati programi yaki buli b vidhileni bilshistyu statichnih perevirok tipiv Napriklad zminna mozhe zberigati abo chislo abo logichne znachennya false Vazhlivo zvernuti uvagu na te sho deyaki z cih viznachen ye superechlivimi inshi konceptualno nezalezhnimi a treti ye okremimi vipadkami z dodatkovimi obmezhennyami inshih bilsh liberalnih mensh silnih viznachen Cherez veliku rozbizhnist mizh cimi viznachennyami mozhna spiratims na tverdzhennya shodo bilshosti mov programuvannya sho voni abo silno abo slabko tipizovani Napriklad Java Pascal Ada ta C vimagayut shob usi zminni mali ogoloshenij tip i pidtrimuyut vikoristannya yavnih privedennya arifmetichnih znachen do inshih arifmetichnih tipiv Inkoli kazhut sho Java C Ada ta Pascal mayut bilsh suvoru tipizaciyu nizh C ce tverdzhennya jmovirno gruntuyetsya na tomu fakti sho C pidtrimuye bilshe tipiv neyavnih peretvoren a C takozh dozvolyaye yavno navoditi znachennya vkazivnikiv todi yak Java ta Pascal ne Samu Java mozhna vvazhati bilsh zhorstko tipizovanoyu nizh Pascal oskilki metodi uhilennya vid statichnoyi sistemi tipiv u Java kontrolyuyutsya sistemoyu tipiv virtualnoyi mashini Java C i VB NET u comu vidnoshenni podibni do Java hocha voni dozvolyayut vimknuti dinamichnu perevirku tipiv shlyahom yavnogo rozmishennya segmentiv kodu v nebezpechnomu konteksti Sistema tipiv Paskalya bula opisana yak nadto silna oskilki rozmir masivu abo ryadka ye chastinoyu jogo tipu sho robit deyaki zavdannya programuvannya duzhe skladnimi Smalltalk Ruby Python i Self usi strogo tipizovani v tomu sensi sho pomilki vvedennya zapobigayut pid chas vikonannya i voni ne vikonuyut neyavnogo peretvorennya tipiv ale ci movi ne vikoristovuyut statichnu perevirku tipiv kompilyator ne pereviryaye ta ne vikonuye pravila obmezhennya tipu Termin kachinij tip teper vikoristovuyetsya dlya opisu paradigmi dinamichnogo druku sho vikoristovuyetsya movami ciyeyi grupi Vsi movi simejstva Lisp ye strogo tipizovanimi v tomu sensi sho pomilki vvedennya zapobigayutsya pid chas vikonannya Deyaki dialekti Lisp taki yak Common Lisp abo Clojure pidtrimuyut rizni formi deklaracij tipiv a deyaki kompilyatori CMUCL i podibni vikoristovuyut ci deklaraciyi razom iz vivedennyam tipu shob umozhliviti rizni optimizaciyi a takozh obmezheni formi perevirki tipu pid chas kompilyaciyi Standard ML F OCaml Haskell Go ta Rust statichno pereviryayutsya tipami ale kompilyator avtomatichno viznachaye tochnij tip dlya bilshosti znachen Mova asemblera i Forth mozhna sharakterizuvati yak netipizovanu Ne maye perevirki tipiv programist povinen perekonatisya sho dani nadani funkciyam mayut nalezhni tipi Bud yake peretvorennya tipu ye yavnim Div takozhPorivnyannya mov programuvannya Tip danih vklyuchaye bilsh detalne obgovorennya pitan tipizaciyi Proyektuvannya za kontraktom stroga tipizaciya yak neyavna forma kontraktu Latentne tipuvannya Bezpeka pam yati Tipobezpechnist Sistema tipizaciyiPrimitki Cornell University Department of Computer Science 2005 Arhiv originalu za 23 listopada 2015 Procitovano 23 listopada 2015 The Unreasonable Effectiveness of Dynamic Typing for Practical Programs Vimeo 12 veresnya 2013 Procitovano 21 bereznya 2021 a href wiki D0 A8 D0 B0 D0 B1 D0 BB D0 BE D0 BD Cite web title Shablon Cite web cite web a Obslugovuvannya CS1 Storinki z parametrom url status ale bez parametra archive url posilannya Liskov B Zilles S 1974 Programming with abstract data types ACM SIGPLAN Notices 9 4 50 59 CiteSeerX 10 1 1 136 3043 doi 10 1145 942572 807045 Jackson K 1977 Parallel processing and modular software construction Design and Implementation of Programming Languages Lecture Notes in Computer Science 54 436 443 doi 10 1007 BFb0021435 ISBN 3 540 08360 X Aahz Typing Strong vs Weak Static vs Dynamic Procitovano 16 serpnya 2015 Type punning and strict aliasing Qt Blog Qt Blog Procitovano 18 lyutogo 2020 Luca Cardelli Typeful programming Hoare C A R 1974 Hints on Programming Language Design In Computer Systems Reliability ed C Bunyan Vol 20 pp 505 534 InfoWorld 25 kvitnya 1983 Procitovano 16 serpnya 2015 Kernighan Brian 1981 Arhiv originalu za 6 kvitnya 2012 Procitovano 22 zhovtnya 2011 CLHS Chapter 4 Procitovano 16 serpnya 2015 Arhiv originalu za 8 March 2016 Procitovano 16 serpnya 2015