CSCI 365Functional Programming

Time

MWF 8:10pm - 9:00am (A1)

MC Reynolds 317

Instructor

Dr. Brent Yorgey
yorgey@hendrix.edu
(501) 450-1377
Office Hours

Image by Chor Ip, CC-BY-SA-2.0

Overview

Functional programming takes as its central organizing principle the idea of evaluating expressions rather than executing instructions. It supports programming at a high level of abstraction and carefully controlling side effects, which are critical given the ever-increasing sophistication of software systems. This course explores functional programming in depth, with a unifying focus on recursion. It combines practical programming experience in Haskell with a deep exploration of the underlying theory. Covered topics include algebraic data types and pattern matching, static type systems, recursion and induction, folds, lambda calculus, laziness, functors, and monads. A few weeks will also be spent learning about computer-checked formal proofs using the dependently typed functional language/proof assistant Agda.

Learning Goals

Upon completing this course, you will be able to:

• Induction and recursion
• Design appropriate recursive data types to model data
• Write recursive programs over recursive data types in Haskell and Agda
• Carry out inductive proofs about recursive data types, in English and in Agda
• Explain the relationship between folds and induction
• Type systems
• Produce typing derivations for terms of the simply typed λ-calculus
• Use types to aid in constructing and reasoning about Haskell and Agda programs
• Use the logical interpretation of types (the Curry-Howard isomorphism) to reason about types and encode mathematical propositions in the type system of Agda
• λ-calculus
• Explain the historical and continuing role of the λ-calculus as a foundational model of logic and computation
• Become comfortable with the mechanics of the λ-calculus as a model of computation:
• Compute the normal form of any λ-calculus term
• Encode algebraic data types in the λ-calculus via Church encoding
• Implement recursive definitions in the λ-calculus using the Y combinator
• Write moderately sophisticated Haskell programs to solve specific problems, using tools such as algebraic data types and pattern-matching
• Design, use, and prove properties of recursion patterns such as maps, filters, and folds
• Agda
• Write basic data type and function definitions in Agda
• Translate back and forth between logical statements expressed in English and as Agda types
• Carry out inductive proofs in Agda

Resources

• You will need to install a Haskell toolchain on your computer. Follow these instructions to install GHCup, which is a tool for managing all the major components of a Haskel toolchain (GHC, cabal, stack, haskell-language-server, etc.).

• For editing Haskell code, I recommend using Visual Studio Code, which has excellent Haskell support. But if you have a different favorite editor, it will probably work with Haskell just fine.

• You should follow this style guide when writing Haskell code in this class.

• If you would find it helpful to have a textbook, try Graham Hutton’s Programming in Haskell. Not everything we will cover is in there but it has significant overlap.

• Haskell Programming from first principles is another Haskell book which has been getting good reviews, and seems quite comprehensive, though I have not personally looked at it.

• Many people from the Haskell community are active on StackOverflow, which can be a good place to ask questions.

• The Haskell-beginners mailing list is a good place to ask beginner-level questions.

• The Haskell-cafe mailing list can also be a good place to ask questions, but is much higher-traffic.

• The Typeclassopedia explains many of the type classes in the standard libraries (Functor, Applicative, Monad, Monoid, Arrow, Foldable, Traversable…).

• The Haskell wikibook actually contains a substantial amount of well-written information; a great resource if you’re having trouble understanding a particular topic and want a different approach.

• There is a Haskell subreddit for aggregating Haskell-related websites, blog posts, and news.

• Hackage is the standard package database for Haskell with a wide variety of applications and libraries.

• Looking for a function but don’t know what it’s called? Want to see the documentation for a particular function? Hoogle searches many standard libraries and can search either by name or by type.

• If you really want the nitty-gritty details of the Haskell language standard, see the 2010 Haskell report.

Calendar

Date Topic In-class code Notes
F 21 Jan Lists part 1 part 2 Haskell.hs

M 24 Jan Algebraic data types ADT.hs
W 26 Jan Thinking functionally; inference rules FunctionalThinking.hs
F 28 Jan Propositional logic

