Functional programming

Stream: Lean for teaching

[Martin Dvořák]

Do you think that LEAN is suitable for a course on functional programming? The default option is Haskell.

Most of the students will have previous experience with imperative programming, but I want the course to be accessible for everyone who can read and write. Hence, I'd also like to know whether "LEAN as one's first programming language" is too crazy.

[Arthur Paulino]

@Alexandre Rademaker told me he's been thinking about it. From what I understood, he's truly considering teaching a course of functional programming using Lean. IIRC, he meant Lean 4.

IMO, if you want to stick to the fundamentals of functional programming, Lean 4 works nicely. Haskell, on the other hand, has a huge package library and might be readier for those who want to program all sorts of systems at the moment

[Jannis Limperg]

Lean has few advantages over Haskell here: less stable, less polished, less docs, less teaching resources, less libraries (important for cool projects), smaller community, less relevant in both academia and industry. Of course it's doable, but you'd be doing your students a disservice.

[Martin Dvořák]

Jannis Limperg said:

Lean has few advantages over Haskell here: less stable, less polished, less docs, less teaching resources, (...)

You are talking about advantages of Haskell, right?

[Jannis Limperg]

Sorry, confusing wording. I mean "Lean is less stable, less polished, ... than Haskell."

[Moritz Doll]

What would be the reason not to use Haskell?

[Chris B]

Playing devil's advocate, there is an extent to which you want educators to be forward thinking, and I think there's value in exposing students to different ideas as long as the overall quality of instruction doesn't suffer. Universities started teaching classes like operating systems in Rust back in 2013/2014 which seems pretty prescient in hindsight (there's some info and student surveys for one class at the university of Virginia here: https://rust-class.org/0/pages/using-rust-for-an-undergraduate-os-course.html).

The overriding question is obviously whether your initial investigation leads you to believe that you can teach a course using Lean that is as good as or better than one using Haskell. If you have the ability to survey student interest in using something new/different that seems like it would be a good initial step.

[Arthur Paulino]

In my undergrad CS course, a teacher used some esoteric language to teach us the fundamentals of OOP. I can't even recall the name of the language! And in parallel, he taught us how to do the same things in C++ and Java. It caused a good impact on me because I was able to grasp the idea of OOP without confusing it with Java/C++ concepts, which I see happening quite often.

[Arthur Paulino]

As a result, I was then able to pick up OOP in Python and Scala pretty quickly

[Eric Taucher]

Here is a monkey wrench to gum up ones thinking. I first learned function programming on my own with F#, then OCaml, then ML, and then Lambda Calculus (untyped and typed). I learned Lambda Calculus with "An introduction to functional programming through Lambda calculus" by Greg Michaelson WorldCat. I am now working through "Types and Programming Languages"
by Benjamin C. Pierce (WorldCat). When I started with Lambda Calculus so many of the errors I encountered with the other languages all started to make sense.

[Eric Taucher]

Two other points to consider. 1. which has been noted is what I call the ethos of a language. Does the language have an active community, how hard is it to install and use the language. Does it have support on multiple OS. Is the community easy to reach and are helpful. etc. etc. 2. The boilerplate and syntax of the language. Languages that added functional after many years tend to have boilerplate code that is hard to grasp. F# on the other hand has |> which made learning composition so nice.

[Kevin Kappelmann]

I've been co-organising a functional programming course for 1000+ students/semester for 2 years. My take: students - in particular if they already have an imperative programming background - find FP concepts challenging and question the applicability of FP beyond academia. You will not do your students a favour if you introduce them to an even more powerful but less widespread language. You will also not do yourself a favour due to a lack of libraries and infrastructure; in particular, if you want to have automated tests for submissions, which I think is a must-have.

If you are interested, here is our (work-in-progress) paper about and resources from our course https://github.com/kappelmann/engaging-large-scale-functional-programming

[Arthur Paulino]

Another strong functional programming language: Clojure. It's even used in the industry, if that helps with motivation

[Arthur Paulino]

My CS department had a strong culture of detachment from languages though. I think that changes the game a bit.

[Martin Dvořák]

Thank you for all your replies!

[Alexandre Rademaker]

Indeed, as @Arthur Paulino said, I am planning a course on functional programming using Lean4 for next year. I have already discuss some ideas with @Leonardo de Moura too. In my previous courses I have used Haskell and the books https://www.amazon.com/Algorithm-Design-Haskell-Richard-Bird/dp/1108491618 and https://www.amazon.com/gp/product/B00O0RKGTO both from Richard Bird. The hard part to adapt is the codes where lazy evaluation is used. On the other hand, many of the equational reasoning presented in the books can be formally proved in Lean.. Ideas are welcome.

In another thread, with my hat of computational linguistics, this is another book that I want to translate to Lean from Haskell: https://staff.fnwi.uva.nl/d.j.n.vaneijck2/cs/

[Alexandre Rademaker]

I guess we can't talk about "a course on functional programming" without context. If you are in a CS department ori if your course will have +100 students, it may have some very different goals. I teach in an Applied Mathematics department and my course will be optional for 10-20 students at most.