Сыстэма тыпаў

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

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

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

Асноўная мэта сыстэмы тыпаў у мове праграмаваньня — паменшыць верагоднасьць памылак шляхам зьмяншэньня памылак тыпаў. Сыстэма тыпаў вызначае, што ўяўляе сабою памылка тыпу, але яе асноўная мэта — прадухіліць выкананьне функцыі са значэньнямі, для якіх гэтая функцыя ня мае сэнсу.

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

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

Агляд выкарыстаньня

Прыкладам простае сыстэмы тыпаў зьяўляецца сыстэма тыпаў мовы C. Часткі праграмы на C — гэта вызначэньні функцый. Адна функцыя выклікаецца іншай функцыяй.

Інтэрфэйс функцыі зьмяшчае назву функцыі і сьпіс яе парамэтраў. Код выклікаючай функцыі зьмяшчае імя выкліканай функцыі разам зь імёнамі зьменных, якія ўтрымліваюць значэньні для перадачы ёй.

Падчас выкананьня праграмы значэньні зьмяшчаюцца ў часовае сховішча, пасьля чаго выкананьне пераходзіць да кода выкліканай функцыі. Код выкліканай функцыі атрымлівае доступ да значэньняў і выкарыстоўвае іх.

Калі код функцыі чакае цэлае значэньне, але код выкліку перадаў значэньне з плаваючай коскаю, то вынік функцыі будзе мець памылку.

Кампілятар C правярае тыпы аргумэнтаў, перададзеных функцыі. Калі тыпы аргумэнтаў не супадаюць з тыпамі парамэтраў аб’яўленымі пры вызначэньні функцыі, кампілятар выдае памылку або папярэджаньне.

Кампілятар можа таксама выкарыстоўваць тып значэньня для аптымізацыі памяці адведзенае пад значэньне і выбару альгарытмаў для апэрацый са значэньнем. Напрыклад, у многіх кампілятарах C тып даных з плаваючай коскаю прадстаўлены ў 32-бітным фармаце ў адпаведнасьці са спэцыфікацыяй IEEE для лікаў з плаваючай коскаю адзінарнае дакладнасьці. Такім чынам, для апэрацый з данымі гэтага тыпу будуць выкарыстоўвацца спэцыфічныя для мікрапрацэсара апэрацыі з плаваючай коскаю (сумаваньне з плаваючай коскаю, множаньне і г. д.).

Строгасьць абмежаваньняў тыпу і спосаб іх ацэнкі ўплываюць на тыпізацыю мовы. Адна й та апэрацыя можа выконвацца са значэньнямі рознага тыпу у выпадку палімарфізму тыпаў. Рэалізацыя тыпаў даных, такіх як цэлыя лікі ці радкі, у канкрэтных мовах праграмаваньня залежыць ад практычных пытаньняў архітэктуры кампутара, рэалізацыі кампілятара і дызайну мовы.

Асновы

Сыстэмы тыпаў вывучае тэорыя тыпаў.. Мова праграмаваньня павінна мець магчымасьць праверыць тып з выкарыстаньнем сыстэмы тыпаў падчас кампіляцыі або падчас выкананьня. Як выказаўся Марк Мэнас:

Фундамэнтальная праблема тэорыі тыпаў заключаецца ў забесьпячэньні таго, каб праграмы мелі сэнс. Асноўная праблема, выкліканая тэорыяй тыпаў, заключаецца ў тым, што код праграмы можа не да канца адпавядаць укладзенай у яго задуме. Пошукі больш багатых сыстэм тыпаў вынікаюць з гэтага.

Мова праграмаваньня з больш дасканалай сыстэмай тыпаў мае больш дэталёвы набор правілаў, чым базавая праверка тыпаў, але коштам гэтага можа стаць неразьвязальнасьць вывядзеньня тыпу і павелічэньне складанасьці праграмаваньня (праграміст павінен анатаваць код). Цяжка знайсьці дастаткова выразную сыстэму тыпаў, якая б задавальняла ўсім практыкам праграмаваньня.

Кампілятар мовы праграмаваньня можа падтрымліваць залежныя тыпы або сыстэму эфэктаў. Віртуальная «вобласьць» коду можа быць зьвязана з «эфэктам», які апісвае, што ў ёй робіцца, і дазваляе, напрыклад, «выдаць» справаздачу пра памылку. Такім чынам, сымбальная сыстэма тыпаў можа быць сыстэмай тыпу і эфэкту.

Сыстэма тыпаў можа быць убудаванай у кампілятар або вызначацца праграмістам. Перавагі вызначанай праграмістам сыстэмы тыпаў ўключаюць:

• Абстракцыя (або модульнасьць). Тыпы дазваляюць праграмістам працаваць з больш абстрактнымі паняцьцямі, чым біт або байт, не клапоцячыся пра рэалізацыю нізкага ўзроўню. Напрыклад, праграмісты могуць разглядаць радок як набор сымбаляў, а не як просты масіў байтаў. Больш за тое, тыпы дазваляюць праграмістам выяўляць інтэрфэйсы паміж дзьвюма падсыстэмамі любога памеру. Гэта паляпшае лякальнасьць коду — любыя дзьве падсыстэмы могуць камунікаваць паміж сабою ў тэрмінах вызначанага інтэрфэйсу, які застаецца ўзгодненым, нягледзячы на зьмены саміх падсыстэм.
• Дакумэнтацыя. У больш разьвітых сыстэмах тыпаў тыпы могуць служыць формай дакумэнтацыі, якая тлумачыць намеры праграміста.

Перавагі вызначанай кампілятарам сыстэмы тыпаў ўключаюць:

