58153096-3: Funktionaalisen ohjelmoinnin periaatteet -seminaari (2 ov)

Seminaari on päättynyt, kiitos osanotosta!

Seminaarin järjesti FT Matti Nykänen (sähköposti matti.nykanen@cs.helsinki.fi, huone C481, puhelin 191 44237).

Aihepiiri

Funktionaalinen ohjelmointi on eräs ohjelmointiparadigma esimerkiksi perinteisen proseduraalisen ohjelmoinnin ja logiikkaohjelmoinnin ohella. Sen tavoitteena on laatia, kuvata ja tarkastella ohjelmia "puhtaina" matemaattisina funktioina - mitä ohjelmointikielten "funktiot" eli aliohjelmat eivät välttämättä ole! Tällöin esimerkiksi ohjelmien oikeellisuuden päättely helpottuu.

Seminaarissa käydään läpi funktionaalisen ohjelmoinnin keskeistä taustaa kuten annetun funktionaalisen ohjelman...

• semantiikkaa eli merkitysoppia,
• suorittamista funktioita sisältävän lausekkeen sieventämisenä,
• laiskaa suorittamista,
• tietorakenteita,
• sekä menimuotoista (polymorfista) tyyppirakennetta ja -päättelyä.

Se on suunnattu etupäässä

• algoritmien erikoistumislinjan vaihtoehtoisista laskentamalleista,
• ohjelmistotekniikan erikoistumislinjan ohjelmointikielten teoriasta sekä
• tietojenkäsittelyn ja logiikan välisistä yhteyksistä

kiinnostuneille.

Tämä opintoseminaari esittelee aihepiiriä päälähteenään osia oppikirjasta [Mit96], joka löytyy kirjastomme kurssikirjahyllystä.

Muita kevätlukukauden 2000 saman alueen kursseja ovat

• Teknillisen korkeakoulun seminaari Ohjelmistojen toteutustekniikat ja
• Teoreettisen filosofian laitoksen kurssi Olioiden, luokkien ja perinnän logiikka.

Esitiedot

Osallistujilta ei edellytetä minkään funktionaalisen ohjelmointikielen hallintaa - ei ennen eikä jälkeen seminaarin. Seminaari sivuaa seuraavien kurssien aihepiirejä:

• Laskennan teoria - laskentamallit.
• Tekoälykielet - ohjelmointikieli "Lisp".
• Tekoäly - syksyn 1998 luentojen tiivistelmä ohjelmointikielen Scheme periaatteista.
• Ohjelmointikielten periaatteet - ohjelmointikieli "ML" ja polymorfismi.
• Logiikka 1 (Matematiikan laitos) - päättelyjärjestelmät.

Kokoontumiset

Seminaari kokoontuu torstaisin 20.1.-13.4. klo 10:15-12:00 sekä 4.5.2000 klo 10:30-12:00 laitoksen salissa A320 yhteensä 12 kertaa.

Suorittaminen

Seminaari suoritetaan tavalliseen tapaan

• pitämällä esitelmä jostakin seminaarin aiheesta sen jollakin kokoontumiskerralla,
• laatimalla siitä 10-15 sivun kirjallinen tiivistelmä ja laittamalla se tarjolle tälle sivulle viimeistään viikkoa ennen esitelmää, sekä
• osallistumalla vähintään 7 kokoontumiskertaan.

Aikataulu

pvm.	esitelmöijä	aihe
20.1.	Nykänen, Matti	Järjestäytyminen ja erään ohjelmointiongelman funktionaalinen ratkaisu (sekä sen Haskell-lähdekoodi).
27.1.	Mielikäinen, Taneli	Lambda-laskennan perusteet.
17.2.	Huhmarniemi, Saara	Ohjelmointikielen PCF todistusjärjestelmä.
24.2.	Sjögren, Jan	Tyypitetty lambda-laskenta.
2.3.	Alanko, Lauri	A Glance at Polymorphic Types (sekä sen liite, myös Haskell-lähdekoodina).
9.3.	Uronen, Pekka	Riippuvat tyypit ja konstruktiivinen tyyppiteoria.
16.3.	Tamm, Hellis	Domain-Theoretic Models of Typed Lambda Calculus.
23.3.	Takkunen, Kimmo	Laiska funktionaalinen ohjelmointikieli Haskell.
30.3.	Sarkkinen, Jussi	Jäsennys korkeamman kertaluvun laiskalla ohjelmoinnilla (sekä sen Haskell-esimerkit).
6.4.	Rinta-Mänty, Janne	Tyypit luonnollisen kielen käsittelyssä (ynnä Haskell-esimerkit Jonesin, Hudakin ja Shaumyanin sekä Rannan lähestymistavoista).
13.4.	Kurppa, Teemu	Sovellusaluekohtaisen kielen kehitys funktionaalisella kielellä (sekä sen esittelemä Haskell-animaatiojärjestelmä Windows-ympäristöön).
4.5.	Mäenpää, Petri (Nokia Networks)	Vierailuesitelmä (HUOM! alkaa vasta klo 10:30): Shines: kokemuksia teollisen funktionaalisen ohjelmointikielen suunnittelusta ja toteutuksesta.

