Систем типова

У програмским језицима, систем типова је збирка правила који додељује правилно названи тип различитим конструкцијама програма од кога се састоји, као што су променљиве, експресије, функције или модули. Главна сврха система типизирања је да смањи могућности за багове у рачунарским програмима дефинисањем сучеља између различитих делова компјутерског програма, и онда да провери да ли су делови повезани на доследан начин. Ова провера се може десити статично (при компилираном времену), динамично (при рантајму), или као комбинација статичке и динамичке провере. Системи типизирања имају остале сврхе такође, као што је омогућавање одређених оптимизација компилатора, дозвола за вишеструку опрему, пружање форме документације, итд.

Систем типизирања сарађује са типом од сваке израчунате вредности и, провером протока ових вредности, покушава да осигура или докаже да се ниједна грешка у типизирању неће појавити. Посебни систем типизирања у питању одлучује тачно шта чини грешку типизирања, али углавном циљ је да се спрече операције од којих се очекује одређени тип вредности који користи вредности за које те операције немају смисла (логичке грешке); грешке меморије ће такође бити спречене. Системи типизирања су често део програмских језика, и уграђени у интерпретаторе и компилаторе; иако систем типизирања језика може бити надограђен опционим алаткама који одрађују додатне врсте провере користећи се оригиналном синтаксом језика или граматиком.

Преглед употребе

Пример једноставног система типова се налазу у С језику. Делови С програма су дефиниције функција. Једна функција је позвана другом функцијом. Сучеље функције наводи име функције и листу вредности које се прослеђују до кода функције. Код позване функције наводи име позваног, заједно са именима променљивих који чувају вредности да би га проследили. Током извршења, вредности су стављење у привремено складиште, онда извршење скочи до кода позване функције. Код позване функције приступа вредностима и користи их. Ако су инструкције унутар функције исписане са претпоставком да примају целобројну вредност, али позвани код је проследио децималну вредност, онда ће нетачни резултат бити израчунат од стране позване функције. С компилатор проверава декларисани тип за сваку послату променљиву, против декларисаног типа за сваки променљиву у сучељу позване функције. Ако типови нису исти, компилатор избацује грешку.

Компилатор може такође користити статички тип вредности да оптимизује складиште које му је потребно и избор алгоритама за операције над вредностима. У многим С компилаторима децимални тип података, на пример, је представљен у 32 бита, у сагласности са IEEE 754. Они ће тако користити специфичну-децималну-тачку скупа операција над тим вредностима (адиција децималне-тачке, множење, итд. ).

Дубина типа ограничења и манир њихове процене утиче на типизирање језика. Програмски језик може даље помагати операцији са различитим конкретним алгоритмима над сваким типом у случају типа полиморфизма. Теорија типизирања је студија система типизирања, иако конкретни системи типизирања програмских језика потичу од делова проблема компјутерске архитектуре, компилаторске имплементације, и дизајна језика. 

Основе

Формално, теорије типизирања проучавају системе типизирања. Програмски језик мора имати догађај да би проверио типизирање користећи се системом типизирања или при компилаторском времену или рантајму, ручно забележен или аутоматски закључен. Као што је Марк Манасе рекао:

Додела типа података—типизирање— даје значење секвенцама битова као што је вредност у меморији или неки објекат као што је променљива. Хардвер рачунара генералне сврхе није у могућности да разлике између на пример меморијске адресе и инструкциског кода, или између карактера, целог броја, или децималне тачке, зато што га не чини унутрашњу разлику између било које могуће вредности које би секвенце битова могле да "значе"". Повезивање секвенци битова са типом преноси то значење хардверу како би се формирао симболични систем сачињен од хардвера и неког програма.

Програм потпомаже свакој вредност са најмање једним одређеним типом, али се такође може стартовати једну вредност која је повезана са многох подтиповима. Други ентитети, као што су објекти, модули, канали комуникације, зависности могу се повезати са типизирањем. Чак и типизирање се може повезати са типизирањем. Имплементација система типизирања може у теорији повезати идентификације назване тип података (тип вредности), класа (тип објектна), и врста (тип типа, или метатип). Ово су апстракције кроз које типизирање пролази, над хијерархијом нивоа који се налазе у систему.

Када програмски језик укључује разрађен систем типизирања, добија фино зрнастији сет правила од класичне провере типизирања, али ово долази по са ценом да када закључци типизирања (и остале особине) постану неодлучив задатак, и када више пажње мора да се посвети од стране програмера да забележи код или да размотри операције које се односе на рачунар и функционисање. Изазов је наћи  довољно изражајан систем типизирања који задовољава све вежбе програмирања  у маниру сигурног типизирања.

