Inferència de tipus

Inferència de tipus, de vegades anomenada reconstrucció de tipus,: 320 , es refereix a la detecció automàtica del tipus d'una expressió en un llenguatge formal. Aquests inclouen llenguatges de programació i sistemes de tipus matemàtics, però també llenguatges naturals en algunes branques de la informàtica i la lingüística.

La tipabilitat s'utilitza de vegades com a sinònim d'inferència de tipus, però alguns autors distingeixen entre la tipabilitat com a problema de decisió (que té una resposta de sí/no) i la inferència de tipus com el càlcul d'un tipus real per a un terme.

Explicació no tècnica

En un llenguatge mecanografiat, el tipus d'un terme determina les maneres en què es pot i no es pot utilitzar en aquest idioma. Per exemple, considerem la llengua anglesa i els termes que podrien omplir l'espai en blanc de la frase "sing _". El terme "a song" és de tipus cantable, de manera que es podria col·locar a l'espai en blanc per formar una frase significativa: "sing a song". D'altra banda, el terme "a friend" no té el tipus cantable, de manera que "sing a friend" no té sentit. En el millor dels casos, podria ser una metàfora; doblegar les regles del tipus és una característica del llenguatge poètic.

El tipus d'un terme també pot afectar la interpretació de les operacions que impliquen aquest terme. Per exemple, "una cançó" és de tipus componible, de manera que l'interpretem com la cosa creada a la frase "escriu una cançó". D'altra banda, "un amic" és de tipus destinatari, de manera que l'interpretem com el destinatari de la frase "escriu a un amic". En llenguatge normal, ens sorprendria que "escriure una cançó" signifiqués adreçar una carta a una cançó o "escriure a un amic" signifiqués esborrar un amic en paper.

Termes amb diferents tipus poden fins i tot referir-se materialment a la mateixa cosa. Per exemple, interpretaríem "penjar l'estenedor" com posar-lo en ús, però "penjar la corretja" com guardar-la, tot i que, en context, tant "estenedor" com "corretja" podrien referir-se a la mateixa corda, només que en moments diferents.

Les tipificacions sovint s'utilitzen per evitar que un objecte es consideri de manera massa general. Per exemple, si el sistema de tipus tracta tots els nombres com a iguals, un programador que escrigui accidentalment codi on 4 se suposa que significa "4 segons" però s'interpreta com a "4 metres" no rebria cap avís del seu error fins que no causés problemes en temps d'execució. En incorporar unitats al sistema de tipus, aquests errors es poden detectar molt abans. Com a un altre exemple, la paradoxa de Russell sorgeix quan qualsevol cosa pot ser un element de conjunt i qualsevol predicat pot definir un conjunt, però una tipificació més acurada ofereix diverses maneres de resoldre la paradoxa. De fet, la paradoxa de Russell va donar inici a les primeres versions de la teoria de tipus.

Hi ha diverses maneres en què un terme pot obtenir el seu tipus:

• El tipus de lletra es pot proporcionar des d'algun lloc extern al passatge. Per exemple, si un parlant es refereix a "una cançó" en anglès, generalment no ha de dir a l'oient que "una cançó" es pot cantar i compondre; aquesta informació forma part del seu coneixement previ compartit.
• El tipus es pot declarar explícitament. Per exemple, un programador podria escriure una instrucció com ara delay: seconds := 4 en el seu codi, on els dos punts són el símbol matemàtic convencional per marcar un terme amb el seu tipus. És a dir, aquesta instrucció no només estableix delay al valor 4, sinó que la part delay: seconds també indica que el tipus de delay és una quantitat de temps en segons.
• El tipus es pot inferir del context. Per exemple, a la frase "I bought it for a song" (Ho vaig comprar per una cançó), podem observar que intentar donar al terme "una cançó" tipus com "cantable" i "composable" portaria a un disbarat, mentre que el tipus "quantitat de moneda" funciona. Per tant, sense que calgui que ens ho diguin, concloem que "song" (cançó) aquí ha de significar "poc o res", com en l'idioma anglès " for a song), no "una peça musical, generalment amb lletra".

Especialment en els llenguatges de programació, pot ser que no hi hagi gaire coneixement previ compartit disponible per a l'ordinador. En els llenguatges manifestament tipats, això significa que la majoria dels tipus s'han de declarar explícitament. La inferència de tipus pretén alleujar aquesta càrrega, alliberant l'autor de declarar tipus que l'ordinador hauria de poder deduir del context.

Comprovació de tipus vs. inferència de tipus

En una tipificació, una expressió E s'oposa a un tipus T, formalment escrit com a E : T. Normalment, una escriptura només té sentit dins d'un cert context, que s'omet aquí.