• Аптымізацыя. Статычная праверка тыпаў можа даць карысную інфармацыю падчас кампіляцыі. Напрыклад, калі тып патрабуе, каб значэньне выраўнівалася ў памяці з мультыплікатарам у чатыры байты, кампілятар можа ўжываць больш эфэктыўныя машынныя інструкцыі.
• Бясьпека. Сыстэма тыпаў дазваляе кампілятару выяўляць бессэнсоўны або некарэктны код. Напрыклад, мы можам вылучыць выраз 3 / "Hello, World" як некарэктны, калі правілы не вызначаюць, як дзяліць цэлы лік на радок. Строгая тыпізацыя забясьпечвае большую бясьпеку, але ня можа гарантаваць поўную бясьпеку тыпаў.

Памылкі тыпу

Памылка тыпу ўзьнікае, калі апэрацыя атрымлівае даныя іншага тыпу, чым чакалася. Напрыклад, памылка тыпу можа адбыцца, калі ў код, які дзеліць два цэлыя лікі, перадаецца радок літар замест лікавых даных. Нежаданыя зьявы, як гэта, могуць адбыцца на многіх этапах распрацоўкі праграмы. Такім чынам, у сыстэме тыпаў неабходны сродак для выяўленьня памылак. У некаторых мовах з аўтаматызаваным вывядзеньнем тыпаў, такіх як Haskell, каб дапамагчы ў выяўленьні памылак, ужываецца статычны аналіз коду.

Бясьпека тыпаў спрыяе карэктнасьці праграмы, але заўжды спалучана з рызыкаю, што сама праверка тыпу становіцца неразьвязальнай праблемаю (як у Праблеме прыпынку). У сыстэме тыпаў з аўтаматызаванай праверкай тыпаў праграма можа працаваць некарэктна, але ня мець памылак кампіляцыі. Дзяленьне на нуль зьяўляецца небясьпечнай і некарэктнай апэрацыяй, але характэрная для большасьці моў праверка тыпаў падчас кампіляцыі ня можа яе выявіць. Для сьцьвярджэньня адсутнасьці падобных дэфэктаў звычайна выкарыстоўваюцца іншыя віды фармальных мэтадаў, агульна вядомыя як праграмны аналіз. У якасьці альтэрнатывы дастаткова выразная сыстэма тыпаў, напрыклад, у мовах з залежнымі тыпамі, можа прадухіліць гэтыя віды памылак (напрыклад, выкарыстоўваючы тып ненулявых лікаў). Акрамя таго, тэсціраваньне праграмнага забеспячэньня зьяўляецца практычным сродак пошуку памылак, якія не выяўляе праверка тыпаў.

Праверка тыпаў

Працэс праверкі і кантроля абмежаваньняў тыпаў — праверка тыпаў — можа адбывацца падчас кампіляцыі (статычная праверка) або падчас выкананьня (дынамічная праверка).

Калі спэцыфікацыя мовы патрабуе строгага выкананьня правілаў праверкі тыпаў, больш-менш дазваляючы толькі тыя аўтаматычныя пераўтварэньні тыпаў, якія не губляюць інфармацыю, можна назваць гэты працэс моцнай тыпізацыяй; у іншым выпадку, слабай тыпізацыяй.

Гэтыя тэрміны звычайна маюць адвольнае вызначэньне.

Статычная праверка тыпаў

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

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

Статычная праверка тыпаў для поўных па Т’юрынгу моў па сваёй сутнасьці кансэрватыўная. Гэта значыць, калі сыстэма тыпаў адначасова надзейная (адхіляе ўсе некарэктныя праграмы) і вырашальная (існуе алгарытм, які вызначае, ці правільна тыпізаваная праграма), то яна павінна быць няпоўнай (існуе карэктная праграма, якая таксама будзе адхілена, нават калі яна ня мае памылак выкананьня). Напрыклад, разгледзім праграму, якая зьмяшчае код:

КАЛІ <складаная умова> ТАДЫ
    <нешта зрабіць>
ІНАКШ
    <паведаміць пра памылку тыпу>

Нават калі выраз <складаная умова> заўсёды праўдзіцца, большасьць сродкаў праверкі тыпаў адхіляць праграму як няправільна тыпізаваную, таму што статычнаму аналізатару цяжка (мабыць увогуле немагчыма) вызначыць, што галіна ІНАКШ ня будзе выкананая. Відавочна, статычная праверка тыпаў хутка выяўляе памылкі нават у тых месцах, што выконваюцца зрэдку. Без статычнай праверкі тыпаў нават тэсты са 100% пакрыцьцём коду могуць быць не ў стане знайсьці такія памылкі тыпаў. Тэсты могуць быць неэфэктыўнымі, калі трэба ўлічваць камбінацыю ўсіх месцаў, дзе ствараюцца і выкарыстоўваюцца значэньні.

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

Многія мовы са статычнай праверкай тыпаў маюць сродкі яе абыходу. Некаторыя дазваляюць праграмістам выбіраць паміж статычнай і дынамічнай бясьпекай тыпаў. Напрыклад, гістарычна C# аб’яўляе зьменныя статычна,  але C# 4.0 уводзіць ключавое слова dynamic, якое выкарыстоўваецца для аб’яўленьня зьменных, якія будуць дынамічна правярацца падчас выкананьня.  Іншыя мовы дазваляюць пісаць код, які ня мае бясьпекі тыпаў; напрыклад, у C праграмісты могуць свабодна пераводзіць значэньне паміж любымі двума тыпамі, якія маюць аднолькавы памер, фактычна падрываючы канцэпцыю тыпу.

Дынамічная праверка тыпаў і інфармацыя пра тыпы падчас выкананьня

Дынамічная праверка тыпаў — гэта працэс праверкі бясьпекі тыпаў праграмы падчас выкананьня. Рэалізацыі моў з дынамічнай праверкай тыпаў звычайна зьвязваюць кожны аб’ект часу выкананьня з тэгам тыпу (спасылкаю на тып), які зьмяшчае інфармацыю аб яго тыпе. Гэтая інфармацыя таксама можа быць выкарыстана для рэалізацыі дынамічнага дыспэтчынга, позьняга зьвязваньня, паніжальнага прывядзеньня, рэфлексіўнага праграмаваньня і падобнае функцыянальнасьці.

