Luento 9 - Tyyppiteorian alkeet

Yhdeksännen luennon aiheena oli tyyppiteoria. Kaikissa ohjelmointikielissä on tyyppejä. Tyyppi kertoo oleellisesti, mitä tietyllä oliolla voi tehdä. Jossain ohjelmointikielessä voi olla esimerkiksi sallittua yhdistää lukuja tyyliin "5 . 2 . 342", josta seuraisi luku "52342". Toisaalta tämän tyylinen operaatio voi aiheuttaa virheen. Virhe voidaan havaita joko käännösvaiheessa tai ajonaikana. Tässä palataan jälleen aiemmin mainittuun jakoon, dynaamisesti ja staattisesti tyypitettyihin kieliin.

Kielet eivät välttämättä ole selvästi ainoastaan staattisia tai vain dynaamisia vaan ne voivat sisältää myös molempia piirteitä. Esimerkiksi Javassa käännösaikana saadaan kiinni melko paljon erilaisia tyyppivirheitä. Toisaalta myös ajonaikana niitä voidaan havaita. Pythonin tapauksessa staattista, käännösaikana tapahtuvaa tyyppitarkistusta ei tehdä lainkaan. Tarkistukset tehdään dynaamisesti ajonaikana.

Tässä yhteydessä lienee tarpeen mainita vahvuuden käsitteestä. Javan staattista ja dynaamista tyyppitarkistusta kumpaakin voidaan pitää melko vahvana. Pythonin staattista tarkistusta voidaan pitää erittäin heikkona, koska sillä ei ole sitä lainkaan, mutta toisaalta sen dynaaminen tarkistus on erittäin vahva.

Itselleni Pythonin lähestymistapa on Javaa luontevampi. Tyyppejä voi halutessaan välillä tarkistaa (esim. assert toimii mukavasti), mutta itse kieli ei pakota määrittelemään eksplisiittisiä tyyppejä. Tyypit määräytyvät sijoituksen perusteella. Esimerkiksi jos sijoitan muuttujaan kokonaisluvun, on sen tyyppi sen jälkeen kokonaisluku. Toisaalta myös kaikki muuttujat viittaavat olioihin (primitiivityyppejä ei ole lainkaan, kuten Javassa), mikä sinällään on ihan mielenkiintoista. Tietenkin myös aliohjelmia voi sijoittaa ovathan ne olioita.

Javan tapauksessa tyyppejä joutuu miettimään tarkemmin. Toisaalta myös geneerisen koodin kirjoittaminen on hankalampaa, mutta tätä varten Javassa onkin omat vippaskonstinsa. Dynaamisesta ympäristöstä tuttua tapaa ajatella on ikäänkuin liimattu Javan päälle, mikä ei välttämättä ole aivan huono asia, geneerisyys kun sattuu olemaan varsin kätevä apuväline.

Näen tyypit osana testausta. Koska dynaamisesti tyypitettyjen kielten tapauksessa tyyppejä ei kirjoiteta eksplisiittisesti itse ohjelmakoodiin, kannattaa esimerkiksi aliohjelmien ja luokkien rajapinta dokumentoida hyvin esimerkiksi testien ja docstringien avulla. Toki näin kannattaa tehdä myös Javan tapauksessa tyypeistä huolimatta.

Luennolla mainittiin, että staattisesti tyypitetyt kielet tulevat ennemmin tai myöhemmin kehittäjän tielle. Kielten rajoituksia voi kiertää mutta pitemmän päälle näin saa aikaan vain sotkua. Kielen kehittäjän näkökulmasta onkin haaste luoda staattisesti tyypitetty kieli, joka hyppii mahdollisimman vähän kehittäjän silmille.

Nähdäkseni staattisesti tyypitetyt kielet voivat toimia hyvin matalamman tason kielinä (vrt. C). Dynaaminen tyypitys sen sijaan toimii paremmin korkeamman abstraktiotason sisältävissä kielissä. Staattisen tyypityksen tapauksessa teknisiä, matalamman tason asioita tulee pohdittua jo luonnostaan enemmän. Dynaamisen tyypityksen tapauksessa teknisen tason jättää mielellään vähemmälle huomiolle.

Kielessä tulee olla tyyppejä joka tapauksessa. Hyvä kysymys onkin, kuinka monta tyyppiä kielessä tulee olla. Tämä riippuu suoraan kielen käyttötarkoituksesta. Mikäli ollaan tekemisissä matalamman tason kielen kanssa, voi olla hyvinkin suotavaa, että kielen tyypit on tarkasti mietitty nimenomaan suorituskyvyn kannalta. Korkeamman tason kielessä abstraktiota voidaan viedä suorituskyvyn kustannuksella korkeammalle tasolle. Ääriesimerkkinä Lua sisältää vain yhden lukutyypin, joka on toteutettu doublena. Perinteistä kokonaislukutyyppiä kielessä ei ole siis lainkaan. Toisaalta esimerkiksi C sisältää laajan kokoelman eri lukutyyppejä.

Luennolla esitettiin myös formaaleja tapoja esittää tyypillinen (siis kieli, joka sisältää tyyppejä) kieli. Oleellista määritelmissä on se, että niiden avulla muodostaa helposti ohjelmakoodiksi muuttuva rajoittimien joukko, jonka avulla tyyppeihin liittyvät tarkistukset voidaan tehdä. Rajoittimet voidaan esittää loogisina päättelylauseina, jotka olivatkin jo tuttuja aiemmalta luennolta. Ajatuksena on, että tietyllä ehdolla voidaan tehdä jotain. Karkeasti yksinkertaistettuna summa 5+8 voidaan esittää sääntönä, joka tarkistaa, että summa muodostuu tekijöistä, joiden kummankin tyyppi on luku.

Staattiset tyyppijärjestelmät vaikuttavat varsin yksinkertaisilta näin äkkiseltään. Kompleksisuus lienee syntyykin siinä vaiheessa, kun pitää määritellä useita eri tyyppejä ja miettiä mahdollisia eri operaatioita, joiden avulla tyypitettyjä muuttujia sallitaan käsiteltävän.