Seminaari 58303101: Tyyppiteoria ja ohjelmointikielet (2 ov).

1. Aihepiiri

Tyyppiteoria (type theory) on eräs matemaattisen logiikan haara, jota on viime aikoina alettu soveltaa myös ohjelmointikieliin. Tyyppiteoriaa on nimensä mukaisesti käytetty erityisesti olemassaolevien ohjelmointikielten tyyppijärjestelmien analysointiin ja uusien (varsinkin funktionaalisten) ohjelmointikielten tyyppijärjestelmien suunnitteluun. Tämän seminaarin tarkoituksena on tutustua alan alkeisiin.

2. Asema opetuksessa

Seminaari sopii erityisesti seuraavista aihepiireistä kiinnostuneille:

Ohjelmistojen erikoistumislinja:

ohjelmointikielten kääntäjät, ohjelmointikielten teoria.

Algoritmien erikoistumislinja:

vaihtoehtoiset laskentamallit, ohjelmoinnin teoria, päättelyjärjestelmät ja logiikat.

Kyseessä on opintoseminaari, johon ei ole ehdottomia esitietovaatimuksia. Logiikan alkeiden tuntemuksesta (esim. Matematiikan laitoksen kurssilta ''Logiikka I'') on tosin hyötyä, samoin funktionaalisen ohjelmoinnin perusteista (esim. laitoksen kurssilta ''Symbolinen ohjelmointi'').

Osa materiaalista on luonteeltaan teoreettisempaa, osassa taas voi halutessaan tutustua näiden teoreettisten ideoiden tietokonetoteutuksissa käytettyihin tekniikoihin.

Seminaarin vastuuhenkilö on vt.prof. Matti Nykänen.

3. Kokoontumiset

Seminaari kokoontuu kevätlukukaudella 2003 yleensä torstaisin klo 14:15-16:00 salissa A320 ellei alla toisin mainita (poikkeukset lihavoitu). Aikataulu on seuraava:

päivä	esitelmöijä	esitelmä
16.01.	Nykänen, Matti	Seminaarin järjestäytyminen.
30.01.	Huovinen, Marja	Lambdakalkyylin perusteita.
13.02.	Krannila, Kaisa	Laajennoksia tyypitettyyn lambdakalkyyliin. (Myös PDF-muodossa.)
20.02.	Miettinen, Mika	Alityypityksen teoriaa.
27.02.	Niskakangas, Risto	Alityypityksen metateoria. (Myös PDF-muodossa.)
06.03.	Saarela, Samppa	Rekursiiviset tyypit - teoria. (Myös PDF-muodossa.)
13.03.	Liukkonen, Panu	Rekursiiviset tyypit - algoritmi.
20.03.	Kirmanen, Jani	Tyypinpäättely.
27.03.	Laasonen, Kari	Tyyppikvanttorit.
03.04.	Mansikka, Harri	Tyyppikvanttorit ja alityypitys. (Myös PDF-muodossa.)
29.04. 12-14 B451	Kivekäs, Otso	Tyyppitoimitukset (Kinds). (Laitoskirjaston kirja lainassa.)
08.05. 12-14 A216	Karvonen, Vesa	Tyyppitoimitukset ja alityypitys. (Myös PDF-muodossa.)
08.05. 14-16 A216	Alanko, Lauri	Efektijärjestelmät.

(Aihepiirikoodit selitetään tuonnempana.)

4. Materiaali

Seminaarissa käsitellään seuraavaa vastikään ilmestynyttä oppikirjaa:

Benjamin C. Pierce: Types and Programming Languages. MIT Press, 2002.

Kirjan sisältö voidaan jakaa seuraaviin aihepiireihin. Edellä olevassa aikataulussa on osoitettu lyhentein, mitä aihepiiriä kukin esitelmä koskee.

A: Lambdakalkyylin perusteet.

1. Tyypittämätön ja tyypitetty lambdakalkyyli (luvut 5, 9 ja 12).
2. Yksinkertaiset laajennukset (luvut 11, 13 ja 14).

Tämä aihepiiri muodostaa yhteisen perustan koko loppuseminaarin erikoistuneemmille aihepiireille.

B: Alityypitys.

1. Teoria (luku 15).
2. Algoritmit (luvut 16 ja 17).

Tämän aihepiirin intuitio on, että jos meillä on sellainen operaatio o, joka soveltuu jonkin tyypin T mukaisille alkioille, niin tämä sama o olisi järkevä myös kaikille sellaisille alkioille, joiden tyyppi U sisältää ainakin kaikki tyypin T ominaisuudet. (Tyypillä U saattaa olla myös muita lisäominaisuuksia, mutta operaatio o ei niitä kaipaa ollakseen järkevä.)

C: Rekursiiviset tyypit.

1. Teoria (luvut 20-21.4).
2. Algoritmit (luvun 21 loppuosa).

