Teorio de tipoj

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

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

greke Abstrakta datumtipo greke Enkonduka papero pri formala bazo de ADT-oj, interrilato al teorio de kategorioj, kaj listo de bonaj referencoj. Paĝoj 3-4 aperas taŭgaj. Referenca nombro [6] aspektas bona, sed ĝi povas ne esti havebla surlinie. greke Naiva komputa tip-teorio per Robert L. Constable greke Peter B. Andrews, Enkonduko al matematika logiko kaj tipa teorio: al vero tra pruvo, dua redakcio, Kluwer Academic Publishers, 2002. http://www.springeronline.com/sgw/cda/frontpage/0,11855,4-0-22-33641956-0,00.html?referer=www.springeronline.com/isbn/1-4020-0763-9 greke Luca Cardelli, "Tipaj Sistemoj," La Komputila Scienco kaj Inĝenierada Gvidlibro, Allen B. Tucker (red.), ĉapitro 103, pp. 2208-2236, CRC Press, Boca Raton, FL, 1997. (rete)