PředmětyPředměty(verze: 809)
Předmět, akademický rok 2017/2018
   Přihlásit přes CAS
Funkcionální programování - NAIL097
Anglický název: Functional programming
Zajišťuje: Katedra teoretické informatiky a matematické logiky (32-KTIML)
Fakulta: Matematicko-fyzikální fakulta
Platnost: od 2017
Semestr: zimní
E-Kredity: 3
Rozsah, examinace: zimní s.:2/0 Zk [hodiny/týden]
Počet míst: neomezen
Minimální obsazenost: neomezen
Stav předmětu: vyučován
Jazyk výuky: čeština, angličtina
Způsob výuky: prezenční
Další informace: http://tomkren.cz/fp/
Garant: Mgr. Tomáš Křen
Mgr. Vít Šefl
Třída: Informatika Mgr. - volitelný
Kategorizace předmětu: Informatika > Teoretická informatika
Anotace -
Poslední úprava: T_KTI (10.05.2011)

Základní pojmy, datové struktury a techniky funkcionálního programování, se zaměřením na jejich teoretické základy. Orientace zejména na funkcionální programovací jazyk Haskell.
Cíl předmětu -
Poslední úprava: RNDr. Petr Pudlák, Ph.D. (11.05.2011)

Naučit teoretické základy funkcionálního programování a jejich uplatnění, zejména v prostředí jazyka Haskell.

Upozornit na možnosti zavádění pojmů vysoké abstrakce ve funkcionálních jazycích, které umožňují obecná řešení širokého spektra úloh.

Přínos typových systémů pro korektnost programů.

Literatura -
Poslední úprava: T_KTI (25.04.2016)

  1. Bryan O'Sullivan, Don Stewart, and John Goerzen: Real World Haskell - Code You Can Believe In. O'Reilly, November 2008, ISBN-10: 0596514980, ISBN-13: 978-0596514983.
    http://book.realworldhaskell.org/read/

  2. Paul Hudak: The Haskell School of Expression: Learning Functional Programming through Multimedia Cambridge University Press, New York, 2000, ISBN 0521644089 / 0521643384.

  3. Thompson, S.: Haskell, The Craft of Functional Programming. Addison-Wesley, 1999, ISBN 0-201-34275-8

  4. Benjamin C. Pierce: Types and Programming Languages. The MIT Press, 2002, ISBN 0262162091

  5. Girard J-Y, Lafont Y, Taylor P: Proofs and Types. Cambridge Press, 1989.
    http://www.paultaylor.eu/stable/Proofs+Types.html

  6. Simon Peyton Jones: Haskell 98 language and libraries: the Revised Report. Cambridge University Press, 2003, ISBN 0521826144.
    http://haskell.org/onlinereport/

  7. Barendregt, Henk, Wil Dekkers, and Richard Statman. Lambda calculus with types. Cambridge University Press, 2013.

  8. Paul Hudak: The Haskell School of Music. Yale University, 2008.

Sylabus -
Poslední úprava: T_KTI (25.04.2016)

Úvod do lambda kalkulu, funkcionálního programování a programovacího jazyka Haskell. Operační sémantika funkcionálních programů, beta-redukce a normální formy výrazů (NF, HNF, WHNF).

Funkce jakožto základní prvek funkcionálních jazyků. Rekurzivní funkce, funkce vyšších řádů, kombinátory.

Churchovo kódování datových struktur. Algebraické datové struktury. Rozpoznávání vzorů (pattern matching).

Typované lambda kalkuly. Intuicionistická logika, systém přirozené dedukce a souvislost s typovanými lambda kalkuly. Curry-Howardova korespondence. Základní pojmy kombinatorické logiky. Závislé typy.

Odvozování typů výrazů. Hindley-Milnerův typový systém a algoritmus pro odvozování principiálního (nejobecnějšího) typu. Generování programů požadovaného typu a jeho aplikace.

Ad-hoc polymorfismus - typové třídy. Souvislost s logickým programováním.

Rekurzivní, nekonečné, induktivní a koinduktivní datové struktury. Totální funkcionální programování. Typové systémy popisující dokazatelně totální funkce - Gödelův Systém T a Girard-Reynoldsův Systém F.

Základní pojmy z teorie kategorií v kontextu funkcionálních jazyků. Funktory, Kleisliho kategorie, monády.

Dále volitelně, podle dostupného času:

Typové systémy pro práci s vedlejšími efekty. Monády, unikátní typy, lineární typy a lineární logika.

Rozšíření standardních typových systémů používaná v různých funkcionálních jazycích. Typové systémy v imperativních jazycích. Generalizované algebraické datové typy.

Funkcionální reaktivní programování (FRP).

Stránka předmětu: http://tomkren.cz/fp/, starší verze

http://petr.pudlak.name/fp/

 
Univerzita Karlova | Informační systém UK