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

Из Википедије, слободне енциклопедије

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

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

Преглед употребе[уреди]

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

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

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

Основе[уреди]

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

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

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

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

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

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

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

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

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

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

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

Провера куцања[уреди]

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

Статичка провера куцања[уреди]

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

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

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

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

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

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

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

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

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

Динамичка провера куцања и рантајм тип информација[уреди]

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

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

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

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

Комбиновање статичне и динамчне провере куцања[уреди]

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

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

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

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

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

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

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

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

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

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

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

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

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

"Јаки" и "слаби" системи куцања[уреди]

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

Сигурносно куцање и сигурносна меморија[уреди]

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

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

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

1 var x := 5; 
2 var y := "37"; 
3 var z := x + y;

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

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

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

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

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

Нивои променљивих провере текста[уреди]

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

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

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

Опциони системи куцања[уреди]

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

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

Полиморфизам и куцање[уреди]

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

Дак куцање[уреди]

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

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

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

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

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

Специјализовани системи куцања[уреди]

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

Зависна куцања[уреди]

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

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

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

Линеарна куцања[уреди]

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

Међусекције куцања[уреди]

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

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

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

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

Сједињено куцање[уреди]

Сједињена куцања су куцања која описују вредности које припадају обема куцањима. На пример, у С-и, приписани карактер има од -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 када су Џон Ц. Мичел и Гордон Плоткин су утврдили формалну теорију под слоганом: "Апстрактни [подаци] типови имају егзистенцијални тип".[21] Теорија је другог реда укуцана ламбда калкулусом сличном Систему Ф, али са егзистенцијалном уместо универзалном квантификацијом.

Постепено куцање[уреди]

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

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

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

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

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

Типови куцања[уреди]

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

Обједињени систем куцања[уреди]

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

Компатибилност: једнакост и подкуцање[уреди]

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

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

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

Референце[уреди]

  1. 1,0 1,1 Pierce (2002)
  2. Cardelli (2004). стр. 1.
  3. Pierce (2002). стр. 208.
  4. Inc., InfoWorld Media Group, (1983). InfoWorld. InfoWorld Media Group, Inc. стр. 66. ISSN 01996649. 
  5. Brian Kernighan: Why Pascal is not my favorite language
  6. R´emy, Didier.
  7. "dynamic (C# Reference)".
  8. Meijer, Erik; Drayton, Peter.
  9. Laucher, Amanda; Snively, Paul.
  10. Xi, Hongwei; Scott, Dana (1998).
  11. Visual Basic is an example of a language that is both type-safe and memory-safe.
  12. Standard ECMA-262.
  13. Strict mode - JavaScript | MDN.
  14. Strict Mode (JavaScript).
  15. „c# - Is there a language that allows both static and dynamic typing?”. Stack Overflow. Приступљено 8. 1. 2016. 
  16. Rozsnyai, S.; Schiefer, J.; Schatten, A. (2007).
  17. Martelli, Alex (26 July 2000).
  18. Stefan Hanenberg.
  19. Kleinschmager, Hanenberg, Robbes, Tanter, Stefik: Do static type systems improve the maintainability of software systems?
  20. Hanenberg, Kleinschmager, S.Robbes, R.Tanter, Stefik: An empirical study on the impact of static typing on software maintainability, ESE 2014
  21. Mitchell, John C.; Plotkin, Gordon D.; Abstract Types Have Existential Type, ACM Transactions on Programming Languages and Systems, Vol. 10, No. 3, July (1988). стр. 470–502
  22. Siek, Jeremy.
  23. Siek, Jeremy; Taha, Walid (September 2006).
  24. Standard ECMA-334, 8.2.4 Type system unification.

Литература[уреди]

Спољашње везе[уреди]