Што је више рестрикција типизирања наметнуто од стране компилатора, биће јаче укуцан програмски језик. Јако укуцани језици често захтевају од програмера да направе екплицитне конверзије у контексту где имплицитна конверзија не би шкодила. Паскалов систем типизирања је описан као "прејак" зато што, на пример, величина низа или ниске је део типизирања, што чини неки програмерски задатак тешким. Хаскел је такође јако укуцан али његова типизирања су аутоматски закључена тако да су експлицитне конверзије често (али не и увек) беспотребне.

Компилатор програмског језика може такође имплементовати зависно типизирање или ефектни систем, што омогућава још програмских спецификација који треба да буду потврђени од стране контролора типизирања. Осим једноставних вредности-типизирања парова, виртуелни "регион" кода сарађује са "ефектном" компонентом описујући шта је урађено са чим, и дозвољавајући на пример да се "одбаци" извештај грешке. Тако симболични систем може бити систем типизирања и ефекта, што чини сигурнију проверу него самосталну проверу. 

Да ли је аутоматизован од стране компилатора или спецификован од стране програмера, систем типизирање чини понашање програма илегалним што је ван правила система типизирања. Предности које су пружене од стране програмера укључују : 

• Апстракција (или модуларност) – типизирања која омогућују програмерима да размишљају на вишем нивоу од бита или бајта, недосађујући се са ниско-нивоим имплементацијама. На пример, програмери могу почети да размишљају о ниски као п збирци карактера вредности уместо као чист низ бајтова. Високо идаље, типизирања омогућавају програмерима да размишљају и да изразе сучеља између било која два подсистема. Ово омогућава више нивоа локализације тако да захтеване дефиниције за компатибилност подсистема остају доследне када та два подсистема комуницирају.
• Документација– У изражајнијим типовима типизирања, типизирање може служити као форма документације која разјашњава намеру програмера. На пример, ако програмер декларише функцију као поврато време типизирања, ово документује функцију када временско типизирање може бити екпслицитно декларисано дубље у коду да би постао целобројни тип.

Предности које пружа компилатор система типизирања укључују:

• Оптимизација – Статични тип провере типизирања може пружити корисну комплитаорску информацију. На пример, ако тип захтева да вредност мора бити поравната у меморију као дељив са четири бајта, компилатор може бити у могућности да користи ефикацније инструкције машина.
• Сигурност – Систем типизирања омогућује компилатору да детектује нејасноће или вероватно нетачни код. На пример, можемо идентификовати експресију 3 / "Hello, World" као нетачну, када правила не говоре како да поделимо цео број са ниском. Јако типизирање пружа већу сигурност, али не може гарантовати комплетну сигурност у типизирању.

Сигурносту  у типизирању доприносу програмској тачности, али може гарантовати само тачност на рачун прављења провере типизирања неодлучивог задатка. У систему типизирања са аутоматском провером типизирања програм се може показати да ради нетачно иако је укуцан сигурно, и да не пружа компилторске грешке. Дељење нулом је несигурна и нетачна операција, али контролор типизирања ради само на компилаторском времену који не скенира за дељење нулом у многим програмским језицима, и онда остаје као рантајм грешка. Да би се доказало одсуство ових више-генералних-него-куцаних дефекта, других типова формалних метода, колективно познатих као програмске анализе, се често користе. Алтернативно, довољно експресивни систем типизирања, као у зависним језицима типизирања, може спречити овде типове грешака (на пример, изражавајући "тип не-нултих борјева" ). Као додатак софтверско тестирање је емпирични метод за проналажење грешака које контролор типизирања не може наћи.

Провера типизирања

Процес потврде и спровођења ограничења типизирања – провера типизирања –може се десити или при компилираном времену (статичка провера) или рантајм (динамчка провера). Ако језичка спецификација тражи јако типизирање правила (тј, више или мање дозвољава само оне аутоматске конверзије типизирања које не губе информацију), један може да се односи на процес као јако искуцан, ако не, онда слабо искуцан. Термини се не користе често буквално. 

Статичка провера типизирања

Статичка провера типизирања је процес провере сигурности типизирања програма базираног на анализи програмског текста (изворног кода). Ако програм прође контролора типизирања, онда програм гарантује да задовољи неки скуп карактеристика сигурнусног типизирања за могуће уносе.

Због тога што статичка провера типизирања оперише над текстом програма, то дозвољава многим баговима да буду ухваћени раније у циклусу развитка.

За статичну проверу типизирања може се сматрати као ограничена форма верификације програма (видети сигурно типизирање). У језику сигурног типизирања, за статичну проверу типизирања се такође може сматрати као оптимизација. Ако компилатор може да докаже да је програм добро откуцан, онда не мора да емитује динамичке провере сигурности, што дозвољава бинарном компилираном резултату да ради брже.