En aquest context, les preguntes següents són d'especial interès:

1. E : T? En aquest cas, es donen tant una expressió E com un tipus T. Ara, és E realment un T? Aquest escenari es coneix com a comprovació de tipus.
2. E : _? Aquí només es coneix l'expressió. Si hi ha una manera de derivar un tipus per a E, aleshores hem aconseguit la inferència de tipus.
3. _ : T? A l'inrevés. Donat només un tipus, hi ha alguna expressió per a aquest o el tipus no té valors? Hi ha algun exemple de T? Això es coneix com a inhabitabilitat de tipus.

Per al càlcul lambda de tipus simple, les tres preguntes són decidibles. La situació no és tan còmoda quan es permeten tipus més expressius.

Tipus en llenguatges de programació

Els tipus són una característica present en alguns llenguatges amb tipatge estàtic fort. Sovint és característica dels llenguatges de programació funcional en general. Alguns llenguatges que inclouen la inferència de tipus inclouen C (des de C23 ), C++ (des de C++11 ), C# (a partir de la versió 3.0), Chapel, Clean, Crystal, D, Dart, F#, FreeBASIC, Go, Haskell, Java (a partir de la versió 10), Julia, Kotlin, ML, Nim, OCaml, Opa, Q#, RPython, Rust, Scala, Swift, TypeScript, Vala, Zig i Visual Basic (a partir de la versió 9.0). La majoria d'ells utilitzen una forma simple d'inferència de tipus; El sistema de tipus Hindley-Milner pot proporcionar una inferència de tipus més completa. La capacitat d'inferir tipus automàticament facilita moltes tasques de programació, deixant el programador lliure d'ometre anotacions de tipus alhora que permet la comprovació de tipus.

En alguns llenguatges de programació, tots els valors tenen un tipus de dades declarat explícitament en temps de compilació, cosa que limita els valors que una expressió particular pot prendre en temps d'execució. Cada cop més, la compilació just-in-time desdibuixa la distinció entre el temps d'execució i el temps de compilació. Tanmateix, històricament, si el tipus d'un valor només es coneix en temps d'execució, aquests llenguatges tenen un tipatge dinàmic. En altres llenguatges, el tipus d'una expressió només es coneix en temps de compilació; aquests llenguatges tenen un tipatge estàtic. En la majoria dels llenguatges amb tipatge estàtic, els tipus d'entrada i sortida de les funcions i les variables locals normalment s'han de proporcionar explícitament mitjançant anotacions de tipus. Per exemple, en ANSI C:

int add_one(int x) {
    int result; /* declare integer result */

    result = x + 1;
    return result;
}

La signatura d'aquesta definició de funció, int add_one(int x), declara que add_one és una funció que pren un argument, un enter, i retorna un enter. int result; declara que la variable local result és un enter. En un llenguatge hipotètic que admeti inferència de tipus, el codi es podria escriure així:

add_one(x) {
    var result;  /* inferred-type variable result */
    var result2; /* inferred-type variable result #2 */

    result = x + 1;
    result2 = x + 1.0;  /* this line won't work (in the proposed language) */
    return result;
}

Això és idèntic a com s'escriu el codi en el llenguatge Dart, excepte que està subjecte a algunes restriccions addicionals com es descriu a continuació. Seria possible inferir els tipus de totes les variables en temps de compilació. A l'exemple anterior, el compilador inferiria que result i x tenen tipus integer ja que la constant 1 és de tipus integer, i per tant que add_one és una funció int -> int. La variable result2 no s'utilitza de manera legal, per la qual cosa no tindria un tipus.

En el llenguatge imaginari en què està escrit l'últim exemple, el compilador assumiria que, en absència d'informació contrària, + pren dos enters i retorna un enter. (Així és com funciona, per exemple, a OCaml.) A partir d'això, l'inferent de tipus pot inferir que el tipus de x + 1 és un enter, la qual cosa significa que result és un enter i, per tant, el valor de retorn de add_one és un enter. De la mateixa manera, com que + requereix que tots dos arguments siguin del mateix tipus, x ha de ser un enter i, per tant, add_one accepta un enter com a argument.

Tanmateix, a la línia següent, result2 es calcula sumant un decimal 1.0 amb aritmètica de coma flotant, cosa que provoca un conflicte en l'ús de x tant per a expressions enteres com de coma flotant. L'algoritme d'inferència de tipus correcte per a aquesta situació es coneix des del 1958 i se sap que és correcte des del 1982. Revisita les inferències anteriors i utilitza el tipus més general des del principi: en aquest cas, coma flotant. Tanmateix, això pot tenir implicacions perjudicials, per exemple, utilitzar un tipus de coma flotant des del principi pot introduir problemes de precisió que no hi haurien estat amb un tipus enter.

