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 2018
• Semestr: zimní
• E-Kredity: 3
• Rozsah, examinace: zimní s.:2/0, Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: čeština, angličtina
• Způsob výuky: prezenční
• Způsob výuky: prezenční
• Další informace: http://tomkren.cz/fp/
• Garant: Mgr. Vít Šefl; Mgr. Tomáš Křen
• Třída: Informatika Mgr. - volitelný
• Kategorizace předmětu: Informatika > Teoretická informatika

Anotace

čeština

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.

angličtina

Poslední úprava: T_KTI (10.05.2011)

Basic notions, data structures and techniques in functional programming, focused on its theoretical foundations. Oriented mainly towards functional programming language Haskell.

Cíl předmětu

čeština

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ů.

angličtina

Poslední úprava: RNDr. Petr Pudlák, Ph.D. (11.05.2011)

Learn theoretical foundations of functional programming and their uses, in particular in the environment of Haskell language.

Draw the attention to possibilities of introducing notions of high abstractions in functional languages that allow general solutions of broad spectrum of tasks.

Contribution of type systems for program correctness.

Podmínky zakončení předmětu

čeština

Poslední úprava: RNDr. Jan Hric (12.06.2019)

Ústní zkouška. Požadavky ústní zkoušky odpovídají sylabu předmětu v rozsahu, v němž byl prezentován na přednášce.

angličtina

Poslední úprava: RNDr. Jan Hric (12.06.2019)

Oral examination. Questions posed in the oral examination explore the topics included in the syllabus to the extent that these topics are covered in lectures.

Literatura

čeština

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

čeština

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/

angličtina

Poslední úprava: T_KTI (25.04.2016)

Introduction to lambda calculus, functional programming and the Haskell programming language. Operational semantics of functional programs, beta-reduction and normal forms of expressions (NF, HNF, WHNF).

Functions as first-class objects of functional languages. Recursive functions, higher-order functions, combinators.

Church encoding of data types. Algebraic data structures. Pattern matching.

Typed lambda calculi. Intuitionistic logic, natural deduction calculus and its connection to typed lambda calculi. Curry-Howard correspondence. Basic notions of combinatory logic. Dependent types.

Expression type inference. Hindley/Milner type system and principal type inference algorithm. Generating expressions of given type and its applications.

Ad-hoc polymorphism - type classes. Connection to logic programming.

Recursive, infinite, inductive and coinductive data structures. Total functional programming. Type systems describing provably total functions - Gödel System T and Girard-Reynold System F.

Basic notions from category theory in the context of functional languages. Functors, Kleisli category, monads.

Facultative topics:

Type systems for working with side effects. Monads, unique types, linear types and linear logic.

Extension of standard type systems used in various functional languages. Type systems in imperative languages. Generalized algebraic data structures.

Functional reactive programming (FRP).

Web page: http://tomkren.cz/fp/, older web page: http://petr.pudlak.name/fp/.