Статичка провера типизирања за Тјурингову-комплетност језика је инхерентно конзервативна. То је, ако је систем типизирања и звук (значи да одвија све нетачне програме) и  одлучив (значи да је могуће написати алгоритам који одлучује да ли је програм добро откуцан), онда увек ће бити могуће да се дефинише програм који је добро откуцас али који не задовољава контролора типизирања. На пример, размотрити програм који садржи овај код:

if <complex test> then <do something> else <generate type error>

Чак иако експресија <complex test> увек има вредност true при рантајму, већина контролора типизирања ће одбити програм као лоше укуцан, зато што је тешко (ако не и немогуће) за статички анализатор да одлучи да ли else грана неће бити узета. С друге стране, статични контролор типизирања ће брзо детектовати грешке типизирања у ретко коришћеним путевима кода. Без статичке провере типизирања, чак и тестови покривености кода са 100% покривеношћу можда неће бити у могућности да пронађу овакве грешке. Тестови можда неће успети да детектују овакве грешке, зато што комбинација свих места где су вредности креиране и свих места где је одређена вредност коришћена мора бити узета у обзир.

Број корисних и честих карактеристика порграмског језика не може бити проверен статички, као што може даункестинг. Због тога, многи језици ће имати и статичку и динамичку проверу типизирања; статички контролор типизирања проверава шта може, и динамички провера остатак.

Многи језици са статичком провером типизирања пружају начин да заобиђу контролора типизирања. Неки језици дозвољавају програмерима да бирају између статичке и динамичке сигурност типизирања. На пример, С# прави разлику између "статички-укуцаних" и "динамички-укуцаних" променљивих; бивша коришћења су проверена статички, док су каснија коришћења  проверена динамички. Други језици дозвољавају корисницима да запишу код који није сигурно-укуцан. На пример, у С-у, програмери могу слободно убацити вредност између било која два типа који имају исту величину. 

За листу језика са статичком провером типизирања, видети категорија за статички укуцане језике.

Динамичка провера типизирања и рантајм тип информација

Динамичка провера типизирања је процес провере сигурности типизирања програма при рантајму. Имплементације динмачко проверених језика типизирања углавном сарађују при сваком рантајм објекту са "тип" тагом (тј., референца за типизирање) садржећи своје информације типизирања. Овај рантајм тип информације (РТТИ) се може такође користити за имплементовање динамичне опреме, касног везивања, даункестинга, рефлексије, и сличних карактеристика.

Многи језици сигурносног типизирања укључују неку форму динамине провере типизирања, иако имају статичног контролора типизирања. Разлог за ово је тај да многе корисне карактеристике или особине је тешко или немогуће потрврдити статично. На пример, претпоставити да програм дефинише два типа, А и Б, где је Б подтип А. Ако програм покуша да конвретује вредност типа А у тип Б, што је познато као даункестинг, онда је операције легална само ако је конвертована вредност стварна вредност типа Б. Због тога, диначна провера је потребна како би се проверило да ли је операција сигурна; ова захтевност је једна од критика даункестинга.

По дефиницији, динамична провера типизирања може изазвати програм да не успе при рантајму. У неким програмским језицима, могуће је учестовати и повратити се из ових падова. У другим, грешке провере типизирања се сматрају фаталним.

Програмски језици који укључују динамичну проверу типизирања али не и статичну проверу типизирања се често називају "динамчно-укуцани програмски језици". За листу таквих језика, погледати категорију за динмачно укуцане програмске језике.

Комбиновање статичне и динамчне провере типизирања

Неки језици дозвољавају и статично и динамчно типизирање (провере типизирања) често званим меканим типизирањем. На пример, Јава и неки други привидно статични куцани језици подржавају даункестинг тип за њихове подтипове, упитивање објекта како би се открио динамично типизирање, и друге операције типизирања које зависе на тип рантајм информације. Општије, многи програмски језици укључују механизме за отпрему над различитим "типовима" података, као што су раздовјени савези, подтипови полиморфизма, и варијанте врсте. Иако се не интерагује са анотацијама типизирања или проверама типизирања, овакви механизми су материјално слични динамичним имплементацијама типизирања. Видети програмски језици за више дискусија о интеракцијама измађу статичног и динамичног типизирања. 

Објектима у објектно оријентисаним језицима се обично приступа преко референци чији је статички тип мете (или тип манифестовања) једнак или објектном рантајм типу (његовом типу латента) или његовом супертипизирању. Ово је правилно по Лисковом принципу супституције, која каже да све операције извршене над инстанцом датог типизирања се могу такође извршити над инстанцом подтипизирања. Овај концепт је такође познат као стапање. У неким језицима подтипизирање може такође поседовати коваријантна или контраковаријантна повратна типизирања и аргументована типизирања односно. 

