Syllabus + Lecture Schedule

[bkc39]

Ok, we are finally getting this repo up to a point where we can start writing lecture notes. I think we should agree on what topics we plan to cover as well as the individual lectures that we plan to write so that we can start making issues and working on these individually.

Here is a rough outline for how I think that this should go. I think we should model the course at a high level off of the version offered by Nate in 2014sp. He has 6 high level topics:

1. Introduction to Functional Programming
2. Mutability
3. Formal Verification
4. Asynchronous Programming
5. Analysis of Algorithms
6. Advanced Topics

Here are my feelings:

• Cut out the Asynchronous Programming part.
• Cut Analysis of algorithms.
• Have formal verification be treated in an integrated way with the rest of the course.
• Have advanced topics be integrated throughout the course as optional sections within the notes.

At a high level I think our syllabus should look like:

1. Introduction to Functional Programming
2. Data Structures
3. Side Effects

Here is the lecture schedule that I propose:

1. Introduction To Functional Programming
   • Expressions and their evaluation.
   • Intuitionistic Propositional Logic
   • The Curry Howard Isomorphism
   • Natural Numbers and Induction
   • Lists and Induction
   • Trees and Induction
2. Data Structures
   • Common Abstract Data Types
     • Stack
     • Queue
     • Heap
     • Set
     • Map
   • Self-Balancing Binary Trees
     • Splay Tree
     • 2-3 Tree
     • Red/Black Tree
   • Algebraic Properties of Data Types
     • Functors
     • Pointed and Applicative Functors
     • Foldable types
     • Traversable types
     • Introduction to Category Theory
3. Side Effects
   • Mutable References and Pitfalls of Side Effects
   • Semantics of IMP via translation to a functional language
   • Monads
   • Monad Transformers
   • Free Monads and Abstract Interpretation

Here is my rationale for the above:

• The goal is to give a very thorough introduction to the fundamentals of programming and proof in the introduction and the concrete data structure part of the course.
• The algebraic stuff (functor hierarchy) will be a natural generalization of the concepts that were already seen up to that point.
• Side effects will basically consist of an overview of why side effects are hard to reason about followed by an in-depth case study focusing on how imperative side-effects translate into a functional context.
• The monad pattern will generalize and unify what was seen in both the algebraic theory, and the theory of side effects.
• We will encapsulate computations with different types of effects using monad transformers.
• Free monads will be the tool to write abstract interpreters that generalize the translation from IMP to a functional language (probably lambda calculus++). The idea will be to use this abstraction to re-implement the same IMP interpreter in a cleaner, more sensible way.

This totals 24 lectures, compared to the 27 lectures and 27 recitations of CS 3110. Overall, I think this syllabus better reflects the title Functional Programming and Data Structures.

We should discuss and finalize this syllabus ASAP so we can begin working on writing the notes.

[bkc39]

Oh as a note, I think that predicate logic will naturally be included during the " and Induction" lectures. We could just have a brief subsection talking about how to extend IPL with the relevant judgments. Identity and refl will be treated similarly, although we may want to include that in the treatment of IPL.

[bennn]

For 1, I was thinking

• type definitions, pattern matching, recursion
• testing (ps1 due)
• polymorphism aka "let's stop repeating ourselves"
• induction aka "we can do better than testing" (ps2 has fold + induction problems)

[bennn]

• ps1 should be due after lecture 2

Also I think the rest of the lectures are great. We may want to turn up on more data structures, or write typed / dep.typed interpreters as the final, but this is exactly what I was thinking (monads included) for the core of the course.

[bkc39]

Ok, I agree that the beginning may have IPL sort of coming out of left field and perhaps it will be a bit unmotivated to a novice. I think using Curry-Howard is a good way to introduce programming and proving simultaneously, even if the deeper implications are ignored at the beginning or put in a black diamond section. Basically,

• Polymorphism follows as a direct consequence of the negative fragment where type variables translate to propositional variables.
• Sum and Product types also follow naturally from the negative and positive fragment, respectively.
• Type definitions, pattern matching and recursion would all be bundled into "_ + Induction".
• Recursion and induction get introduced simultaneously as two sides of the Curry-Howard isomorphism extending the connection already built in lectures 1 and 2.
• General data types get added following the same scheme as Nat, List and Tree, namely:
  1. Make a recursive definition in code.
  2. Define a type formation judgment for the type you just defined.
  3. Define the elimination form (induction principle) for the new proposition corresponding to your type.

This way our treatment of algebraic data types and structural induction are all instances of the same unifying framework. I think that the benefits of this make up for the apparent non-sequitur in Lecture 2.

Also, I agree that testing should be covered in the beginning. The question is how to integrate it correctly.

I haven't given any thought to how the problem set schedule would correspond to this. The only thing I know is that PS 1 gets released on the day of the first lecture. We should probably make a separate issue to talk about problem sets though.