M 31 Jan Propositional logic, part 2
W 2 Feb Polymorphism Polymorphism.hs
F 4 Feb No class (snow)

M 7 Feb List recursion patterns RecursionPatterns.hs
W 9 Feb Folds RecursionPatterns.hs
F 11 Feb Currying Currying.hs

M 14 Feb λ calculus: definitions   Lambda calculus (video)
W 16 Feb λ calculus: encoding bool Church.hs
F 18 Feb λ calculus: encoding bool, nat Nat.hs

W 23 Feb fix and the Y combinator Fix.hs Y combinator (video)
F 25 Feb Simply typed lambda calculus

M 28 Feb The Curry-Howard isomorphism
W 2 Mar Introduction to Agda Agda workspace
F 4 Mar More Agda: negation and equality intro.agda

M 7 Mar More Agda: isEven
W 9 Mar Agda: proving properties of functional programs
F 11 Mar Agda: equational reasoning eqreasoning.agda

M 14 Mar Review
W 16 Mar No class
F 18 Mar STLC in Agda STLC.agda

M 28 Mar Wholemeal programming Wholemeal.hs
W 30 Mar no class
F 1 Apr More wholemeal programming Wholemeal.hs

M 4 Apr Type classes TypeClasses.hs
W 6 Apr Monoids TypeClasses.hs
F 8 Apr Monoidal trees Tree.hs Monoids and finger trees

M 11 Apr Kinds and Functor Kinds.hs Functor.hs
W 13 Apr More Functor instances Functor.hs
F 15 Apr Semantic editor combinators Functor.hs

M 18 Apr Introduction to Applicative Applicative.hs
W 20 Apr More Applicative Applicative.hs
F 22 Apr Yet More Applicative Applicative.hs

M 25 Apr Making a Haskell app, part 1 guess.tgz
W 27 Apr Making a Haskell app, part 2 guess2.tgz
F 29 Apr Making a Haskell app, part 3: hangman hangman.tgz

Coursework and policies

This course uses specifications grading. Briefly, this means that grading of individual assignments is on a credit/no-credit basis, with a specification that tells you what you must do in order to get credit. Your final letter grade in the course, in turn, is determined by the below specification that says what you must complete in order to get each letter grade.

A Complete all modules to level 2
Complete a final project

B Complete all but one modules, at least half to level 2
Complete a final project

C Complete all but two modules to level 1

D Complete at least half of the modules to level 1

Due dates policy

• Every assignment has a specific date and time (usually 5pm) at which it is due.

• Assignments may be turned in any time up to the deadline. I will try my best to return graded assignments, with feedback, within two weekdays of being turned in.

• Assignments will not be accepted after the deadline.

• However, I will automatically grant extensions to anyone who asks. Simply send me an email prior to the deadline, asking for an extension on a particular assignment, and informing me what your new deadline will be. The new deadline should be a specific day and time (“11pm this Saturday, March 5”, not “in a couple days”). I will hold you to the new deadline.

• Yes, this process may be chained: you may ask for another extension prior to your chosen deadline, and so on. The key is communication.
• If you get level 1 credit for an assignment and want level 2 credit, or if you don’t get credit at all, you may revise and resubmit the assignment until you do. There is no deadline for resubmitted assignments.

• However, the above only applies if you made a reasonable attempt at the assignment the first time. You cannot turn in a half-finished assignment before the deadline and then “revise” it by completing the rest. If your assignment is only half-finished, you must request an extension.

• The latest any assignment may be turned in is 5pm on Friday, May 6.

• Exceptions to this policy can be made in cases of emergency, mental health issues, etc. Please come talk to me!

Submission policies

• Problem sets may be completed individually or in groups of up to 3. You may pick your own groups (though I am happy to serve the role of matchmaker if you need help finding a group).

• Assignments must be turned in electronically via the assignment submission form.

• Coding assignments must be turned in as .hs, .lhs, and/or .agda files (.zip or .tar.gz files are OK too).

• Written assignments must be turned in as a PDF. All standard document editing programs have an option for exporting to PDF; if you are unsure how to do this, please ask.

Modules

