Obsahom predmetu Teória typov je úvod do základných pojmov, definícii, vlastnosti a technik používaných v typových systémoch.
Ciele predmetu:
- teoreticky - osvojiť si základne princípy a formálne prístupy používane v teórii typov,
- pragmaticky - použitie typových systémov v programovacích jazykoch a prekladačoch.
Použite metódy:
- výpočtový základ tvorí λ-kalkul,
- pri každej konštrukcii jazyka λ-kalkulu nás zaujíma:
- motivácia - pre čo bola konstrukcia zavedena,
- syntax, typovanie a sémantika,
- otázky implementácie z hladiska navrhu kontroly resp. odvodenia typov.
Stručná osnova predmetu:
- Základné pojmy teórie typov.
- Netypovaný jazyk čísel a pravdivostných hodnôt, NBL.
- Netypovaný λ-kalkul.
- Typovaný NBL.
- Jednoducho typovaný lambda kalkul.
- Odvodené tvary termov.
- Súčinové a súčtové typy.
- Rekurzia a rekurzívne typy.
- Referenčné typy.
- Výnimočné situácie.
- Podtypy.
- Závislé typy.
- Polymorfné typy.
- Typová rekonštrukcia - odvodenie typu.
- Systém F, Let polymorfizmus
Organizácia predmetu
- Pre úspešné absolvovanie predmetu je potrebné získať minimálne 16 bodov z 30 v priebežnom hodnotení a minimálne 36 bodov zo 70 v rámci skúšky.
Zápočet
- 30 bodov.
Skúška
- 70 bodov.
Vyučujúci
Garant predmetu:
Prednášky a cvičenia:
Odporúčaná literatúra:
- B.C.Pierce: Types and programming languages, MIT Press, Cambridge, 2001 (Перевод на русский язык: Бенджамин Пирс. Типы в языках программирования. — Добросвет, 2012. — 680 с. — ISBN 978-5-7913-0082-9)
- B.C.Pierce et al.: Software Foundations, Electronic textbook, 2024
- Valerie Novitzká, Daniel Mihályi: Teória typov, TU Košice, 2015
- J.-Y. Girard: Proofs and types, Cambridge Univ.Press, 1989
- J.R.Hindley: Basic simple type theory, Cambridge Univ.Press, 1997
- R.Sethi: Programming Languages, WileyaSons, 1996
- W.Horowitz: Higher-order Programming Languages, WileyaSons, 1982
- Введение. Функциональное и императивное программирование: Computer Science Center, 2015