Lecture dates

12. 5. 2020

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.

Video recordings

Dependent types - introduction

Introduces the dependent types as the 'missing' combination of types and terms; reviews the lambda cube; basic  definitions; dependently-typed programming languages.

Dependent types - vectors

Introduces the most common dependent type - vectors; short discussion of Idris syntax; some functions over vectors; matrices.

Dependent types - finite sets

The second most common dependent type and its use for indexing; implicit parameters in terms with dependent types.

Dependent types - dependent pairs

Explains the trickiest (and the most strange) dependent type - dependent pairs; typical use case - filter.