There will be a number of modules corresponding to topics in the course. Each module consists of one or more problem sets, a quiz, and occasionally some other small assignments. Each module can be completed to one of two levels:

• Level 1 means you have achieved the learning objectives for the module.
• Level 2 means you have somehow gone above and beyond the basic requirements in order to explore the topic in more depth.

Each individual module specifies what you need to do to get Level 1 or Level 2 credit. For example, there may be an extra challenge problem set and/or reading you must complete to get Level 2 credit.

# Module Resources Assigned Due
1 Introduction to Haskell   W 19 Jan W 26 Jan
2 ADTs and proofs Proof.hs W 26 Jan W 2 Feb
3 Polymorphism and recursion patterns   W 9 Feb W 16 Feb
4 Lambda calculus lc.tgz, bool.lc W 16 Feb W 23 Feb
No module week of 23 Feb
5 STLC and Curry-Howard STLC.hs, survey W 2 Mar W 9 Mar
6 Agda   M 14 Mar W 30 Mar
7 Wholemeal programming   W 6 Apr W 13 Apr
8 Monoids starter code W 13 Apr W 20 Apr

Quizzes

There will be 12 weekly short quizzes (typically on Wednesdays) testing you on key aspects of the previous week’s problem set.

Quizzes will be graded on a credit/no credit basis, but you can re-take a quiz as many times as you like until getting credit.

The first opportunity to take a given quiz will be in class, in written form (however, you need not take it if you do not feel prepared). To retake a quiz, just schedule a 15-minute meeting slot, being sure to clearly indicate which quiz or quizzes you intend to retake.

Final project

Overview/important dates

You may complete a final project which extends or ties together some of the things we have learned over the course of the semester. A final project is required to get an A or B in the course.

Important dates:

• Monday, April 18 – Project proposals due
• April 25–29 – Checkpoint meetings
• Friday, May 6, 2:00-5:00pm – Final project presentations

Format

You may work by yourself, or in groups of up to three students. Groups of five are right out.

You have quite a bit of latitude in what sort of project you choose to complete (subject to approval, of course). Possible types of projects include (but are not limited to):

• Developing some sort of Haskell application or library
• Encoding some proofs using Agda
• An expository presentation; e.g. pick a functional pearl (I’m happy to suggest some good ones), or a functional data structure, etc., understand and possibly re-implement it, and present it to the class.

Your project should somehow go beyond what we have covered in class, that is, completing the project should require you to learn something new.

Project proposal

You must submit a project proposal by Monday, April 18th explaining what you intend to do. The proposal should be about 1 page, and must clearly explain:

• What you intend to do
• Your specific goals for the project, i.e. what are the criteria for a successful project?
• An explanation of what you expect to learn, i.e. how does your project go beyond what we have covered in class?

I will provide feedback on your proposal to ensure that your project is at an appropriate level of difficulty.

Checkpoint meetings

During the week of April 25–29, your group must schedule a meeting with me to discuss your progress, ask questions, etc. (of course I am happy to meet with you at other times as well.)

Presentations

During the afternoon on Friday, May 6, you will give a 15–20 minute presentation on your project. The presentation could take many forms depending on the type of project. For example, it could just be a demo, if you primarily produced some sort of artifact; it could be a presentation with slides or a chalkboard talk explaining something.

Since giving a good presentation is not really a learning goal of this course, there is no particular specification or set of criteria that a presentation must meet. However, here are some suggestions for giving a good presentation:

• Give a practice run-through to a friend or two. This will help you be more familiar with what you plan to say.
• Don’t just scroll through your code (it tends to be very boring for the audience). If there are particular parts of your code that you want to highlight, copy them onto slides.
• You don’t have to make slides, but they can be helpful. If you do make slides, make sure each slide has just a few words or phrases.
• Include a live demo of your project if at all possible (and if this makes sense for your project).

Final submission

You may submit your project in one of two ways:

• By submitting a .tar, .tgz or .zip file

• By submitting a link to a publically accessible source repository, e.g. on github or bitbucket. Be sure to submit a link to one or more specific commits, tags, etc. representing what you would like to be graded, rather than just to the repository in general.

