Engaging, Large-Scale Functional Programming Education in Physical and Virtual Space: Syllabus

Table of Links

1 Introduction

2 Course Structure and Conditions

2.1 Conditions

2.2 Syllabus

3 Lectures

4 Practical Part

4.1 Engagement Mechanisms

4.2 Technical Setup and Automated Assessment

4.3 Selected Exercises and Tools

5 Check Your Proof by Example

6 Exams

7 Related Work

8 Conclusion, Acknowledgements, and References

2.2 Syllabus

The course deals with the basics of functional programming and the verification of functional programs. Most parts of the course could be done using any functional language. We chose Haskell because of its simple syntax, large user community, and good testing facilities (in particular QuickCheck). The syllabus stayed close to the one presented in [4]. The changes are the omission of the parser case study, the rigorous introduction of computation induction and type inference, and the decision to split off I/O from monads and introduce it earlier. The last is done in an effort to convince students more quickly that pure functional languages can be practical and deal with side effects. For ease of reference, we list the syllabus below. New or modified topics are marked (∗):

1. Introduction to functional programming

   
   

2. Basic Haskell: Bool, QuickCheck, Integer and Int, guarded equations, recursion on numbers Char, String, tuples

   
   

3. List comprehension, polymorphism, a glimpse of the Prelude, basic typeclasses (Num, Eq, Ord), pattern matching, recursion on lists (including accumulating parameters), scoping by example

   
   

4. Proof by structural induction and computation induction on lists (∗)

   
   

5. Type inference algorithm (∗)

   
   

6. Higher-order functions: map, filter, foldr, λ-abstractions, extensionality, currying

   
   

7. Typeclasses

   
   

8. Algebraic datatypes and structural induction

   
   

9. Concrete I/O without introducing monads (∗)

   
   

10. Modules: module syntax, data abstraction, correctness proofs

    
    

11. Case studies: Huffman codings, skew heaps

    
    

12. Lazy evaluation and infinite lists

    
    

13. Complexity and optimisation

    
    

14. Monads (∗)

Concepts are introduced in small, self-contained steps. Characteristic features of functional programming languages such as higher-order functions and algebraic data types are only introduced midway through the course. This makes the design of interesting practical tasks harder but ensures that students are not overwhelmed by the diversity of new principles that are not part of introductory imperative programming courses. In general, the course progresses from ideas close to what is known from imperative languages (e.g. boolean conditions, recursion on numbers, auxiliary functions, etc.) to simple applications of new concepts (e.g. recursion and induction on lists) to generalised new concepts (e.g. algebraic data types and structural induction).