Sovint, però, s'utilitzen algoritmes d'inferència de tipus degenerats que no poden fer marxa enrere i, en canvi, generen un missatge d'error en aquesta situació. Aquest comportament pot ser preferible, ja que la inferència de tipus no sempre és neutral algorítmicament, tal com s'il·lustra amb el problema de precisió de coma flotant anterior.

Un algorisme de generalitat intermèdia declara implícitament result2 com una variable de coma flotant, i la suma converteix implícitament x en una variable de coma flotant. Això pot ser correcte si els contextos de crida no proporcionen mai un argument de coma flotant. Aquesta situació mostra la diferència entre la inferència de tipus, que no implica conversió de tipus, i la conversió de tipus implícita, que força les dades a un tipus de dades diferent, sovint sense restriccions.

Finalment, un inconvenient significatiu dels algorismes complexos d'inferència de tipus és que la resolució de la inferència de tipus resultant no serà òbvia per als humans (sobretot a causa del backtracking), cosa que pot ser perjudicial, ja que el codi està pensat principalment per ser comprensible per als humans.

Descripció tècnica

La inferència de tipus és la capacitat de deduir automàticament, parcialment o totalment, el tipus d'una expressió en temps de compilació. El compilador sovint pot inferir el tipus d'una variable o la signatura de tipus d'una funció, sense que s'hagin proporcionat anotacions de tipus explícites. En molts casos, és possible ometre completament les anotacions de tipus d'un programa si el sistema d'inferència de tipus és prou robust o el programa o el llenguatge és prou simple.

Per obtenir la informació necessària per inferir el tipus d'una expressió, el compilador recopila aquesta informació com a agregat i posterior reducció de les anotacions de tipus donades per a les seves subexpressions, o mitjançant una comprensió implícita del tipus de diversos valors atòmics (per exemple, cert). : Bool; 42 Enter; 3.14159 : Real; etc.). És mitjançant el reconeixement de l'eventual reducció d'expressions a valors atòmics implícitament tipats que el compilador d'un llenguatge d'inferència de tipus pot compilar un programa completament sense anotacions de tipus.

En formes complexes de programació d'ordre superior i polimorfisme, no sempre és possible que el compilador infereixi tant, i les anotacions de tipus ocasionalment són necessàries per a la desambiguació. Per exemple, se sap que la inferència de tipus amb recursivitat polimòrfica és indecidible. A més, les anotacions de tipus explícites es poden utilitzar per optimitzar el codi obligant el compilador a utilitzar un tipus més específic (més ràpid/més petit) del que havia inferit.

Alguns mètodes per a la inferència de tipus es basen en la satisfacció de restriccions o en teories de mòdul de satisfacció .

Exemple d'alt nivell

Per exemple, el map de funcions de Haskell aplica una funció a cada element d'una llista, i es pot definir com:

map f [] = []
map f (first:rest) = f first : map f rest

(Recordeu que : a Haskell denota cons, estructurant un element principal i una cua de llista en una llista més gran o desestructurant una llista no buida en el seu element principal i la seva cua. No denota "de tipus" com en matemàtiques i en altres llocs d'aquest article; a Haskell aquest operador "de tipus" s'escriu :: en canvi.)

La inferència de tipus a la funció map es duu a terme de la següent manera. map és una funció de dos arguments, de manera que el seu tipus està restringit a ser de la forma a -> b -> c. En Haskell, els patrons [] i (first:rest) sempre coincideixen amb llistes, de manera que el segon argument ha de ser un tipus de llista: b = [d] per a algun tipus d. El seu primer argument f s'aplica a l'argument first, que ha de tenir el tipus d, corresponent al tipus de l'argument de la llista, de manera que f :: d -> e ( :: significa "és del tipus") per a algun tipus e. El valor de retorn de map f Finalment, map f és una llista de tot allò que f produeix, per tant [e].

Ajuntar les parts porta al map :: (d -> e) -> [d] -> [e]. Les variables de tipus no tenen res d'especial, per tant es poden reetiquetar com a

map :: (a -> b) -> [a] -> [b]

Resulta que aquest també és el tipus més general, ja que no s'apliquen més restriccions. Com que el tipus de map inferit és paramètricament polimòrfic, el tipus dels arguments i els resultats de f no s'infereixen, sinó que es deixen com a variables de tipus, i per tant map es pot aplicar a funcions i llistes de diversos tipus, sempre que els tipus reals coincideixin en cada invocació.