Specification

To get credit for your project, you must meet the following criteria:

• Turn in a project proposal meeting the criteria explained above.
• Have your proposal (or some variant thereof) approved by me.
• Accomplish what you set out to do in your proposal, or something of comparable scope.
• It is normal for projects to diverge somewhat from the proposal. If you are concerned whether you will meet this criterion, please talk to me about it. (Somewhat paradoxically, being concerned about this is probably a sign that you need not be!)
• Schedule and attend a checkpoint meeting.
• Give a project presentation on Friday, May 6.
• Your project must use good Haskell or Agda style and be well-documented (including both in-code comments and, as appropriate, external documents explaining e.g. how to run and use the project).
• Your project must be free of compilation errors and should correctly accomplish whatever it is supposed to accomplish.
• An exception to this criterion is that if there are known, minor bugs that you cannot or do not have time to fix, you may simply document them as such.
• You must demonstrate evidence that you put energy and effort into your project and that you have learned something. In your presentation, or in a document accompanying your project, you should be sure to highlight work you did and things you learned, especially if it is not obvious from looking at the final product. For example, if you spent a bunch of time trying an approach that ultimately did not work, you should talk about that and what you learned from the experience.

I will provide feedback on final projects that do not meet the specifications, allowing you an opportunity to address the issues and turn in a revised project.

Expectations

Although you and I play different roles in the course, we both have your learning as a common goal. There are things I expect from you as a student in the course, but there are also things you can expect of me as the course instructor and facilitator.

If I am not fulfilling my responsibilities outlined below, you are welcome (and encouraged!) to call me out, perhaps via the anonymous feedback form. I will also initiate a conversation if you are not fulfilling yours. However, none of us will meet all of the expectations perfectly—me included!—so it’s also important that we have grace and patience with one another.

What I expect from you What you can expect from me
Communication
• Check your email and Teams for occasional course announcements.
• Let me know via email or Teams message if you will need to miss class for some reason.
• Let me know as soon as possible if you feel you are struggling, would like extra help, or have something going on that will affect your engagement in the course or your ability to fulfill your responsibilities.
• Clearly communicate expectations, assignment details and dates, and grading standards.
• Return grades and feedback on submitted work within two weekdays of submission.
• Respond to emails within 24 hours.
Preparation
• Come prepared to fully engage in class meetings, with distractions minimized, to the best of your ability.
• Spend time outside of class actively practicing unfamiliar or shaky concepts or skills (not just reading over notes).
• Have a concrete plan for how we will spend each class meeting, prepared to lead you through the plan.
Engagement
• Make myself available to meet outside of class, and give you my full attention during a meeting.
• Be committed to your learning, open to feedback and willing to respond in substantive ways to your suggestions or concerns.

Attendance

Attendance in this class is not required as part of your grade. However, I do expect you to attend and appreciate knowing in advance if you will need to miss class.

Disabilities

If you have a documented disability or some other reason that you cannot meet the above expectations, and/or your learning would be best served by a modification to the usual course policies, I would be happy to work with you—please get in touch (via Teams or email)! The course policies are just a means to an end; I don’t care about the policies per se but I do care about you and your learning.

It is the policy of Hendrix College to accommodate students with disabilities, pursuant to federal and state law. Students should contact Julie Brown in the Office of Academic Success (505.2954; brownj@hendrix.edu) to begin the accommodation process. Any student seeking accommodation in relation to a recognized disability should inform the instructor at the beginning of the course.

Diversity and Inclusion

Hendrix College values a diverse learning environment as outlined in the College’s Statement on Diversity. All members of this community are expected to contribute to a respectful, welcoming, and inclusive environment for every other member of the community. If you believe you have been the subject of discrimination please contact Dean Mike Leblanc at leblanc@hendrix.edu or 501-450-1222 or the Title IX Coordinator Allison Vetter at titleix@hendrix.eduor 501-505-2901. If you have ideas for improving the inclusivity of the classroom experience please feel free to contact me. For more information on Hendrix non-discrimination policies, visit hendrix.edu/nondiscrimination.