Muista myös kurssipalaute!

Esitelmäaiheita

1. Lambda-laskennan perusteet. Varsinkin funktionaalisia (mutta myös muita) ohjelmointikieliä tavataan kuvailla ns. Lambda-laskennalla (Lambda Calculus): päättelyjärjestelmällä sellaisille funktioille jotka voidaan määritellä kirjoittamalla vastaava lauseke. Sen perusteiden [Mit96, luvut 4-4.3.3 ja 4.4.1] tunteminen kuuluu jo lähes alamme yleissivistykseen.
2. Funktionaalisen ohjelman suorittaminen sieventämällä. Funktionaalisen ohjelman suoritusta voi ajatella sitä vastaavan lambda-lausekkeen sieventämisenä (reduction) [Mit96, luvut 2, 3.7 ja 4.4.2-4.4.3]. Erityisesti funktion argumentit voidaan laskea laiskasti (lazy, non-strict) eli vasta kun - tai jos - niitä tarvitaan. Tämä mahdollistaa uudenlaisia ohjelmointitekniikoita.
3. Funktionaalisten ohjelmien merkitysoppia. Lambda-lausekkeille voidaan antaa merkitys esimerkiksi osittainjärjestysten (Complete Partial Order, CPO) avulla [Mit96, luvut 5-5.3]. Samalla saadaan ymmärrettävä selitys rekursiolle.
4. (Melkein) funktionaalisen ohjelmointikielen formaali suoritusmekanismi. Edellisen kaltaisilla välineillä voidaan kuvata myös todellisten ohjelmointikielten semantiikkaa, esimerkkinä scheme [AS96,KCR98,HPR98].
5. Mutkikas tyypitys. Funktionaalisella ohjelmointikielellä kirjoitetun lausekkeen tyypin määrääminen [Hin97, luku 3][Mit96, luvut 4.3.5 ja 11][Tho99, luku 13] on mutkikasta kahdesta syystä: (i) Se saattaa sisältää korkeamman kertaluvun (higher-order) funktioita, eli sellaisia jotka saavat argumentteinaan ja/tai palauttavat arvoinaan toisia funktioita - joilla myös on omat tyyppinsä. Matemaattinen esimerkki on derivaattaoperaattori D_x: se saa argumenttinaan funktion reaaliluvuilta reaaliluvuille, ja palauttaa arvonaan toisen funktion samoin reaaliluvuilta reaaliluvuille. (ii) Se saattaa sisältää myös monimuotoisia eli polymorfisia funktioita, eli sellaisia joiden tyypit on määrätty vain osittain. Esimerkiksi funktio "listan y pituus" on määritelty jokaiselle listalle y, olivatpa sen sisältämät alkiot mitä tyyppiä t hyvänsä, joten sen tyyppi on "t-listoilta luonnollisille luvuille kaikilla tyypeillä t".
6. Kaavat ja tyypit. Tuo tyypitys on vaikeaa, koska se on itse asiassa sama asia kuin todistaminen eräässä logiikassa [Hin97, luku 6][Mit96, luvut 4.3.4 ja 9.1.4][GTL89, luku 3].
7. Yleistetty monimuotoisuus. Edellä mainittua hyvin yksinkertainen monimuotoisuus voidaan laajentaa "oikeaksi" monimuotoisuudeksi jolloin saadaan entistäkin abstraktimpia tyyppirakenteita. [Mit96, luku 9][GTL89, luku 9]
8. Tyyppiteoria ja ohjelmointi. Tyypitystä voidaan kehittää yhä ilmaisuvoimaisemmaksi, jolloin ohjelmien määrittelyt (spesifikaatiot) voidaan esittää tyyppeinä ja tarkistaa ne automaagisesti, tai jopa johtaa ohjelmia määrittelyistään. [Bac90,CNS⁺94][Mit95, luvut 9.1.3. ja 9.1.4][Ran94, luvut 1,2 ja 8]
9. Laiska funktionaalinen ohjelmointikieli Haskell. [Tho99] Se on iso, se on konservatiivinen, se on standardoitu ... se on funktionaalisen maailman Ada! Laitoksellamme on Linux-versio Haskell-tulkista hugs, joka käynnistyy komennolla ''/opt/hugs98/bin/hugs''.
10. Jäsennys korkeamman kertaluvun laiskalla ohjelmoinnilla. Kun käytössämme on sekä korkeamman kertaluvun funktiot että laiska sieventäminen, saamme rekursiivisesti etenevän jäsentäjän pelkästään lukemalla annettu kielioppi funktionaalisena ohjelmana [Hut92,KoP98,Oka98a][Tho99, luku 17.5].
11. Jäsennys ja järjestys. Toisaalta lausekkeen sievennysjärjestys on vapaa, toisaalta taas "ulkomaailmaan" liittyvät tapahtumat kuten syötteen luku ja tulosten kirjoitus [Wad97, luku 2] pitäisi tehdä tietyssä järjestyksessä. Jäsennyksestä on lyhyt matka monadeihin [HM98a,HM98b], jotka tarjoavat erään ratkaisun tähän(kin) ongelmaan.
12. Soveltavaa kielitiedettä? Luonnollisen kielen tietokonejäsentämistä voi lähestyä myös "funktionaalisesti" tyyppien kautta [JoH95,Ran94,ShH97].
13. Laiskan funktionaalisen ohjelmointikielen toteuttaminen. [Pey92,ApS96]
14. Funktionaalisen ohjelman suoritus verkonkudonnalla. Funktionaalista ohjelmaa voi suorittaa sieventämällä paitsi lauseketta myös verkkoa [ESP97]. Samalla saadaan eräs toinen ratkaisu suoritusjärjestysongelmaan [MJB⁺99, luku 4.3][Wad97, luku 3.3].
15. Onko funktionaalinen ohjelma välttämättä tehoton? [Pip97,BJM97]
16. Funktionaalisia tietorakenteita. Chris Okasakin mukaan "First, from the point of view of designing and implementing efficient data structures, functional programming's stricture against updates (i.e., assignments) is a staggering handicap, tantamount to confiscating a master chef's knives. ... The second difficulty is that functional data structures are expected to be more flexible than their imperative counterparts." [Oka98b, luku 1.1] Näihin haasteisiin voi vastata eri tavoin:
    • Suunnittelemalla funktionaalisia vastineita imperatiivisille tietorakenteille, kuten jonoille (queues) [Oka98b, luvut 5.2, 6.3.2, 6.4.2, 7.2, 8.2.1, 8.4, 10.1.3 ja 11.1-11.2], keoille (heaps) [Oka98b, luvut 3.1-3.2, 5.3-5.5, 6.4.1, 7.3, 9.3.2 ja 10.2.2], tai hajasaantilistoille (random access lists) [Oka98b, luvut 9.2.1,9.3.1 ja 10.1.2].
    • Kehittämällä funktionaalisten kielten laiskan suoritusmekanismin huomioivia algoritmianalyysimentelmiä [Oka98b, luvut 5-6].
    • Kehittämällä suunnittelumetodeja joille laiska suoritus onkin etu eikä haitta [Oka98b, luvut 7-8]
    • Mallintamalla tietorakenteita aritmetiikalla [Oka98b, luvut 9 ja 11].
