Luento 10 - Lisää tyyppiteoriaa

Tällä kertaa pidettiin erittäin matemaattisesti orientoinut luento. Olennaisesti esitettiin staattisten tyyppijärjestelmien teoreettista perustaa. Tässä yhteydessä en aio käydä todistuksia läpi ja tästä tulleekin lyhin postaus tähän asti kirjoitetuista.

Olennaisin kysymys tämän postauksen kannalta lieneekin mitä opin luennolla, onhan kyseessä oppimispäiväkirja. Intuitiivisesti voi tuntua selvältä, että vahvasti tyypitetty kieli ei tuota ajonaikaisia (dynaamisia) virheitä vaan kaikki tyyppivirheet saadaan kiinni käännösvaiheessa. Kuitenkin asian todistaminen ei ole aivan vaivatonta, kuten luennolla näin.

Kenties tähän asti mystisin esitetty asia oli Hindleyn ja Milnerin tyyppipäättely. Tässä tapauksessa tyypit nimenomaan päätellään niiden käyttökontekstin perusteella.

Luennolla mainittiin myös Curry-Howard vastaavuudesta (Curry-Howard correspondence), jonka ajatuksena on, että ohjelmoinnista tuttuja tyyppejä ja ohjelmia vastaavat matematiikan puolella väittämät ja todistukset. Ohjelmointi on jossain mielessä matematiikkaa ja todistaminen taas ohjelmointia. Tästä varmaan seuraa myös, että matematiikkaa voidaan muuntaa ohjelmiksi ja toisinpäin. Toisin sanoen koodin toimivuus voidaan todistaa, mikä sinällään on ihan järkeenkäypää. Vaikeampi kysymys onkin onko mahdollista kirjoittaa kääntäjä, joka muuttaisi todistuksia haluttuun kieleen ja toisinpäin.

Todistuksista voisin mainita vielä sen verran, että äkkiseltään katsottuna ne näyttävät erittäin vaikeaselkoisilta. Tämä kuitenkin johtuu vain niiden korkeasta abstraktiotasosta. Matemaattinen notaatio on erittäin tiivistä. Luentojen välisellä tauolla kävinkin keskustelua notaation kääntämisestä konkreettiseksi suomeksi, mikä sinällään madalti todistusten ymmärtämisen kynnystä. Asiat ymmärtäisi ehkä kenties vielä paremmin, jos oikeasti joutuisi rakentamaan niihin pohjautuvia kieliä.