Tämä aihepiiri käsittelee ohjelmoijan määrittelemiä äärettömiä rakenteisia tyyppejä kuten puita. Se on muista aihepiireistä kuin A erillinen kokonaisuus, joten sen sijoittaminen seminaariaikatauluun on niitä vapaampi.

D: Parametrinen polymorfia.

1. Tyypinpäättely (luku 22).
2. Tyyppikvanttorit (luvut 23 ja 24).
3. D.2 ja B yhdessä (luku 26)

Tämä aihepiiri käsittelee sellaista polymorfian (monimuotoisuuden) lajia, joka esiintyy sellaisissa ohjelmointikielissä kuin ML. Se käsittelee sellaisia operaatioita kuin ''listan pituus'', joiden merkitys on sama riippumatta siitä, mitä tyyppiä T parametrina saadun listan alkiot ovat. Toisin sanoen, ''listan pituus'' on määritelty kaikilla tyypeillä T - eli kvantifioitu yli tyypin T.

(Oliokielten ad hoc eli ''tässä ja nyt'' -polymorfiassa samalla operaatiolla on sitä vastoin eri merkitys eri olioille.)

Osaan D.1 voi käyttää myös (vastuuhenkilöltä löytyvää) kirjaa

J. Roger Hindley: Basic Simple Type Theory. Cambridge University Press, 1997.

E: Tyyppitoimitukset.

1. Tyyppitoimitukset ja D yhdessä (luvut 29 ja 30).
2. E.1 ja B yhdessä (luvut 31 ja 32).

Tämä aihepiiri käsittelee sellaisia ''laskutoimituksia'' kuten array of T, jotka ottavat sisään yhden tyypin T, ja palauttavat arvonaan uuden tyypin ''taulukko jonka alkiot ovat tyyppiä T''.

Jälkimmäinen osa E.2 on itse asiassa laaja esimerkki hypoteettisesta olio-ohjelmointikielen tyyppirakenteesta, ja siinä sovelletaan seminaarin kaikkia muita aiempia aihepiirejä kuin C. Toinen mahdollinen lähde voisi olla esimerkiksi seuraava kirja:

Kim B. Bruce: Foundations of Object-Oriented Languages. MIT Press, 2002.

Kirjaan liittyy läheisesti myös ohjelmointikieli nimeltä O'Caml. Se on eräs ML-kieliperheen (katso aihepiiri D) murre, johon on lisätty oliot (katso aihepiiri E.2).

(Sen pohjana olevasta kielestä Caml löytyy vastuuhenkilöltä oppikirja
Guy Cousineau ja Michel Mauny: The Functional Approach to Programming. Cambridge University Press, 1998.
Tosin kielten välillä on muitakin eroja kuin pelkästään oliot.)

Näin ollen O'Caml on esimerkki siitä, millainen seminaarin aihepiireihin liittyvä ohjelmointikieli voisi olla käytännössä. Lisäksi seminaarin oppikirjan esittelemien tyyppijärjestelmien O'Caml-kieliset toteutukset ovat saatavilla verkosta, ja osa kirjan laskuharjoituksista pyytääkin laajentamaan jotakin toteutusta jollakin kirjassa selostetulla lisäpiirteellä. Jos on kiinnostunut toteutustekniikoista, voi esitelmässään ratkaista ja selittää tällaisia harjoituksia.

Ohjelmointikielen O'Caml Linux-toteutus on asennettu laitokselle hakemistoon /opt/ocaml/.

5. Suoritustapa

Seminaari suoritetaan tavalliseen tapaan pitämällä oma esitelmä, johon liittyy kirjallinen työ, sekä osallistumalla aktiivisesti muuhun seminaaritoimintaan.

Kullakin kokoontumiskerralla pidetään yksi esitelmä.

Esitelmöijä valmistaa esitelmäaiheestaan 10-15 sivun kirjallisen työn, ja palauttaa sen PDF- tai PS-tiedostona viikkoa ennen itse esitelmää vastuuhenkilölle, joka panee sen jakoon muita osallistujia varten tälle sivulle. (Ensimmäisen esitelmäkerran 30.01. työ jaetaan kuitenkin paperilla vasta itse esitelmän aluksi.)

Aktiivinen osallistuminen edellyttää läsnäoloa vähintään 9 kokoontumiskerralla (joita on yhteensä 13). Jos läsnäolosi on mahdotonta jostakin sinusta riippumattomasta syystä (kuten sairaudesta, samanaikaisesta tentistä, tms.) niin ilmoita siitä vastuuhenkilölle (sähköpostitse), mielellään jo etukäteen.

6. Arvostelusta

Tässä seminaarissa ei ole sellaisia tieto/taitomittareita kuin kokeita, tehtyjen laskuharjoitusten määrää, tms. Sen sijaan vastuuhenkilö määrää kullekin osallistujalle arvosanan sillä perusteella, kunka selkeästi hänen kirjallinen työnsä ja suullinen esityksensä onnistuvat selvittämään aiheen sisällön seminaariyleisölle. Tähän auttavat Tieteellisen kirjoittamisen kurssin opit...