Одређени језици, на пример Clojure, Common Lisp, или Cython су динамично проверени по дифолту, али дозвољава програмима да пређу и статичну проверу типизирања пружајући опционалне анотације. Један разлог за коришћење оваквих помоћи би био да се оптимизује перформанс критичних секција програма. Ово је формализовано постепеним типизирањем. Програмско огружење DrScheme, педагошко окружење базирано на Lisp-у, и претходних језика Racket је такође мекано-куцан. 

С друге стране, као у верзије 4.0, #С језик пружа начин да покаже да променљива не би требало да буде статично проверена. Променљива чији је типdynamic неће бити тема статичној провери типизирања. Стога, програм се ослања на рантајм информацији типизирања да одлучи како се променљива може користити.

Статична и динамична провера типизирања у пракси

Избор између статичног и динамично типизирања захтева одређене компримисе.

Статично типизирање може начи грешке при типизирању ослањајући се на компилаторско време, што би требало да повећа поузданост принетог програма. Међутим, програмери се не слажу око тога колико се често грешке при типизирању јављају, што резултује у даљим неслагањима око односа ових багова који су кодирани да ће бити ухваћени адекватно представљајући пројектована укуцавања у коду. Статично типизирања заговара веровање да су програми поузданији када им је добро проверено типизирање, док динамично типизирање заговара на дистрибуиране кодова за које је доказано да су поуздани и за мале багове база података.. Вредност статичног типизирања, онда , вероватно расте као што се јачина система типизирања повећава. Заговорници зависно куцаних језика као што је Dependent ML и Епиграм  су предложили да скоро сви багови се могу сматрати грешкама типизирања, ако су типизирања коришћена у програму добро декларисана од стране програмера или тачно закључена од стране компилатора. 

Статично типизирање обично резултује компилираном коду који се извршава доста брже. Када компилатор зна тачан тип података који се користи, може да проиведе оптимизован машински код. Даље, компилатори за статично укуцане језике могу начи пречице асемблера много лакше. Неки динамично укуцани језици као што је Common Lisp дозвољавају опционалне декларације типизирања за оптимизацију због овог разлога. Статично типизирање чини ово прожетим. Видети оптимизацију.

Супротно, динамично типизирање може дозволити компилаторима да раде много брже и да дозволи интерпретаторима да динамично учитају нови код, пошто промене изворног кода у динамчно куцаним језицима могу резултовати мањом провером за рад и мање кода да се понавља. Ово може такође смањити измени-компилирам-тестирај-дебагуј круг.

