Tyyppi-tuote

Tuotetyyppi (myös Π -tyyppi , tyyppien tuote ; englanninkielinen  tuotetyyppi ) - ohjelmointikielien rakentaminen ja intuitionistinen tyyppiteoria , tietotyyppi , rakennettu alkuperäisten tyyppien karteesisena tuotteena ; toisin sanoen monikko tyyppejä tai " monikko tyyppinä " . Käytetyt tyypit ja niiden järjestys määräävät tuotetyypin allekirjoituksen ; objektien järjestys luodussa monikossa säilyy koko sen elinkaaren ajan annetun allekirjoituksen mukaisesti.

Esimerkiksi, jos tyypit Aja Bovat arvojoukkoja aja bvastaavasti, niin niistä muodostuva karteesinen tulo kirjoitetaan muodossa A× Bja tuloksena oleva tuotetyyppi on koko joukko mahdollisia pareja . (a,b)

Teoreettinen ja sovellettu arvo

Call by value - kielillä tuotetyyppi voidaan tulkita tyyppiluokan tuotteeksi . Curry-Howardin mukaan tuotetyypit vastaavat logiikan konjunktioitaAND (operaatioita ).

Kahden tyyppisen tuotteen erikoistapausta kutsutaan usein " pariksi " tai tarkemmin sanottuna " järjestetyksi pariksi ". Mielivaltaisen äärellisen määrän tyyppejä tuloa kutsutaan " n-aariseksi tuotetyypiksi " tai " n-tyypin joukoksi ". Venäjänkielisessä kirjallisuudessa on myös muunnos nimestä " järjestetty enka " (yleistys sanoista " kaksi ", " troika " jne.), joka on kielellisesti rakennettu analogisesti englanninkielisen termin " tuple " kanssa (katso tuple   ( ks. Englanti) ).

Tuotetyypin rappeutunut muoto, nollatyyppien tulo, on yksittäinen tyyppi ( englanniksi  unit type , “ unit type ”), eli tyyppi, jota edustaa yksi arvo. Joidenkin kielten tyyppijärjestelmät (kuten Python ) voivat tarjota yhden tai useamman ainutlaatuisen yksittäistyypin, jotka eivät ole yhteensopivia nolla-tuple-tyypin kanssa .

Tuotetyypit on rakennettu useimpiin toiminnallisiin ohjelmointikieliin. Esimerkiksi tuotetyyppi 1 × … × tyyppi n kirjoitetaan tyypiksi 1 * … * tyyppi n ML : ssä tai (tyypiksi 1, … ,tyyppi n) Haskellissa . Molemmissa kielissä monikot kirjoitetaan muodossa (v 1, ... ,v n) ja niiden komponentit erotetaan mallisovituksella . Lisäksi useimmat toiminnalliset kielet tarjoavat algebrallisia tietotyyppejä , jotka laajentavat sekä tuotetyypin että summatyypin käsitteitä . Yhden konstruktorin määrittämät algebralliset tyypit ovat isomorfisia tuotetyyppien kanssa.

Tyyppisarja puhtaana tuotetyyppinä toimii muodollisena perusteluna yleisemmälle " tietue " yhdistelmätyypille kielissä , vaikka jotkut kielet toteuttavatkin molemmat säilöt. Ero on yleensä siinä, että monikot asettavat ja tallentavat komponenttiensa järjestyksen tietokoneen muistiin (tämä on tärkeää käytettäessä komponenttejaan osoitearitmeettisten tietojen avulla ), mutta ne eivät tarjoa pääsyä niihin hyväksyttyjen tunnisteiden ja tietueiden kautta. päinvastoin, määritä tunnisteet, mutta älä määritä järjestystä. Poikkeuksia kuitenkin on:

• Standard ML -kielessä arvotuplet toteutetaan muistin asettelun optimoimiseksi tietueiden avulla, joiden komponenttitunnisteet ovat niiden järjestysnumerot monikkossa; osoitearitmetiikka ei ole käytettävissä; tyypit lakkaavat olemasta kokoamisen jälkeen; ja vaadittu järjestys saadaan voimaan vain kieltenvälisellä vuorovaikutuksella .
• C : ssä tietotyyppi " struct " ( struct) yhdistää tietueiden ja monikoiden ominaisuudet, eli sen avulla voit määrittää komponenteille tunnisteita ja samalla varmistaa niiden järjestyksen säilymisen. Lisäksi, toisin kuin tietueet ja monikot, C:n rakenteet voivat sisältää osoittimia omiin objekteihinsa, jolloin voit rakentaa suoraan rekursiivisia tietotyyppejä .

Toteutus ohjelmointikielillä

Tuples

Merkinnät

Monilla kielillä tietue on aggregoitu tietotyyppi , joka kapseloi piilottamatta erityyppisiä arvoja .

Joissakin kielissä (esimerkiksi C tai Pascal ) arvojen muistiin sijoittamisjärjestys määritetään tyyppiä määritettäessä ja se tallennetaan objektien koko elinkaaren ajan, mikä mahdollistaa epäsuoran pääsyn (esim. esimerkiksi osoittimien kautta ); muilla kielillä (esimerkiksi ML :ssä ) sijoitusjärjestystä ei ole määritelty, joten arvoihin pääsee käsiksi vain hyväksytyllä tunnisteella. Joillakin kielillä, vaikka järjestys säilyy, kääntäjä hallitsee kohdistusta , joten osoitearitmetiikka voi olla alustasta riippuvaista. Jotkut kielet sallivat kohdistamisen eri tietueiden esiintymien välillä, huomioimatta erot tietuekomponenttien tunnisteissa ja perustuvat vain järjestykseen. Muut kielet päinvastoin ottavat huomioon vain nimien yhteensopivuuden ja ratkaisevat erot niiden määrittelyjärjestyksessä.

Tietueet esiteltiin ensin Cobol-kielellä , jossa niillä oli melko monimutkainen merkintä. Tarkistaessaan tyypin yhdenmukaisuutta Cobol ottaa huomioon vain tietueiden kenttien nimien vastaavuuden eikä ota huomioon niiden järjestyksen vastaavuutta.

Tuples toimii muodollisena perusteena tietueille tyyppiteoriassa . Samaan aikaan kielissä monikot voidaan joskus toteuttaa tietueiden avulla, jotka käyttävät tunnisteena tuloksena olevan monikon kenttien indeksinumeroita.

C:n rakenteet

C - kielessä rakenne ( struct) on yhdistetty tietotyyppi , joka kapseloi piilottamatta erityyppisiä arvoja . Järjestys, jossa arvot sijoitetaan muistiin, määritetään tyyppiä määritettäessä, ja se säilytetään objektien koko elinkaaren ajan, mikä mahdollistaa epäsuoran pääsyn (esimerkiksi osoittimien kautta ).

Muistiinpanot

Linkit

• Homotopy Type Theory: Univalent Foundations of Mathematics, osa  1.5 . — Univalent Foundations Program, Institute for Advanced Study.
• Robert Harper . Standard ML:n esittely. - Carnegie Mellon University, 1986. - 97 s. — ISBN PA 15213-3891.
• Emmanuel Chalois, Pascal Manoury, Bruno Pagano. Ohjelmakehitys Objective Camlin kanssa. – 2007.