Sistema de tipus
En programació informàtica, un sistema de tipus és un sistema lògic que inclou un conjunt de regles que assigna una propietat anomenada tipus (per exemple, enter, coma flotant, cadena) a cada terme (una paraula, frase o un altre conjunt de símbols). Normalment, els termes són construccions de llenguatge diferents d'un programa d'ordinador, com ara variables, expressions, funcions o mòduls.[1] Un sistema de tipus dicta les operacions que es poden realitzar en un terme. Per a les variables, el sistema de tipus determina els valors permesos d'aquest terme.[2]
Els sistemes de tipus formalitzen i apliquen les categories implícites que el programador utilitza per als tipus de dades algebraiques, estructures de dades o altres tipus de dades, com ara "cadena", "matriu de flotació", "funció que retorna booleà".[3]
Els sistemes de tipus s'especifiquen sovint com a part dels llenguatges de programació i s'incorporen als intèrprets i compiladors, encara que el sistema de tipus d'un llenguatge es pot ampliar amb eines opcionals que realitzen comprovacions addicionals utilitzant la sintaxi i la gramàtica de tipus originals del llenguatge.
L'objectiu principal d'un sistema de tipus en un llenguatge de programació és reduir les possibilitats d'errors en programes informàtics a causa d'errors de tipus. [4] El sistema de tipus donat en qüestió determina què constitueix un error de tipus, però en general, l'objectiu és evitar que les operacions que esperen un determinat tipus de valor s'utilitzin amb valors dels quals aquesta operació no té sentit (errors de validesa).
Els sistemes de tipus permeten definir interfícies entre diferents parts d'un programa informàtic, i després comprovar que les peces s'han connectat de manera coherent. Aquesta comprovació es pot produir de manera estàtica (en temps de compilació), dinàmicament (en temps d'execució) o com una combinació d'ambdues.[5]
Els sistemes de tipus també tenen altres propòsits, com ara expressar regles empresarials, habilitar determinades optimitzacions del compilador, permetre l'enviament múltiple i proporcionar una forma de documentació.[6]
Visió general d'ús
[modifica]Un exemple de sistema de tipus simple és el del llenguatge C. Les porcions d'un programa C són les definicions de funció. Una funció és invocada per una altra funció.
La interfície d'una funció indica el nom de la funció i una llista de paràmetres que es passen al codi de la funció. El codi d'una funció invocadora indica el nom de la invocada, juntament amb els noms de les variables que contenen valors per passar-li.
Durant l'execució d'un programa informàtic, els valors es col·loquen a l'emmagatzematge temporal i, a continuació, l'execució salta al codi de la funció invocada. El codi de la funció invocada accedeix als valors i en fa ús.
Si les instruccions dins de la funció s'escriuen amb el supòsit de rebre un valor enter, però el codi de trucada ha passat un valor de coma flotant, la funció invocada calcularà el resultat incorrecte.
El compilador C comprova els tipus d'arguments passats a una funció quan es crida amb els tipus de paràmetres declarats a la definició de la funció. Si els tipus no coincideixen, el compilador llança un error o un avís en temps de compilació.
Un compilador també pot utilitzar el tipus estàtic d'un valor per optimitzar l'emmagatzematge que necessita i l'elecció dels algorismes per a les operacions sobre el valor. En molts compiladors C el tipus de dades flotant, per exemple, es representa en 32 bits, d'acord amb l'especificació IEEE per a números de coma flotant de precisió única. Per tant, utilitzaran operacions de microprocessador específiques de coma flotant sobre aquests valors (suma de coma flotant, multiplicació, etc.).
La profunditat de les restriccions de tipus i la manera de la seva avaluació afecten l'escriptura de la llengua. Un llenguatge de programació també pot associar una operació amb diverses resolucions per a cada tipus, en el cas del polimorfisme de tipus. La teoria de tipus és l'estudi dels sistemes de tipus. Els tipus concrets d'alguns llenguatges de programació, com els nombres enters i les cadenes, depenen de qüestions pràctiques d'arquitectura d'ordinadors, implementació del compilador i disseny de llenguatges.[7]
Fonaments
[modifica]Formalment, la teoria de tipus estudia els sistemes de tipus. Un llenguatge de programació ha de tenir l'oportunitat de verificar el tipus mitjançant el sistema de tipus, ja sigui en temps de compilació o en temps d'execució, amb anotacions manuals o deduïdes automàticament. Com Mark Manasse va dir de manera concisa: [8]
L'assignació d'un tipus de dades, denominat escriptura, dóna significat a una seqüència de bits com un valor en memòria o algun objecte com una variable. El maquinari d'un ordinador de propòsit general és incapaç de discriminar entre, per exemple, una adreça de memòria i un codi d'instrucció, o entre un caràcter, un nombre enter o un nombre de coma flotant, perquè no fa cap distinció intrínseca entre cap dels possibles valors que pot significar una seqüència de bits. Associar una seqüència de bits a un tipus transmet aquest significat al maquinari programable per formar un sistema simbòlic format per aquest maquinari i algun programa.
Un programa associa cada valor amb almenys un tipus específic, però també pot passar que un valor estigui associat amb molts subtipus. Altres entitats, com ara objectes, mòduls, canals de comunicació i dependències es poden associar amb un tipus. Fins i tot un tipus es pot associar amb un tipus. Una implementació d'un sistema de tipus podria, en teoria, associar identificacions anomenades tipus de dades (un tipus de valor), classe (un tipus d'objecte) i tipus (un tipus de tipus o metatipus). Aquestes són les abstraccions per les quals pot passar la mecanografia, en una jerarquia de nivells continguts en un sistema.
Quan un llenguatge de programació desenvolupa un sistema de tipus més elaborat, obté un conjunt de regles més detallat que la comprovació de tipus bàsica, però això té un preu quan les inferències de tipus (i altres propietats) es tornen indecidibles, i quan el programador ha de prestar més atenció per anotar el codi o per considerar les operacions i el funcionament relacionats amb l'ordinador. És difícil trobar un sistema de tipus prou expressiu que satisfà totes les pràctiques de programació d'una manera segura.
Un compilador de llenguatge de programació també pot implementar un tipus dependent o un sistema d'efectes, que permet que un verificador de tipus pugui verificar encara més especificacions del programa. Més enllà dels simples parells de tipus valor, una "regió" virtual de codi s'associa amb un component "efecte" que descriu què es fa amb què i que permet, per exemple, "llençar" un informe d'error. Així, el sistema simbòlic pot ser un sistema de tipus i efectes, la qual cosa el dota de més control de seguretat que el control de tipus sol.
Comprovació de tipus
[modifica]El procés de verificació i aplicació de les restriccions de tipus (comprovació de tipus ) pot produir-se en temps de compilació (una comprovació estàtica) o en temps d'execució (una comprovació dinàmica).
Si una especificació d'idioma requereix les seves regles d'escriptura amb força, més o menys permetent només aquelles conversions de tipus automàtiques que no perden informació, es pot referir al procés com a fortament tipificat ; si no, com feblement escrit.
Normalment, els termes no s'utilitzen en sentit estricte.
Comprovació de tipus estàtic
[modifica]La comprovació de tipus estàtic és el procés de verificació de la seguretat del tipus d'un programa basat en l'anàlisi del text d'un programa ( codi font ). Si un programa passa un verificador de tipus estàtic, es garanteix que el programa satisfà algun conjunt de propietats de seguretat de tipus per a totes les entrades possibles.
Comprovació de tipus dinàmica i informació de tipus d'execució
[modifica]La verificació de tipus dinàmica és el procés de verificació de la seguretat del tipus d'un programa en temps d'execució. Les implementacions de llenguatges de verificació de tipus dinàmica generalment associen cada objecte en temps d'execució amb una etiqueta de tipus (és a dir, una referència a un tipus) que conté la seva informació de tipus. Aquesta informació de tipus d'execució (RTTI) també es pot utilitzar per implementar l'enviament dinàmic, l'enquadernació tardana, la baixada, la programació reflexiva (reflexió) i funcions similars.
Combinant la comprovació de tipus estàtica i dinàmica
[modifica]Alguns idiomes permeten escriure tant estàtic com dinàmic. Per exemple, Java i alguns altres llenguatges aparentment escrits de forma estàtica admeten la baixada de tipus als seus subtipus, consultant un objecte per descobrir-ne el tipus dinàmic i altres operacions de tipus que depenen de la informació del tipus d'execució. Un altre exemple és C++ RTTI. De manera més general, la majoria dels llenguatges de programació inclouen mecanismes per a l'enviament de diferents "tipus" de dades, com ara unions disjuntives, polimorfisme en temps d'execució i tipus variants. Fins i tot quan no interacciona amb anotacions de tipus o comprovació de tipus, aquests mecanismes són materialment similars a les implementacions d'escriptura dinàmica.
Referències
[modifica]- ↑ Pierce, 2002, p. 1.
- ↑ «Type Systems» (en anglès). [Consulta: 24 març 2025].
- ↑ «Types and the Type System» (en anglès). [Consulta: 24 març 2025].
- ↑ Cardelli, 2004, p. 1.
- ↑ Sedlacek, Magnus. «Introduction to type systems» (en anglès americà), 05-06-2024. [Consulta: 24 març 2025].
- ↑ «Material Design» (en anglès). [Consulta: 24 març 2025].
- ↑ «Type Systems in Software Explained With Examples» (en anglès americà), 27-09-2020. [Consulta: 24 març 2025].
- ↑ Pierce, 2002, p. 208.