Functional Programming and Verification

Chair for Logic and Verification

Installing Haskell 🛠️

The following guide provides you installation instructions for a complete Haskell programming environment, including a compiler, build tools, linter, and editor. It is important that you use this environment for the online tutorials. If you face any problems, you can ask for help at this BBB room on Friday, 06.11.2020 at 14.00–15.00 and 17.00–18.00.

  1. Install stack. Stack is a build tool for Haskell.
  2. Open a terminal and install the Haskell developer linter plugin:
stack install hlint
  1. Install VSCodium. VSCodium is an extensible, open-source code editor. Alternatively, you can install the non-free VSCode editor. Note that Microsoft puts some telemetry/tracking on top of VSCodium. We hence strongly suggest you to use VSCodium.
  2. Ensure that the codium command – or code if you installed VSCode – is available in your PATH by opening a new terminal and running codium. This might already work out of the box. If not, open VSCodium and follow the instructions here or add VSCodium to your PATH manually.
  3. (Skip if you installed VSCode) Change the extensionsGallery section of the resources/app/product.json file as described here.
  4. Install the supplementary Haskell extensions for VSCodium by running the following in your terminal (again, replace codium by code if needed):
codium --install-extension ms-vsliveshare.vsliveshare --install-extension haskell.haskell --install-extension justusadam.language-haskell --install-extension hoovercj.haskell-linter --install-extension jcanero.hoogle-vscode

Checking Your Programming Setup 🤔

  1. Download and unzip the test project.
  2. Open VSCodium (e.g. by running codium in your terminal).
  3. Open the downloaded test project: File -> Open Folder -> Select the test project. A window might appear on the bottom right of VSCodium, telling you that the required Haskell files are being downloaded. If so, wait for this download to be finished.
  4. Open the file src/HaskellTest.hs in the VSCodium-explorer on the left of the editor. This is how a typical Haskell file looks like.
  5. Open the file haskell-test.cabal. This file specifies how the project should be build, including its dependencies, and which file is to be executed.
  6. Open the file stack.yaml. This file specifies which curated set of packages should be used when resolving the project’s dependencies. This will make sure that all dependencies play well-together and no version conflicts arise.
  7. Let us now compile the project: Open the integrated terminal of VSCodium. One easy way to do this is by using VSCodium’s nice “Command Palette”. Press CTRL+SHIFT+P (⌘+SHIFT+P on MacOS) to open the palette, type view integrated terminal, and then press the Return key.
  8. You will see a terminal at the bottom of your editor. The terminal should already be located in the project folder. Run stack ghci in the terminal. This will build the executable/library as specified in haskell-test.cabal (if needed) and start a REPL environment called GHCi. All functions in your source file are available in this environment. For example, you can enter fib 0 to print the first fibonacci number. Congrats, you just built and executed your first Haskell programm 🎉 If you change the source code, save it and then type :r in the console to reload the code. You can press :q to quit GHCi. See below or here for more tips and tricks. Indeed, your setup at hand can do much more than just compiling Haskell programms. It can also assist you writing them and help avoiding mistakes:
  9. Open src/HaskellTest.hs again and remove the type signature main :: IO(). You will see a lightbulb appear above the function body, suggesting you the just removed type signature. You can click on the suggestion to apply it to your code. One can automatically infer (in most cases) the most general type of a given function in Haskell. Check out what happens if you remove the signature of fib!
  10. Not only will you get assistance for type signatures, but the setup will also detect some code-smells. Replace the call print fibs by print (fibs !! 0) to only print the first element of the list fibs. Again, a lightbulb will appear, suggesting you replace fibs !! 0 by head fibs. The latter is the standard way in Haskell to obtain the first element of a list – writing fibs !! 0 indeed looks suspicious and arcane to Haskell programmers!
  11. Often, you are looking for a function whose type is known to you, but you do not know how it is called or whether it exists at all. As an example, imagine you are looking for a function that removes the first element of a list of integers and returns the remaining elements. In Haskell, the type of such a function is [Integer] -> [Integer] as it takes a list of integers and returns a list of integers (the remaining elements). When facing such a situation, you can again fire up the command palette (CTRL+SHIFT+P) and type hoogle. Hoogle is the Google for Haskell. A small window will appear where you can enter your interface in question, that is [Integer] -> [Integer]. Press Return and shortly after, you will see a list of suggestions appear. The first suggestion – tail :: [a] -> [a] – sounds quite promising and indeed does the right job as you can verify by clicking on the entry and reading its documentation. Note how the type of tail is more general than the one we were looking for; however, Hoogle, clever as it is, still found the right result.

Connecting With Peers 👐💬

In our tutorials, we will make extensive use of pair programming for pedagogical as well as sociological benefits. For this, we use the VS Live Share plugin you already installed. You will need a GitHub or Microsoft account to connect to your peers. We recommend you the former – most likely, you already have a GitHub account anyway. Please make sure this plugin works before attending the first tutorial:

  1. If you haven’t logged into Live Share before, do so now:
    1. Log in here.
    2. Click Having trouble? Click here for user code directions.
    3. Copy the user code.
    4. Open the command palette in VSCodium and open Live Share: Sign in with user code.
    5. Paste the user code from your clipboard.
  2. On the left sidebar of VSCodium, you will find a the Live Share button (curved arrow to the right above a circle). Click it.
  3. Press “Share Read/Write”.
  4. The live sharing session will start and automatically copy a URL to your clipboard.
  5. Open a second VSCodium instance (CTRL+SHIFT+N), click the Live Share button there, press “Join”, and enter the URL if needed (it should get pasted automatically from your clipboard).
  6. Place the VSCodium instances side-by-side and explore the features of the live sharing plugin. In the future, you will have fun using this with your friends and tutors, making the online semester a bit more social again ☺️

GHCi Commands 🔤

Command Explanation
:r or :reload reload source files; use after updating and saving your .hs files in your editor
:l <file> or :load <file> load Haskell source file and its dependents
:t <expr> or :type <expr> print the type of the expression <expr>.
:i <name> or :info <name> display information about the given name(s); works with function names, type names, etc.
:browse list all functions in scope including type signatures
<pattern> = <expr> introduce temporary value or function definition (these disappear after reloading any files)
:? or :help print complete list of GHCi commands
:q or :quit quit