Teorio de tipoj

El Vikipedio, la libera enciklopedio
Saltu al: navigado, serĉo

En programlingva teorio, branĉo de komputiko, la teorio de tipoj provizas la formalan bazon por la dizajno, analitiko kaj studo de tipo-sistemoj. Ja, multaj komputilo-sciencistoj uzas la terminon teorio de tipoj por nomi la formalan studon de tipo-sistemoj por programlingvoj, kvankam iuj limigas ĝin al la studo de pli abstraktaj formalismoj kiel tipitaj λ-kalkuloj. Je la plej larĝa nivelo, teorio de tipoj estas la branĉo de matematiko kaj logiko, kiu koncernas sin kun klasigi entojn en kolektojn nomitajn kiel tipoj. En ĉi tiu senco, ĝi rilatas al la metafizika nocio de 'tipo'. La moderna teorio de tipoj estis inventita parte en respondo al la paradokso de Russell, kaj estas esprimitas elstare en Principoj Mathematica far Russell kaj Whitehead.

Tipa sistemo[redakti | redakti fonton]

La difinoj de tipo-sistemo diversas, sed jena de Benjamin C. Pierce malglate korespondas al la aktuala interkonsento en la programlingva teoria komunaĵo:

Tipo-sistemo estas akordiĝema sintakta maniero pruvi la foreston de certaj programaj kondutoj kaj per tio klasigi frazojn laŭ la specoj de valoroj, kiujn ili komputas.

En aliaj vortoj, tipo-sistemo dividas programajn valorojn en arojn nomitajn kiel tipoj (ĉi tio estas nomata kiel "tip-asigno"), kaj proklamas certajn programajn kondutojn kiel mallaŭregula sur la bazo de la tipoj, kiuj estas tial asignitaj. Ekzemple, tip-sistemo povas klasifiki valoron "hola" kiel linio kaj la valoro 5 kiel nombro, kaj malpermesi la programisto adicii "hola" al 5 surbaze de tiu tip-asigno. En ĉi tiu tipa sistemo, la programo

"hola" + 5

devas esti mallaŭregula. De ĉi tie, ĉiu programo permesita laŭ la tip-sistemo devus esti verŝajne libera de la erara konduto de adicio de linioj kun nombroj.

La dizajno kaj realigo de tip-sistemoj estas aktuala proksime same kiel aktuala estas programlingvo mem. Fakte, proponantoj de la teorio de tipoj kutime proklamas, ke la dizajno de tipo-sistemoj estas la pura esenco de programlingva dizajno: "Dizajnu la tip-sistemon ĝuste, kaj la lingvo dizajniĝos mem.".


Eksteraj ligiloj[redakti | redakti fonton]