Большасьць моў зь бясьпекаю тыпаў маюць некаторую форму дынамічнае праверкі тыпаў, нават калі яны таксама маюць статычную праверку тыпаў. Прычына гэтага ў тым, што многія карысныя функцыі цяжка або немагчыма рэалізаваць інакш. Напрыклад, няхай праграма вызначае два тыпы, A і B, дзе B зьяўляецца падтыпам A. Калі праграма спрабуе пераўтварыць значэньне тыпу A у тып B, што вядома як паніжальнае прывядзеньне, то апэрацыя толькі тады магчымая калі значэньне, якое пераўтвараецца, насамрэч зьяўляецца значэньнем тыпу B. Такім чынам, каб пераканацца, што апэрацыя бясьпечная, неабходна дынамічная праверка. Гэтае патрабаваньне зьяўляецца адным з крытычных для паніжальнага прывядзеньня.

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

Мовы праграмаваньня, якія маюць толькі дынамічную праверку тыпаў, часта называюць «дынамічна тыпізаванымі мовамі праграмаваньня».

Спалучэньне статычнае і дынамічнае праверак тыпаў

Некаторыя мовы падтрымліваюць як статычную, так і дынамічную тыпізацыю. Напрыклад, Java і некаторыя іншыя мовы са статычнай тыпізацыяй падтрымліваюць паніжальнае прывядзеньне тыпаў да іх падтыпаў, выяўленьня дынамічнага тыпу аб’екта і іншыя апэрацыі, якія залежаць ад інфармацыі пра тып падчас выкананьня. Іншы прыклад — C++ RTTI. Абагульняючы, большасьць моў праграмаваньня маюць мэханізмы перанакіраваньня паміж рознымі «відамі» даных, такія як дыскрымінальныя аб’яднаньні і палімарфізм часу выкананьня. Нават калі яны не ўзаемадзейнічаюць з анатацыямі тыпу або праверкай тыпу, рэалізацыя такіх мэханізмаў істотна падобныя да рэалізацыі дынамічнае тыпізацыі.

Да аб’ектаў у аб’ектна-арыентаваных мовах звычайна зьвяртаюцца па спасылцы, чый статычны тып (або тып вызначэньня) роўны тыпу аб’екта падчас выкананьня, альбо яго супэртыпу. Гэта адпавядае прынцыпу замяшчэньня Ліскоў, які абвяшчае, што ўсе апэрацыі, якія можна выканаць над асобнікам дадзенага тыпу, таксама могуць быць выкананы над асобнікам падтыпу. Гэтае паняцьце таксама вядомае як палімарфізм падтыпаў. У некаторых мовах падтыпы могуць таксама мець каварыянтныя або інварыянтныя тыпы зваротных значэньняў і тыпы аргумэнтаў адпаведна.

Некаторыя мовы, як Clojure, Common Lisp або Cython дынамічна тыпізуемыя па змаўчаньні, але дазваляюць праграмам уключаць статычную праверку тыпаў праз дадатковыя анатацыі. Што можа выкарыстоўвацца, напрыклад, для аптымізацыя прадукцыйнасьці крытычных разьдзелаў праграмы. Больш фармальны тэрмін — паступовая тыпізацыя. Асяродьдзе праграмаваньня DrRacket (пэдагагічнае асяродьдзе, заснаванае на Lisp) і папярэднік мовы Racket, таксама мае мяккую тыпізацыю.

І наадварот, пачынаючы з вэрсіі 4.0, мова C# дае магчымасьць пазначыць, што зьменная не павінна правярацца статычна. Зьменная тыпу dynamic ня будзе падлягаць статычнай праверцы тыпу. Замест гэтага праграма абапіраецца на інфармацыю аб тыпе часу выкананьня, каб вызначыць, як можна выкарыстоўваць зьменную.

У Rust тып dyn std::any::Any забясьпечвае дынамічную тыпізацыю static тыпаў.

Статычная і дынамічная праверка тыпаў на практыцы

Выбар паміж статычнай і дынамічнай тыпізацыяй патрабуе пэўных кампрамісаў.

Статычная тыпізацыя можа надзейна знаходзіць памылкі тыпу падчас кампіляцыі, што павышае надзейнасьць праграмы. Аднак праграмісты разыходзяцца ў меркаваньнях наконт таго, як часта ўзьнікаюць памылкі тыпу, што прыводзіць да далейшых разнагалосьсяў наконт долі закадзіраваных памылак, якія будуць выяўляцца шляхам адпаведнага прадстаўленьня распрацаваных тыпаў у кодзе. Прыхільнікі статычнае тыпізацыі лічаць, што праграмы больш надзейныя, калі яны прайшлі добрую праверку тыпаў, у той час як прыхільнікі дынамічнае тыпізацыі прыводзяць прыклады надзейнага кода зь невялікай базаю памылак на мовах з дынамічнай тыпізацыяй. Значэньнье статычнае тыпізацыі ўзрастае па меры павелічэньня трываласьці сыстэмы тыпаў. Прыхільнікі залежнае тыпізацыі, рэалізаванай ў такіх мовах, як Dependent ML і Epigram, выказалі здагадку, што амаль усе памылкі можна лічыць памылкамі тыпу, калі тыпы, якія выкарыстоўваюцца ў праграме, правільна аб’яўлены праграмістам або правільна выведзены кампілятарам.