17. Funktionaalinen robotti. Robotiikka on tila- ja komentoperustaista ohjelmointia. Vai onko? [PHE98]

Materiaalia

AS96

Abelson,H. ja Sussman,G.J.: Structure and Interpretation of Computer Programs, toinen painos. MIT Press. 1996.

ApS96

Appel,A.W. ja Shao,Z.: An Empirical and Analytic Study of Stack vs. Heap Cost for Languages with Closures. Journal of Functional Programming 6(1), ss. 47-74, 1996.

Bac90

Backhouse,R.C.: Constructive Type Theory: A Perspective from Computing Science. Sivut 1- 32 teoksessa E.W. Dijkstra (toim.) Formal Development of Programs and Proofs. Addison-Wesley, 1990.

BJM97

Bird,R., Jones,G. ja de Moor, O.: More Haste, Less Speed: Lazy versus Eager Evaluation. Journal of Functional Programming 7(5), ss. 541-547, 1997.

CNS⁺94

Coquand,T., Nordström,B., Smith,J.M. ja von Sydow,B.: Type Theory and Programming. Bulletin of the EATCS 52, 1994.

ESP97

van Eekelen,M., Smetsers,S. ja Plasmeijer,R.: Graph Rewriting Semantics for Functional Programming Languages. Proceedings of the Fifth Annual Conference of the European Association for Computer Science Logic (EACSL) (CSL'96) ss. 106-128, 1997.

GTL89

Girard,J-Y., Taylor,P. ja Lafont,Y.: Proofs and Types. Cambridge University Press, 1989.

Hin97

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

HPR98

Honsell,F., Pravato,A. ja Ronchi Della Rocca,S.: Structured Operational Semantics of a fragment of the language Scheme. Journal of Functional Programming 8(4), ss. 335-365, 1998.

Hut92

Hutton,G.: Higher-Order Functions for Parsing. Journal of Functional Programming 1(1), ss. 323-343, 1992.

HM96a

Hutton,G. ja Meijer,E.: Monadic Parsing in Haskell. Journal of Functional Programming 8(4), ss. 437-444, 1998.

HM96b

Hutton,G. ja Meijer,E.: Monadic Parser Combinators. Tutkimusraportti NOTCS-TR-96-4, Nottinghamin yliopisto, 1996.

JoH95

Jones,M.P. ja Hudak,P.: Using Types to Parse Natural Languages. Proceedings of the Glasgow Workshop on Functional Programming, 1995.

KCR98

Kelsey,R., Clinger,W. ja Rees,J. (toim.): Revised⁵ Report on the Algorithmic Language Scheme. ACM SIGPLAN Notices 33(9), ss. 26-76, 1998.

KoP98

Koopman,P. ja Plasmeijer,R.: Efficient Combinator Parsers. Implementation of Functional Languages (IFL'98) ss. 122-138, 1998.

MJB⁺99

de Mast,P., Jansen,J-M., Bruin,D., Fokker,J., Koopman,P., Smetsers,S., van Eekelen,M. ja Plasmeijer,R. Functional Programming in Clean. Käsikirjoitus, heinäkuu 1999.

Mit96

Mitchell,J.C.: Foundations for Programming Languages. MIT Press, 1996.

Oka98a

Okasaki,C.: Even Higher-Order Functions for Parsing or Why Would Anyone Ever Want To Use a Sixth-Order Function? Journal of Functional Programming 8(2), ss. 195-199, 1998.

Oka98b

Okasaki,C.: Purely Functional Data Structures. Cambridge University Press, 1998.

PHE98

Peterson,J., Hudak,P. ja Elliott,C.: Lambda in Motion: Controlling Robots in Haskell. Practical Aspects of Declarative Languages (PADL'99) 1998, ss. 91-105.

Pey92

Peyton-Jones,S.L.: Implementing Lazy Functional Languages on Stock Hardware: the Spineless Tagless G-Machine. Journal of Functional Programming 2(2), ss. 127-202, 1992.

Pip97

Pippenger,N.: Pure versus Impure Lisp. ACM Transactions on Programming Languages and Systems 19(2), ss. 223-238, 1997.

Ran94

Ranta,A.: Type-Theoretical Grammar. Oxford University Press/Clarendon Press, 1994. (Lainassa Janne Rinta-Männyllä; eräpäivä 13.3.2000.)

ShH97

Shaumyan,S. ja Hudak,P.: Linguistic, Philosophical, and Pragmatic Aspects of Type-Directed Natural Language Parsing. Proceedings of the Conference on Logical Aspects of Computational Linguistics, 1997.

Tho99

Thompson,S.: Haskell: the Craft of Functional Programming, toinen painos. Addison-Wesley, 1999.

Wad92

Wadler,P.: How to Declare an Imperative. ACM Computing Surveys 29(3), ss. 240-263, 1992.