CSCI 490: Functional Programming (S’16)

Final project

Overview/important dates

You will complete a final project which will extend or tie together some of the things we have learned over the course of the semester.

Important dates:

• Tuesday, April 19 – Project proposals due
• April 25–29 – Checkpoint meetings
• Thursday, May 5, 2-5pm – 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 Idris
• 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 explaining what you intend to do. The proposal should be about 1 page, and should 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?

Checkpoint meetings

During the week of April 25–29, your group must schedule a 30-minute 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

In the afternoon on Thursday, May 5, 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.

Final submission

You may submit your project in one of two ways:

• By emailing me a .tar, .tgz or .zip file

• By emailing me a link to a publically accessible source repository, e.g. on github, bitbucket, or hub.darcs.net. 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.

Grading

Grading will be as follows:

• Proposal (10%).

• Style (10%). Your project should use good Haskell or Idris style and be well-documented.

• Checkpoint (10%). Did you make some progress on your project by the time of the checkpoint meeting?

• Presentation (20%). Your presentation should be clear and instructive, demonstrating your project and what you learned.

• Correctness (25%). Your project should be free of compilation errors and should correctly accomplish whatever it is supposed to accomplish. For an expository project, your explanations should be clear and correct.

• Effort/accomplishment (25%). I will be looking for evidence that you put energy and effort into your project and that you have learned something. In your presentation, 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.

Docs

• Syllabus
• Haskell style guide
• lhs2TeX and SProof
  • lhs2TeX and SProof tutorial
  • tutorial source
  • sproof.sty
• Presentation rubric

Lectures

• Th 21 Jan — Introduction to Haskell

• T 26 Jan — Algebraic data types & pattern matching
  In-class code

• Th 28 Jan — Propositional logic

• T 2 Feb — Polymorphism, recursion patterns

• Th 4 Feb — Folds
  In-class code

• T 9 Feb — Currying, induction
  In-class code

• Th 11 Feb — Induction
  In-class code
  In-class LaTeX

• T 16 Feb — Untyped λ-calculus I

• Th 18 Feb — Untyped λ-calculus II

• T 23 Feb — Y combinator, STLC I

• Th 25 Feb — STLC II, Curry-Howard Isomorphism, Lambda cube

• T 1 Mar — Intro to Idris
  In-class code

• T 8 Mar — Idris II (Inductive proofs, dependent functions and pairs)
  In-class code

• Th 10 Mar — Idris III (Equality, structured proofs)
  In-class code

• T 15 Mar — Idris IV (Induction)
  In-class code

• Th 17 Mar — Idris V (Encoding STLC)
  In-class code

• T 29 Mar — Type classes
  In-class code

• Th 31 Mar — Kinds and Functors
  In-class code

• T 5 Apr — Applicative
  Expr solution with Functor, In-class code

• Th 7 Apr — Guest lecture (Kenny Foner)
  Lecture notes on GitHub

• T 12 Apr — Applicative

• Th 14 Apr — Applicative
  In-class code

• T 19 Apr — Monad

• Th 21 Apr — Monad
  In-class code

• T 26 Apr — Free monads and embedded domain-specific languages
  In-class code

Assignments

Weekly assignments will be posted here and on Moodle, and are due every Tuesday before the beginning of class.

hshw.sty

• Week 1: Intro to Haskell [ lhs ]. Due Tuesday, 26 January.
• Week 2: Algebraic Data Types and Proof Trees [ lhs, Proof.hs ]. Due Tuesday, 2 February.
• Week 3: Polymorphism and Recursion Patterns [ lhs ]. Due Tuesday, 9 February.
• Week 4: Induction [ lhs ]. Due Tuesday, 16 February.

• Week 5: Lambda calculus [ lhs ]. Due Tuesday, 23 February.

  Here is an installation script for the command-line lambda-calculus interpreter. It should work on OS X or Linux. (I don’t know how to make an installer for Windows, but you should be able to simply look in the installation script and manually execute the commands it contains.) Make a new, empty directory and copy the installation script into it, then run the script (e.g. by doing chmod +x lc-install and then ./lc-install). It should create a directory .cabal-sandbox/bin containing an executable named lc; you can copy the lc executable anywhere you like.

• Week 6: STLC [ lhs, STLC.hs ]. Due Tuesday, 1 March.

• Week 7: Idris Basics. Due Tuesday, 8 March.

• Week 8: Proofs and Curry-Howard in Idris. Due Tuesday, 15 March.

• Week 10: Type classes [ lhs, ExprT.hs, StackVM.hs, Parser.hs ]

• Week 11: Applicative functors [ lhs, AParser.hs, SExpr.hs ]

Resources

Installation and coding environment

• Follow the instructions here to install Haskell on your computer.

• If you have a favorite text editor it will probably work just fine for editing Haskell programs. There is a nice haskell-mode for emacs. Vim comes with syntax highlighting for Haskell out of the box; for more options try this vim haskell mode. Other editors commonly used with Haskell include Nodepad++, TextMate, Gedit, Sublime Text, or Atom.

LaTeX

• The LaTeX wikibook is a great resource.

• ShareLaTeX is a great site for collaborative editing of LaTeX documents. Unfortunately it won’t work super well for this class since you also need to be able to run your LaTeX documents as Haskell programs, and preprocess them using lhs2TeX. However, the ShareLaTeX documentation may still be useful.

• To install LaTeX on your own computer, use one of these:
  • MikTeX (Windows)
  • TeXShop (Mac)
  • TeX Live (Linux — there is probably a texlive package in your package manager, so no need to download it directly from this website)

Help/community

• The #haskell IRC channel is a great place to get help. Strange as it may seem if you’ve spent time in other IRC channels, #haskell tends to be full of friendly, helpful people.

• tryhaskell.org gives you a ghci session in your browser, and includes a very simple tutorial. It also features an interface to the #haskell IRC channel.

• lpaste.net is a good place to paste programs you’re having trouble with in order to get help from people in #haskell.

• 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 Haskell wiki has a list of frequently asked questions.

Reading

• Haskell Programming from first principles is a book in progress which has been getting good reviews. An early access, electronic version is currently available for purchase.

• 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.

• Learn You a Haskell for Great Good! is a whimsical Haskell tutorial with funny illustrations. Might be good as an extra reference though I disagree with many of the pedagogical choices it makes. Available for free online or in dead tree form.

• The Haskell wiki is a huge grab-bag of all sorts of information, examples, explanations. The quality varies but it’s definitely a great resource.

• Planet Haskell aggregates blog posts from the Haskell community.

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

Reference

• Haskell standard library documentation.

• A useful Haskell cheatsheet.

• Hackage is a huge repository of Haskell packages. If it isn’t on Hackage, it doesn’t exist. Packages can be automatically downloaded and installed from Hackage using the cabal-install tool.

• 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.

• Hayoo is another search engine for the Haskell documentation, which is much more complete (it searches all of Hackage).

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