Статычная тыпізацыя звычайна прыводзіць да скампіляванага кода, які выконваецца хутчэй. Калі кампілятар ведае дакладныя тыпы даных (што неабходна для статычнай праверкі праз вызначэньне або вывад), ён можа стварыць аптымізаваны машынны код. Па гэтай прычыне некаторыя мовы з дынамічнай тыпізацыяй, такія як Common Lisp, дазваляюць неабавязковыя дэклярацыі тыпаў для аптымізацыі.

Наадварот, дынамічная тыпізацыя дазваляе кампілятарам працаваць хутчэй, а інтэрпрэтатарам дынамічна загружаць новы код, таму што зьмены ў зыходным кодзе ў мовах з дынамічнай тыпізацыяй прыводзяць да меншай колькасьці праверак і меншага прагляду кода. Што таксама скарачае цыкль праўка-кампіляцыі-тэст-наладка.

Мовы са статычнай тыпізацыяй, у якіх адсутнічае вывядзеньне тыпу (напрыклад, C і Java да вэрсіі 10) патрабуюць дэкляраваньня тыпаў мэтадаў або функцый. Гэта можа служыць дадатковай праграмнай дакумэнтацыяй, якая зьяўляецца актыўнай і дынамічнай, а не статычнай. Мова можа быць статычна тыпізаванаю, не патрабуючы дэклярацый тыпаў (прыклады ўключаюць Haskell, Scala, OCaml, F#, Swift і ў меншай ступені C# і C++) — яўная дэклярацыя тыпу не зьяўляецца абавязковым патрабаваньнем для статычнае тыпізацыі.

Дынамічная тыпізацыя дазваляе канструкцыі, якія немагчымыя пры простай статычнай праверцы тыпаў. Напрыклад, функцыя eval, якая выконвае адвольны радок тэксту як код. Функцыя eval магчымая са статычнай тыпізацыяй, але патрабуе пашыранага выкарыстаньня алгебраічных тыпаў даных. Акрамя таго, пры дынамічнай тыпізацыі прасьцей працаваць з прамежкавым кодам і зьдзяйсьняць прататыпіраваньне, напрыклад, выкарыстоўваць падменныя структуры даных (аб’ект-падманка) замест сапраўдных структур даных (звычайна для экспэрымэнтаў і тэсьціраваньня).

Пры дынамічнай тыпізацыі звычайна магчымая качыная тыпізацыя, што робіць прасьцейшым паўторнае выкарыстаньне коду. Мовы са статычнай тыпізацыяй таксама могуць падтрымліваць качыную тыпізацыю ці іншыя мэханізмы, такія як шаблёны, якія таксама спрашчаюць паўторнае выкарыстаньне коду.

Дынамічная тыпізацыя звычайна палягчае выкарыстаньне мэтапраграмаваньня. Напрыклад, шаблёны C++ звычайна больш грувасткія для напісаньня, чым эквівалентны код Ruby або Python, паколькі C++ мае больш жорсткія правілы адносна вызначэньня тыпаў. Гэта прымушае распрацоўшчыка пісаць больш шаблённага кода, чым гэта патрэбна распакоўшчыку Python. Больш прасунутыя канструкцыі часу выкананьня, такія як мэтаклясы і інтраспэкцыя, часта цяжэй выкарыстоўваць у мовах са статычнай тыпізацыяй. У некаторых мовах такія магчымасьці таксама могуць выкарыстоўвацца, напрыклад, для стварэньня новых тыпаў на месцы на аснове даных часу выкананьня. Такія прасунутыя канструкцыі часта забясьпечваюцца дынамічнымі мовамі праграмаваньня; многія зь іх зьяўляюцца дынамічна тыпізаванымі, хаця дынамічная тыпізацыя неабавязкова зьвязана з дынамічнымі мовамі праграмаваньня.

Моцныя і слабыя тыпізацыя

Асноўны артыкул: Моцная й слабая тыпізацыя

Пры апісаньні мовы праграмаваньня часта ужываюцца тэрміны моцная або слабая тыпізацыя. На самай справе не існуе іх агульнапрынятага вызначэньня. Увогуле, існуюць больш дакладныя тэрміны для адлюстраваньня адрозьненьняў паміж сыстэмамі тыпаў, якія прымушаюць людзей называць іх «моцнымі» або «слабымі».

Бясьпека тыпаў і бясьпека памяці

Трэці спосаб катэгарызацыі сыстэмы тыпаў мовы праграмаваньня — гэта бясьпека апэрацый з тыпізаванымі данымі і пераўтварэньняў. Для апісаньня моў, якія не дазваляюць апэрацыі або пераўтварэньні, якія парушаюць правілы сыстэмы тыпаў, выкарыстоўваецца тэрмін тыпабясьпечная мова.

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

Разгледзім наступную праграму на мове, якая адначасова мае бясьпеку тыпаў і бясьпеку памяці:

var x := 5;
var y := «37»;
var z := x + y;

У гэтым прыкладзе зьменная z будзе мець значэньне 42. Нават калі гэта ня тое, што чакаў праграміст, — гэта дакладна вызначаны вынік. Калі y нельга было б пераўтварыць у лік (напрыклад, «Hello World»), вынік таксама быў бы дакладна вызначаным. Зьвярніце ўвагу, што праграма можа мець бясьпеку тыпаў або бясьпеку памяці і ўсё роўна выходзіць з ладу пры памылковай апэрацыі. Гэта для моў з сыстэмаю тыпаў, якая недастаткова прасунутая, каб дакладна вызначыць законнасьць апэрацый над усімі магчымымі апэрандамі. Але калі праграма сустракае апэрацыю, якая не зьяўляецца тыпабясьпечнаю, спыненьне праграмы часта зьяўляецца адзіным варыянтам.

А зараз разгледзім падобны прыклад на C:

int x = 5;
char y[] = «37»;
char* z = x + y;
printf(«%c\n», *z);

У гэтым прыкладзе z будзе паказваць на адрас памяці на пяць знакаў далей за y, што эквівалентна тром знакам пасьля канцавога нулявога знака радка, на які паказвае y. Зварот да гэтага месца ў памяці нечаканы. У тэрмінах C гэта проста нявызначаныя паводзіны, і праграма можа рабіць што заўгодна; з простым кампілятарам яна сапраўды можа надрукаваць любы байт, які захоўваецца пасьля радка «37». Як паказвае гэты прыклад, C ня мае бясьпекі памяці. Паколькі адвольныя даныя лічацца знакамі, гэта таксама не тыпабясьпечная мова.

Увогуле, бясьпека тыпаў і бясьпека памяці ідуць поруч. Напрыклад, мова, якая падтрымлівае арытмэтыку паказальнікаў і пераўтварэньне ліку ў паказальнік (напрыклад, C), не зьяўляецца ні бясьпечнаю для памяці, ні для тыпаў, таму што дазваляе доступ да адвольнае памяці, як калі б гэта была законная памяць любога тыпу.

Зьменныя ўзроўні праверкі тыпаў

Некаторыя мовы дазваляюць прымяняць розныя ўзроўні праверкі да розных рэгіёнаў кода. Прыклады:

• Дырэктыва use strict у JavaScript і Perl прымяняе больш жорсткую праверку.
• declare(strict_types=1) у PHP актывізуе строгую праверку тыпаў.
• З Option Strict On у VB.NET кампілятар будзе патрабаваць пераўтварэньня паміж аб’ектамі.

Дадатковыя інструмэнты, такія як лінтар і IBM Rational Purify, таксама можна выкарыстоўваць для узмацьненьня строгасьці праверкі тыпаў.

Апцыянальныя сыстэмы тыпаў

У сваёй прапанове Гілад Браха выказаў прыхільнасьць да стварэньня незалежнае ад мовы сыстэмы тыпаў. Сыстэма тыпаў павінна быць модулем, які можна падключыць да мовы па меры неабходнасьці. Ён лічыць, што гэта выгадна, таму што тое, што ён называе абавязковымі сыстэмамі тыпаў, робіць мовы менш выразнымі, а код больш няўстойлівым. Патрабаваньне, каб сыстэма тыпаў не ўплывала на сэмантыку мовы, цяжка выканаць.

Апцыянальная тыпізацыя падобная да паступовае тыпізацыі, але й адрозьніваецца ад яе. У той час як яны абедзьве могуць выкарыстоўвацца для выкананьня статычнага аналізу кода (статычная тыпізацыя), апцыянальная сыстэма тыпаў не забясьпечвае бясьпеку тыпаў падчас выкананьня (дынамічная тыпізацыя).

Палімарфізм і тыпы

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

Спэцыялізаваныя сыстэмы тыпаў

Шмат сыстэм тыпаў выкарыстоўваецца ў пэўных асяродьдзях з пэўнымі тыпамі даных або для статычнага аналізу кода. Часта яны заснаваныя на ідэях фармальнай тэорыі тыпаў і даступныя толькі ў выглядзе прататыпаў.

У наступнай табліцы даецца агляд канцэпцый тэорыі тыпаў, якія выкарыстоўваюцца ў спэцыялізаваных сыстэмах тыпаў. Назовы $M$, $N$, $O$ ахопліваюць тэрмы, а назовы $\sigma$, $\tau$ — тыпы. Будуць выкарыстоўвацца наступныя абазначэньні:

• $M:\sigma$ азначае, што $M$ мае тып $\sigma$;
• $M(N)$ — прымяненьне $M$ на $N$;
• $\tau [\alpha :=\sigma ]$ (адпаведна $\tau [x:=N]$) апісвае тып, які атрымліваецца ў выніку замены ўсіх уваходжаньняў зьменнай тыпу $\alpha$ (адпаведна, зьменнай тэрма $x$) у $\tau$ па тыпу $\sigma$ (адпаведна тэрм $N$).

Тып	Натацыя	Вызначэньне
Функцыянальны	$\sigma \to \tau$	Калі $M:\sigma \to \tau$ і $N:\sigma$, тады $M(N):\tau$.
Здабытак	$\sigma \times \tau$	Калі $M:\sigma \times \tau$, тады $M=(N,O)$ — пара такая, што $N:\sigma$ і $O:\tau$.
Сума	$\sigma +\tau$	Калі $M:\sigma +\tau$, тады $M=\iota _{1}(N)$ — першая іньекцыя такая, што $N:\sigma$, ці $M=\iota _{2}(N)$ — другая іньекцыя такая, што $N:\tau$.
Перасячэньне	$\sigma \cap \tau$	Калі $M:\sigma \cap \tau$, тады $M:\sigma$ і $M:\tau$.
Аб’яднаньне	$\sigma \cup \tau$	Калі $M:\sigma \cup \tau$, тады $M:\sigma$ ці $M:\tau$.
Запіс	$\langle x:\tau \rangle$	Калі $M:\langle x:\tau \rangle$, тады $M$ мае складнік $x:\tau$.
Палімарфічны	$\forall {}\alpha .\tau$	Калі $M:\forall {}\alpha .\tau$, тады $M:\tau [\alpha :=\sigma ]$ для любога тыпу $\sigma$.
Існасьць	$\exists {}\alpha .\tau$	Калі $M:\exists {}\alpha .\tau$, тады $M:\tau [\alpha :=\sigma ]$ для некаторага тыпу $\sigma$.
Рэкурсіўны	$\mu \alpha .\tau$	Калі $M:\mu \alpha .\tau$, тады $M:\tau [\alpha :=\mu \alpha .\tau ]$.
Залежная функцыя	$(x:\sigma )\to \tau$	Калі $M:(x:\sigma )\to \tau$ і $N:\sigma$, тады $M(N):\tau [x:=N]$.
Залежная пара	$(x:\sigma )\times \tau$	Калі $M:(x:\sigma )\times \tau$, тады $M=(N,O)$ пара такая, што $N:\sigma$ і $O:\tau [x:=N]$.
Залежнае перасячэньне	$(x:\sigma )\cap \tau$	Калі $M:(x:\sigma )\cap \tau$, тады $M:\sigma$ і $M:\tau [x:=M]$.
Сямейнае перасячэньне	$\bigcap _{x:\sigma }\tau$	Калі ${\textstyle M:\bigcap _{x:\sigma }\tau }$, тады $M:\tau [x:=N]$ для любога $N:\sigma$.
Сямейнае аб’яднаньне	$\bigcup _{x:\sigma }\tau$	Калі ${\textstyle M:\bigcup _{x:\sigma }\tau }$, тады $M:\tau [x:=N]$ для некаторага $N:\sigma$.

Залежныя тыпы

Залежныя тыпы заснаваны на ідэі выкарыстаньня скаляраў або значэньняў для больш дакладнага апісаньня тыпу іншага значэньня. Напрыклад, $\mathrm {matrix} (3,3)$ можа быць тыпам матрыцы памеру $3\times 3$. Затым мы можам вызначыць правілы тыпізацыі, такія як наступнае правіла для матрычнага множаньня:

$\mathrm {matrix} _{\mathrm {multiply} }:\mathrm {matrix} (k,m)\times \mathrm {matrix} (m,n)\to \mathrm {matrix} (k,n)$

дзе $k$, $m$, $n$ — адвольныя цэлыя дадатныя значэньні. Варыянт ML пад назваю Dependent ML быў створаны на аснове гэтае сыстэмы тыпаў, але паколькі праверка тыпаў для залежных тыпаў неразьвязальная, ня ўсе праграмы могуць быць правераны бяз пэўных абмежаваньняў. Dependent ML абмяжоўвае праверку роўнасьці тыпаў, для вырашэньня якой карыстаецца арытмэтыкай Прэсбургера.

Іншыя мовы, такія як Epigram, робяць значэньні ўсіх выразаў у мове вырашальнымі, каб праверка тыпаў таксама была вырашальнай. Аднак у цэлым доказ разьвязальнальнасьці неразьвязальны, таму многія праграмы патрабуюць карыстальніцкіх анатацый, якія могуць быць вельмі нетрывіяльнымі. Паколькі гэта перашкаджае працэсу распрацоўкі, многія моўныя рэалізацыі маюць опцыі для адключэньня гэтае ўмовы. Коштам гэтага можа стацца, што праграма праверкі тыпаў будзе працаваць ў бясконцым цыкле, калі правяраюцца праграмы, якія ня маюць праверкі тыпаў, што прыводзіць да збою кампіляцыі.

Лінейныя тыпы

Лінейныя тыпы — гэта тыпы такіх значэньняў, якія маюць уласьцівасьць мець адну і толькі адну спасылку на сябе ва ўсе часы. Лінейныя тыпы заснаваныя на тэорыі лінейнае лёгікі і цесна зьвязаныя з унікальнасьцю тыпаў. Яны карысныя для апісаньня вялікіх нязьменных значэньняў, такіх як файлы, радкі і гэтак далей, таму што любая апэрацыя, якая адначасова зьнішчае лінейны аб’ект і стварае падобны аб’ект (напрыклад, str = str + "a"), можа быць аптымізавана нябачна для праграміста зьмяненем проста на месцы. Звычайна гэта немагчыма, бо такія зьмяненьні могуць выклікаць пабочныя эфэкты ў тых частках праграмы, якія зьмяшчаюць іншыя спасылкі на аб’ект, парушаючы празрыстасьць спасылак. Яны таксама выкарыстоўваюцца ў экспэрымэнтальнай апэрацыйнай сыстэме Singularity для міжпрацэснае камунікацыі, статычна гарантуючы, што працэсы ня могуць сумесна выкарыстоўваць аб’екты ў агульнай памяці, каб прадухіліць стан гонкі. Мова Clean (падобная на Haskell) выкарыстоўвае гэтую сыстэму тыпаў, каб атрымаць вялікую хуткасьць (у параўнаньні з выкананьнем глыбокага капіраваньня), застаючыся ў бясьпечнай.

Тыпы-перасячэньні

Тыпы-перасячэньні — гэта тыпы, якія апісваюць значэньні, якія належаць адразу абодвум іншым дадзеным тыпам зь перакрытымі наборамі значэньняў. Напрыклад, у большасьці рэалізацый C сымбаль са знакам мае дыяпазон ад −128 да 127, а сымбаль бяз знака — дыяпазон ад 0 да 255, таму тып-перасячэньне гэтых двух тыпаў будзе мець дыяпазон ад 0 да 127. Такі тып можа быць бясьпечна перададзены ў функцыі, якія чакаюць сымбаль са знакам або бяз знака, таму што ён сумяшчальны з абодвума тыпамі.

Тыпы-перасячэньні карысныя для апісаньня тыпаў перагружаных функцый: напрыклад, калі «int → int» — гэта тып функцыі, якая прымае цэлы лік і вяртае цэлы лік, а «float → float» — гэта тып функцыі, якая прымае аргумэнт тыпу float і вяртае float, тады перасячэньне гэтых двух тыпаў можа выкарыстоўвацца для апісаньня функцый, якія выконваюць тое ці іншае, у залежнасьці ад таго, з аргумэнтам якога тыпу, яны былі выкліканы. Такая функцыя можа быць перададзена ў іншую функцыю, якая строга прымае функцыю тыпу «int → int»; код для «float → float» проста ня будзе выконвацца.

У герархіі падклясаў перасячэньне тыпу зь яго тыпам продкам (напрыклад, яго бацькоўскім тыпам) — самы вытворны тып. Перасячэньне роднасных тыпаў (з агульным тыпам продкам) — пустое.

Мова Forsythe мае рэалізацыю тыпаў-перасячэньняў. Абмежаваная форма — рафінаваныя тыпы.

Тыпы-аб’яднаньні

Тыпы-аб’яднаньні — гэта тыпы, якія апісваюць значэньні, якія адносяцца да любога з двух тыпаў. Напрыклад, у C сымбаль са знакам мае дыяпазон ад −128 да 127, а сымбаль бяз знака — дыяпазон ад 0 да 255, таму аб’яднаньне гэтых двух тыпаў будзе мець агульны «віртуальны» дыяпазон ад −128 да 255, які можа выкарыстоўвацца часткова ў залежнасьці ад таго, да якога складніка аб’яднаньня зьвяртаюцца. Любая функцыя, якая прымае даныя гэтага тыпу-аб’яднаньня, павінна працаваць карэктна з цэлымі лікамі ў гэтым поўным дыяпазоне. У больш агульным пляне — адзіныя дапушчальныя апэрацыі над тыпам-аб’яднаньнем — гэта апэрацыі, якія дапушчальныя для ўсіх тыпаў у складзе аб’яднаньня адразу. Канцэпцыя «union» ў C падобная да тыпаў-аб’яднаньняў, але не зьяўляецца бясьпечнай для тыпаў, паколькі дазваляе апэрацыі, якія дапушчальныя для любога тыпу, а не для ўсіх. Тыпы-аб’яднаньні важныя ў праграмным аналізе, дзе яны выкарыстоўваюцца для прадстаўленьня сымбалічных значэньняў, дакладная прырода якіх (напрыклад, значэньне або тып) невядомая.

У герархіі падклясаў аб’яднаньне тыпу зь яго тыпам продкам (напрыклад, яго бацькоўскім тыпам) зьяўляецца тыпам продкам. Аб’яднаньне роднасных тыпаў (тыпаў з агульным продкам) зьяўляецца падтыпам іх агульнага продка (гэта значыць, усе апэрацыі, дазволеныя для іх агульнага продка, дазволеныя для тыпу-аб’яднаньня, але яны таксама могуць мець іншыя агульныя апэрацыі).

Тыпы-існасьці

Тыпы-існасьці часта выкарыстоўваюцца ў сувязі з тыпамі запісаў для прадстаўленьня модуляў і абстрактных тыпаў даных з-за іх здольнасьці адьдзяляць рэалізацыю ад інтэрфэйсу. Напрыклад, тып $T=\exists X\langle a:X;f:(X\to int);\rangle$ апісвае інтэрфэйс модуля, які мае элемэнт з імем $a$ тыпу $X$ і функцыю з імем $f$, якая прымае парамэтар таго жа тыпу $X$ і вяртае цэлы лік. Што можа быць рэалізавана рознымі спосабамі; напрыклад:

• $intT=\langle a:int;f:(int\to int);\rangle$
• $floatT=\langle a:float;f:(float\to int);\rangle$

Абодва гэтыя тыпы зьяўляюцца падтыпамі больш агульнага тыпу-існасьці $T$ і адпавядаюць канкрэтным тыпам рэалізацыі, таму любое значэньне аднаго з гэтых тыпаў таксама зьяўляецца значэньнем тыпу $T$. Калі значэньне $t$ мае тып $T$, мы ведаем, што $t.f(t.a)$ добра тыпізаваны, незалежна ад таго, чым зьяўляецца абстрактны тып $X$. Што дае гібкасьць для выбару тыпаў, прыдатных для канкрэтнае рэалізацыі, у той час як кліенты, якія выкарыстоўваюць толькі значэньні тыпу інтэрфэйсу — тыпу-існасьці — ізаляваны ад гэтага выбару.

Увогуле, праграма праверкі тыпаў ня можа зрабіць выснову, да якога тыпу-існасьці належыць дадзены модуль. У прыведзеным вышэй прыкладзе $intT=\langle a:int;f:(int\to int);\rangle$ таксама можа мець тып $\exists X\langle a:X;f:(int\to int);\rangle$. Самае простае рашэньне — анатаваць кожны модуль яго прызначаным тыпам, напрыклад:

• $intT=\langle a:int;f:(int\to int);\rangle$ як $\exists X\langle a:X;f:(X\to ;int);\rangle$

Нягледзячы на тое, што абстрактныя тыпы даных і модулі былі рэалізаваны ў мовах праграмаваньня даволі даўно, толькі ў 1988 годзе Джон С. Мітчэл і Гордан Плоткін стварылі фармальную тэорыю пад лёзунгам: «Абстрактныя тыпы [даных] зьяўляюцца тыпамі-існасьцямі». Тэорыя ўяўляе сабою тыпізаванае лямбда-злічэньне другога парадку, падобнае да сыстэмы Эф, але з квантыфікацыяй існаваньня замест унівэрсальнай.

Паступовая тыпізацыя

У сыстэме тыпаў з паступовай тыпізацыяй зьменным можа быць прысвоены тып альбо падчас кампіляцыі (статычная тыпізацыя), альбо падчас выкананьня (дынамічная тыпізацыя). Гэта дазваляе выбіраць любую парадыгму тыпізацыі карыстаючыся адной моваю. Для прадстаўленьня статычна невядомых тыпаў выкарыстоўваецца спэцыяльны тып пад назваю дынамічны. Паступовая тыпізацыя замяняе паняцьце роўнасьці тыпаў новай залежнасьцю, званай узгодненасьцю, якая суадносіць дынамічны тып з кожным іншым тыпам. Адносіны ўзгодненасьці сімэтрычныя, але не пераходныя.

Яўная або няяўная дэклярацыя й вывад

Многія статычныя сыстэмы тыпаў, такія як у C і Java, патрабуюць дэклярацыі тыпаў — праграміст павінен яўна зьвязаць кожную зьменную з пэўным тыпам. Іншыя, такія як у Haskell, выконваюць вывядзеньне тыпаў: кампілятар робіць высновы аб тыпах зьменных на аснове таго, як яны выкарыстоўваюцца. Напрыклад, дадзена функцыя f(x, y), што сумуе x і y, кампілятар можа зрабіць выснову, што x і y павінны быць лікамі, бо сумаваньне вызначана толькі для лікаў. Такім чынам, любы зварот да f дзе-небудзь яшчэ ў праграме, дзе ў якасьці аргумэнта вызначаны нялікавы тып (напрыклад, радок або сьпіс), будзе сыгналізаваць пра памылку.

Лікавыя і радковыя канстанты і выразы ў кодзе могуць і часта азначаюць тып у пэўным кантэксьце. Напрыклад, выраз 3.14 можа мець на ўвазе тып з плаваючай коскаю, а [1, 2, 3] — сьпіс цэлых лікаў, звычайна, масіў.

Вывядзеньне тыпу наогул магчыма, калі яно разьвязальнае ў пэўнай сыстэме тыпаў. Больш за тое, нават калі вывядзеньне неразьвязальнае ў цэлым для дадзенае сыстэмы тыпаў, яно часта магчымые для вялікага мноства рэальных праграм. Сыстэма тыпаў Haskell, вэрсыя сыстэмы тыпаў Хіндлі-Мілнера, зьяўляецца абмежаваньнем сыстэмы Эф-Амэга да так званых паліморфных тыпаў рангу 1, у якіх вывад тыпу вылічальны. Большасьць кампілятараў Haskell дазваляюць палімарфізм адвольнага рангу ў якасьці пашырэньня, але гэта робіць вывад тыпаў невылічальным. (Аднак праверка тыпаў вырашальная, і праграмы першага рангу па-ранейшаму маюць вывад тыпаў; паліморфныя праграмы больш высокага рангу адхіляюцца, калі ім не дадзены відавочныя анатацыі тыпаў.)

Праблемы вырашэньня

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

• Маючы тыпавае асяродьдзе $\Gamma$, тэрм $e$, і тып $\tau$, вырашыць, ці тэрму $e$ можна прысвоіць тып $\tau$ у тыпавым асяродьдзі $\Gamma$.
• Маючы тэрм $e$, вырашыць, ці існуе тыпавае асяродьдзе $\Gamma$ і тып $\tau$ такія, што тэрму $e$ можна прысвоіць тып $\tau$ у тыпавым асяродьдзі $\Gamma$ .
• Маючы тыпавае асяродьдзе $\Gamma$ і тып $\tau$, вырашыць, ці існуе тэрм $e$ якому можна прысвоіць тып $\tau$ у тыпавым асяродьдзі $\Gamma$.

Уніфікаваныя сыстэмы тыпаў

Некаторыя мовы, такія як C# або Scala, маюць уніфікаваныя сыстэмы тыпаў. Гэта значыць, што ўсе тыпы C#, уключаючы прымітыўныя тыпы, спадкуюць ад адзінага каранёвага аб’екта. Кожны тып у C# спадкуе ад клясы Object. Некаторыя мовы, такія як Java і Raku, маюць каранёвы тып, але таксама маюць прымітыўныя тыпы, якія не зьяўляюцца аб’ектамі. Java забясьпечвае тыпы аб’ектаў-абгортак, якія існуюць разам з прымітыўнымі тыпамі, таму распрацоўшчыкі могуць выкарыстоўваць альбо тыпы аб’ектаў-абгортак, альбо больш простыя неаб’ектныя прымітыўныя тыпы. Raku аўтаматычна пераўтварае прымітыўныя тыпы ў аб’екты пры доступе да іх мэтадаў.

Сумяшчальнасьць: эквівалентнасьць і падтыпы

Сродак праверкі тыпаў для мовы са статычнай тыпізацыяй павінен пераканацца, што тып любога выразу адпавядае тыпу, чаканаму кантэкстам, у якім гэты выраз зьяўляецца. Напрыклад, у прызначэньні формы x := e, выведзены тып выразу e павінен адпавядаць заяўленаму або выведзенаму тыпу зьменнай x. Гэта паняцьце ўзгодненасьці, якое называецца сумяшчальнасьцю, характэрнае для кожнае мовы праграмаваньня.

Калі тыпы e і x аднолькавыя і для гэтага тыпу дазволена прызначэньне, то гэта правільны выраз. Такім чынам, у найпростых сыстэмах тыпаў пытаньне аб сумяшчальнасьці двух тыпаў зводзіцца да таго, ці роўныя яны (ці эквівалентныя). Розныя мовы, аднак, маюць розныя крытэрыі вырашэньня таго, ці два выразы тыпу адпавядаюць аднаму тыпу. Усе гэтыя розныя крытэрыі можна зьвесьці да двух крайніх выпадкаў, якімі зьяўляюцца структурная тыпізацыя, пры якой тыпы з аднолькавай структурай эквівалентныя, і намінатыўная тыпізацыя, пры якой тыпы роўныя толькі тады, калі яны маюць аднолькавае «імя».

У мовах з падтыпамі вырашэньне сумяшчальнасьці больш складанае: калі B зьяўляецца падтыпам A, то значэньне тыпу B можа выкарыстоўвацца ў кантэксьце, дзе чакаецца значэньне тыпу A (каварыяцыя), нават калі адваротнае немагчыма. Як і эквівалентнасьць, адносіны падтыпу вызначаюцца па-рознаму для кожнае мовы праграмаваньня з мноствам магчымых варыяцый. Наяўнасьць парамэтрычнага або спэцыяльнага палімарфізму ў мове таксама можа паўплываць на сумяшчальнасьць тыпаў.