IA014 Advanced Functional Programming
Lecture IX - Dependent types
Lecture dates
19. 5. 2021
Reading
Programming in IDRIS: A Tutorial [PDF]
Read Section 3. Types and Functions
A. Bove, P. Dybjer: Dependent Types at work. [PDF]
Additional material
Read the materials explaining how to simulate dependent types in Haskell using GADTs, type families etc. in Lecture VIII.
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/fi/jaro2021/IA014/um/09-dependent.pdf
Lecture recordings
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/fi/jaro2021/IA014/um/vid/2021-05-19_ia014.mp4