Статично укуцани језици којима фали укуцани закључак (као што је С и Јава) захтева да програмери декларишу типизирања која сматрају методом или функцијом за коришћење. Ово може служити као додатна документација програма, коју компилатор неће дозволити програмеру да игнорише или да дозволи да се изостави из синхронизације. Међутим, језик може бити статичн укуцан без захтева декларација типизирања (примери укључују Haskell, Скалу, OCaml, F# и у мањој мери С# и С++ ), тако да експлицитно типизирање декларације није потребан захтев за статично типизирање у свим језицима.

Динамично типизирање даје конструкцију коју неки статични контролери типизирања не би одбили као илегалне. На пример, eval фунцкије, који извршавају произвољан податак као код, постају могући. Eval функција је могућа статичним типизирањем, али захтева напредна коришћења алгебарских типова података. Даље, динамично типизирање боље се прилагођава прелазном транзиционалном коду и прототипизирању, као што је дозвољавање чувару структуре података (лажни објекат) да буде транспарентно коришћен уместо пуном покривеном структуром података (обично за сврхе експериментисања и тестирања).

Динамично типизирање дозвољава дак типизирање (што омогућава лакшу поновну употребу кода). Многи језици са статичним типизирањем такође имају дак типизирање или друге механизме као генерично програмирање који такође омогућава лакшу поновну употребу кода.

Динамично типизирање чини матапрограмирање лакшим за коришћење. На пример, С++ шаблони су типично гломазнији за типизирање него еквиваленти Рубијевог или Пајтоновог кода. Напредније рантајм конструкције као што су метакласе и самоиспитивање су често много теже за коришћење у статично укуцаним језицима. У неким језицима, овакве карактеристике се могу такође користити тј. да генеришу нове типове и понашања при лету, базираним на рантајм подацима. Овакве напредне конструкције су често пружене динамичним програмским језицима; многи од ових су динамчно укуцани, иако је нема потреба да динамчно типизирање буде у односу да динамично програмираним језицима.

"Јаки" и "слаби" системи типизирања

Језици се често колоквијално односе као "јако укуцани" или "слабо укуцани". У ствари, не постоји универзално прихваћена дефиниција шта ови термини значе. Углавном, постоје прецизнији термини који представљају разлику између система типизирања који су довели људе да их назову "јаким" или "слабим". 

Сигурносно типизирање и сигурносна меморија

Трећи начин категоризовања система типизирања програмских језика користи сигурност укуцаних операција и конверзија. Рачунарски научници сматрају језик "сигурно-укуцаним" ако не дозвољава операције или конверзије које крше правила система типизирања.

Неки посматрачи користе термин меморијски-сигуран језик (или само сигуран језик) да опишу језика који не дозвољавају програмима да приступе меморији која није приписана за њихово коришћење. На пример, меморијски-сигуран језик је проверити границе низа, или ће статично гарантовати (тј., при компилираном времену пре егзекуције) да ће ако тај низ изађе из граница низа проузроковати компилирано-време и можда рантајм грешке.

Размотрити следећи програм језика који је и сигурносно-укуцан и меморијски-сигуран:

var x := 5;
var y := "37";
var z := x + y;

У овом примеру, променљива z ће имати вредност 42. Иако ово можда неће бити оно што је програмер планирао, то је добро дефинисан резултат. Ако је y другачији стринг, онај који не би могао да се пребаци у број (нпр. "Hello World"), резултат био био добро дефинисан такође. Имати на уму да програм може бити сигурно-откуцан или меморијски-сигуран и идаље да се заустави при невладиној операцији; у ствари, ако програм стартује операцију која није сигурносно-откуцана, гашење програма је често једина опција. Сада размотрити сличан пример у С-у:

int x = 5;
char y[] = "37";
char* z = x + y;

У овом примеру z ће показати на адресу меморије пет карактера изнад y, једнако са три карактера после извршења нултог карактера стринга који је показан од странеy. Ово је меморија за коју се не очекује да ће програм приступити. Може садржати небитне податке, и сигурно не садржи нешто корисно. Како овај пример показује, С није ни меморијски-сигуран нити је сигурносно-укуцан језик.

Углравном, сигурносно-типизирање и меморијска-сигурност иду једно уз друго. На пример, језик који подржава аритметички показивач и број-до-показивача конверзије (као С) није ни меморијски-сигуран нити сигурносно-откуцан, пошто дозвољава алгебарској меморији да буде приступљено као да је валидна меморија било ког типа.

За више информација, видети меморијску сигурност.

Нивои променљивих провере текста

Неки језици дозвољавају различите нивое провере како би применили на различите регионе кода. Примери укључују:

•  use strict директива у јаваскрипту и Перлу примењује јачу проверу. 
•  @ оператор у PHP-у потискује неке поруке грешке
• Option Strict On у VB.NET-у дозвољава компилатору да захтева конверзију између објеката.

Додатне алатке као што су lint и IBM Rational Purify се могу такође користити за постизање високог нивоа ограничења.

Опциони системи типизирања

Препоручено је, првенствено од стране Гилада Брахе, да избог система типизирања буде независан од избора језика; да систем типизирања треба да буде модул који може бити "укључен" у језик ако је тражено. Он сматра да је ово повољно, зато што оно што он зове обавезни системима типизирања чини језик мање изражајним и код крхким.ref>Bracha, G.: Pluggable Types</ref> Захтевност којом типизирање не утиче на семантику језика је тешко испунити, наслеђивање базирано на класи постаје немогуће.

Опционално типизирање се односи на основно типизирање, али идаље је посебан

Полиморфизам и типизирање

Термин "полиморфизам" се односи на могућност кода (тачније, методе или класе) да делује на вредности вишеструког типизирања, или могућност различитих инстанци исте структуре података да би се задржали елементи различитих типизирања. Системи типизирања који дозвољавају полиморфизам углавно то раде да би побољшали потенцијал за поновно коришћење кода: у језику са полиморфизмом, програмери морају само да имплементују структуру података као што је листа или асоцијативни низ једном, више него једном за сваки тип елемент који планирају да користе. Због овог разлока рачунарски научници неки пут користе одређене форме полиморфизма, генеричко програмирање. Фондација полиморфизма теоретичког-типизирања су блиско повезани са тим апстракцијама, модуларностима и (у неким случајевима) подтипизирањима.

Дак типизирање

У "дак типизирању", изјава која позива методу m над објектном који се не ослања на декларисан тип објекта, билоког типа, мора пружити имплементацију позване методе, када је позвана, при рантајму.

Дак типизирање се разликује од структурног типизирања у томе, ако је "део" (целог модула структуре) потребан за дату локлану компутацију је доступан у рантајму, дак систем типизирања је задовољен и његој анализи идентитета типизирања. Са друге стране, структурни систем типизирања ће захтевати анализу целог модула структуре при компилаторском времену да открије идентитет типизирања или независност типизирања.

Дак типизирање се разликује од номинативног система типизирања у бројним аспектима. Најистакнутији су они за дак типизирање, тип информација је одлучен приликом рантајма (што је контраст компилираном времену), и име типизирања је ирелевантно за одлучивање идентитета типизирања или зависности типизирања; само парцијална структура информације је потребна за то за дату тачку у извршавању програма.

Дак типизирање користи премису која (односи се на вредности) "ако хода као патка, и квакуће као патка, онда је патка" (ово је референца која се односи на дак тест која се преписује Џејмсу Виткомбу Рајлију). Термин је можда скован од стране  Алекса Мартелија 2000 у поруци  за comp.lang.python група вести (видети Пајтон ).

Док је један контролисани експеримент показао повећање код поизводње развојника за дак типизирање у једноставним развојничким пројектима, остали контролисани експерименти над АПИ коришћењу су показали обрнуто.

Специјализовани системи типизирања

Многи системи типизирања су креирани како би били специјализовани за коришћење у одређеним окружењима са одређеним типовима података, или за из-бенда статичну програмску анализу. Често, ово је базирано на идејама из формалне теорије типизирања и доступне су само као прототипи система истраживања.

Зависна типизирања

Зависна типизирања су базирана на идеји коришћења скалара или вредности да би се прецизније описало укуцавање неке друге вредности. На пример, $matrix(3,3)$ може бити тип 3×3 матрице. Можемо дефинисати правила типизирања као што је следеће за множење матрица:

где су $k$, $m$, $n$ алгебарске позитивне целобројне вредности. Варијанта ML-а која се зове Зависни ML је креиран базирајући се на систем типизирања, али зато што је провера типизирања за конвензионална зависна типизирања неодлучива, не могу сви програми који га користе да буду проверени без неких врста ограничења. Зависна ML ограничења, врста једнакости може одличити за Пресбургерову аритметику.

Остали језици као што је Епиграм чини вредност свих експресија у језику одлучивим тако да провера типизирања може бити одлучива. Међутим, углавном доказ одлучивости је неодлучив, много програми захтевају ручно-написане анотације које можда нису тривијалне. Пошто ово отежава развој процеса, много имплементације језика пружају лакши начин у форму опције да се искључи ово стање. Ово, међутим, долази по цени да контролор-типизирања улази у бесконачну петљу када нахрани програма који не проверавају типизирање, што проузрокује пад компилације.

Линеарна типизирања

Линеарна типизирања, базирана на теорији линеарне логике, су блиско повезани са спорим типизирањима, су типовима који су додељени вредности и имају особину да имају само једну референцу све време. Ово је вредно за описивање велике непроменљиве вредности као што су фајлови, стрингови, и тако даље, зато што свака операције која истовремено уништава линеарни објекат и ствара слични објекат (као што је 'str = str + "a"') може бити оптимизован "испод хаубе" у мутацију. Нормално ово није могуће, пошто овакве мутације могу изазвати нежељене ефекте над деловима програма који држи остале референце за објекат, што крши референтну транспарентност. Такође се користе у прототипу оперативног система Јединственост за међу процес комуникације, статично се осигурава да процеси не могу делити објекте у подељеној меморији како би спречили трку стања. Чисти језик (језик као Хаскел) користи систем типизирања да би добио на брзини (у односу на обављање дубоке копије) док остаје сигуран.

Међусекције типизирања

Међусекције типизирања су типизирања која описују вредности које припадају обема осталим датим типизирањима са сетовима вредности који се преклапају. На пример, у већини имплементација С-а приписан карактер има опсег -128 до 127 и неприписан карактер има опсег од 0 до 255, тако да типизирање међусекције ова два типизирања ће имати опсег од 0 до 127. Оваква међусекција типизирања се мође сигурно прећи у фунцкије које очекују или приписане или неприписане карактере, зато што је компатибилно са оба типизирања. 

Међусекцијска типизирања су корисна за описивање прекорачена типизирања функције: На пример, ако "int → int" је тип функција које узимају целобројни аргумент и враћају цео број, и "float → float" је тип функција које узимају децимални аргумент и враћају децимални број, онда међусекција између ова два типизирања се може користити да опише функције која одрађује једну или другу, базирано на типу излаза који је дат. Таква функције се може проследити у другу функције која  очекује "int → int" сигурност функције; једноставно неће користити "float → float" функционалност.

У хијерархији подкласа, међусекција типизирања и предачко типизирање (као његов родитељ) је најизведеније типизирање. Међусекција типизирања близанаца је празна.

Форсит језик укључује генералну имплементацију међусекцијског типизирања. Ограничена форма префињеног типизирања.

Сједињено типизирање

Сједињена типизирања су типизирања која описују вредности које припадају обема типизирањима. На пример, у С-и, приписани карактер има од -128 до 127 опсег, и неприписан карактер има од 0 до 255 опсег, тако да сједињење ова два типизирања би имало општи "виртуелни" опсег од -128 до 255 који се може делимично користити у зависности од тога који је члан сједињења коришћен. Свака функција која контролише сједињено типизирање би морала да има посла са целим бројевима у овом комплетном опсегу. Генералније, једине валидне операције над сједињеним типизирањем су операције које су валидне над обема типизирањима и које су сједињене. С-ов концепт "сједињења" је сличан сједињеним типизирањима, али није сигурно укуцан, пошто ограничава операције које су валидне у оба типизирања. Сједињена типизирања су битна за програмску анализу, где се користе да представе симболичне вредности чије право порекло (тј, вредност или тип) није познато.

У хијерархији подкласа, сједињено типизирање и типизирање предака (као што је родитељско) је типизирање предака. Сједињење типизирања полубрата њиховог честог предка (то је, све операције које су дозвољене над њиховим честим предком су дозвољене над сједињеним типизирањем, али могу такође имати остале валидне операције заједничке).

Егзистенцијално типизирање

Егзистенцијално типизирање се често користи у конекцији са рекордним типизирање да би се представили модули и апстрактни типови података, због њихове могућности да одвоје имплементације са њихових сучеља. На пример, тип  "T = ∃X { a: X; f: (X → int); }" описује модул сучеља који има члана податка назван а од типа X и функцију названу f која узима параметар истог типа X и враћа цео број. Ово може бити имплементовано на различите начине, на пример: 

• intT = { a: int; f: (int → int); }
• floatT = { a: float; f: (float → int); }

Ова типизирања су оба подтипизирања генералнијег егзистенцијалног типа Т и одговара конкретним имплементацијама типизирања, тако да било која вредност једног од ових типизирања је вредност типа Т. Дата вредност "т" типа "T", знамо да "т.ф (т.a)" је добро укуцано, необраћајући пажњу шта је апстракти тип Х. Ово даје флексибилност у бирању типизирања које одговарају делимичним имплементацијама док клиенти који користе само вредност сучељног типизирања—егзистенцијално типизирање—су одвојени од ових избора.

Углавном немогуће је за контролора типизирања да закључи које егзистенцијално типизирање припада датом модулу. У примеру изнат { a: int; f: (int → int); } може такође имати тип ∃X { a: X; f: (int → int); }. Најједноставније решење је записати сваки модул са његовим намењеним типом, тј.:

• intT = { a: int; f: (int → int); } as ∃X { a: X; f: (X → int); }

Иако апстракти типови података и модул су имплементовани у програмске језике већ дуже време, то није било све до 1988 када су Џон Ц. Мичел и Гордон Плоткин су утврдили формалну теорију под слоганом: "Апстрактни [подаци] типови имају егзистенцијални тип". Теорија је другог реда укуцана ламбда калкулусом сличном Систему Ф, али са егзистенцијалном уместо универзалном квантификацијом.

Постепено типизирање

Постепено типизирање је систем типизирања чије променљиве могу бити укуцане или приликом компилаторског времена (што је статично типизирање) или приликом рантајма (што је динамично типизирање), дозвољавајући софтверским развојницима да брилају оба типа парадигме као прилагођавајућу, из једног језика. Посебно, постебено типизирање користи специјално типизирање које се зове динамчино да престави статично-непозната типизирања, и постепено типизирање мења појам једнакости типизирања са новом релацијом која се назива доследност која односи динамично типизирање на сва остала типизирања. Релација доследност је суметрична али не транзистивна.

Експлицитна или имплицитна декларација и закључак

Многи статични системи типизирања, као што су они у С-у и Јави, захтевају декларацију типизирања. Програмер мора експлицитно помоћи свакој варијабли са посебним типизирањем. Остали, као што су Хаскел, користе закључно типизирање: Компилатор изводи закључке о типизирањима променљивих базираним на томе како програмери користе те променљиве. На пример, дата фунцкија  f(x, y) која додаје x и y заједно, компилатор може закључити да x и y морају бити бројеви – пошто је адиција само дефинисана за бројеве. Због тога, сваки позив на f другде у програму који спецификује не-бројив тип (као што је стринг или листа) као аргумент би дао грешку.

Нумеричке и константе стринг и експресије у коду могу и често подразумевају типизирање у одређеном контексту. На пример, експресија 3.14 може подразумевати децималну тачку, док [1, 2, 3] може подразумевати листу целих бројева - типично низ.

Тип закључка је у генералном могућ, ако је одлучив у теорији типизирања у питању. Штавише, зак иако је закључак неодлучив у генерали за дату теорију типизирања, закључак је често могућ за велике подсетове стварних програма. Хаскелов систем типизирања, верзија Хиндлеја-Милнера, је рестрикција Система F-омега тако званом ранка-1 полиморфног типизирања, у чијем случају је закључак одлучив. Већина Хаскелових компилатора дозвољавају алгебарски-ранк полиморфизма као екстензију, али ово чини типизирање закључка неодлучивим. (провера типизирања је одлучива, међутим, и ранк-1 програми идаље имају закључак; полиморфни програми вишег ранка су одбијени осим ако не дају експлицитне записе)

Типови типизирања

Типови типизирања је врста. Врсте се појављују експлицитно у куцаном програмирању, као што је конструктор типизирања у Хаскеловом језику.

• Примитивни тип података - најједноставнија врста типизирања; нпр., цео број и децимални број
  • Булов тип података
  • Интегрално типизирање - типизирање целих бројева, нпр. цели бројеви и природни бројеви 
  • – типизирање бројева у децималној репрезентацији
• типизирање референце
• Опционо типизирање
  • Нулабл врсте
• Композитне врсте – типизирања компонована пореко других типизирања: нпр., низови или рекорди.

  Апстрактни тип података

• Алгебарско типизирање
• Подтип
• Наслеђивање
• Објектни типови; нпр, типизирање променљиве
• Делимично типизирање
• Рекурзивно типизирање
• типизирања функције; нпр., бинарне функције
• универзално квантификована типизирања, као што је параметарско типизирање 
• егзистенцијално квантификована типизирања, као што су модули
• – типизирања која идентификују подсетове других типизирања
• Зависна типизирања - типизирања која зависе од услова (вредности)
• – типизирање које описује или ограничава структуру објектно-оријентисаних система
• Пре-дефинисана типизирања пружена за погодност у реалним апликацијама, као што је датум, време и новац.

Обједињени систем типизирања

Неки језици као С# имају обједињени систем типизирања. Ово значи да сви С# типиови, укључујући примитивне типове наслеђивања из једног кореног објекта. Сваки тип у С# наслеђује класе Објекта. Јава има неколико примитивних типова који нису објекти. Јава пружа омотач објектног типизирања који постоји заједно са примитивним типизирањем тако да развојници могу да користе или омотач објектног типизирања или једноставне не-објектна примитивна типизирања.

Компатибилност: једнакост и подтипизорање

Контролор типова за статично типизиране језике мора да провери да ли је тип било ког израза доследан са типизирањам које се очекује од контекста код које се тај израз појављује. На пример, у додељеној изјави форме  x := e, закључено типизирање експресије e мора бити доследан са декларисаним или закљученим типом променљиве x. Овај појам доследности, названим компатибилност, је специфичан за сваки језик.

Ако су типизирање e и типизирање x  исти и додељивање дозвољено за то типизирање, онда је ово валидна експресија. У једноставним системима типизирања, даље, питање да ли су два типизирања компатибилна се смањује до те мере да ли су једнаки (или еквивалентни). Различити језици, међутим, имају различити критеријум када су два типа експресија разумљива за означавање истог типизирања. Ове две теорије једначина типизирања варирају доста, два екстремна случаја структурног типизирања система, у коме било која два типизирања која описују вредности са истом структуром су еквивалентна, и номинативни системи типизирања, у којима ниједан од два синтаксно посебна типа експресија не означавају исто типизирање (тј., типизирања морају да имају исто "име" да би били једнаки).

Код језика са подтипизираем, релација компатибилности је комплекснија. Посебно, ако је  A подтип B, онда вредност типа A се може користити у контексту где је један од типа B очекиван, чак и ако обрнуто није тачно. Као једнакост, релација подтипа је дефинисана другачије за сваки језик програмирања, са многим могућим варијацијама. Присуство параметра или ад хок полиморфизма у језику може такође имати импликације за компатибилност типизирања.

Литература

• Inc., InfoWorld Media Group (1983). InfoWorld. InfoWorld Media Group, Inc. стр. 66. 
• Cardelli, Luca; Wegner, Peter (1985). „On understanding types, data abstraction, and polymorphism”. ACM Computing Surveys. 17 (4): 471—523. S2CID 2921816. doi:10.1145/6041.6042. 
• Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8. 
• Cardelli, Luca . "Type systems". In Allen B. Tucker. CRC Handbook of Computer Science and Engineering (PDF) (2nd ed.). . CRC Press. 2004. ISBN 978-1-58488-360-9. 
• Tratt, Laurence, Dynamically Typed Languages, Advances in Computers, Vol. 77. стр. 149–184, July 2009

Спољашње везе

• Smith, Chris, What To Know Before Debating Type Systems