Haskell

Haskell is an advanced, purely functional programming language with Hindley-Milner type system, concurrent runtime and lazy (non-strict) evaluation.

Things to keep in mind:

  • Static type system doesn't necessarily mean wrestling with types like in C thanks to the advanced type inference in Haskell: in fact on many occassions you can let the compiler write your logic for you based on the type signatures
  • Lazy evaluation is much more aligned with mathematical reasoning and abstractions: it allows for e.g. manipulations on infinite lists
  • One of the defining features of purely functional languages, referential transparency, lets us reason about our programs in a much more structured way
  • What's more, Haskell programs are, to an extent, provable: you can prove things like termination or even correctness of algorithm implementation, see Curry-Howard correspondence
  • That said, Haskell flexibility prevents it from having some of the critical capabilities required to be a fully operational proof assistant like Coq: it's a trade-off
  • Haskell carries deep ideas applicable to modern imperative dynamically typed languages (such as Python): it just might make you a better programmer (but you don't have to program to learn Haskell!)

Format I have in mind is to focus on LYAH (one chapter per week) and supplement with exercises and relevant chapters from HFFP. During weekly meetings we would then discuss our reflections on the chapter, things we found hard or interesting, go through the solutions for exercises and review relevant blogposts to a level of detail dependent on time constraints.

It would be also great to try and connect what we learn here to our university curriculum, especially MA211 and MA203.

Below you'll find a long list of links, loosely partitioned into vague categories. Have a look and skim a couple pages to get an overall feeling for Haskell. Bold font means it's quality content.

Motivation

Formal verification and type theory

Fundamental resources

Advanced resources

Environment

Miscellaneous

Research

20/06/2020