Sessions in this room

1. 10:05 in Tutorials #2

   Learn FP with Code Katas

   Functional programming helps you reason about and test your code by breaking it into self contained pieces in pure functions. In this workshop you will be given a code kata and a set of constraints which train pair programming and functional thinking such as ping pong, navigator-driver, verbs instead of nouns. Each pair will pick up a language which supports functional programming and a constraint based on their self evaluated experience level. The idea is to use constraints to trigger creative problem solving.

   Please bring your laptop which should be ready for development, with everything you need installed i.e. IDE and unit testing framework for languages such as Scala, Haskell, Clojure. Make sure it is set up properly by having a new project with a failing test. The workshop assumes basic programming skills and participants should be already able to solve problems using them. You can consider this a mini version of a coderetreat.

2. 14:15 in Tutorials #2

   Type-Level Programming in Haskell

   How types help us solve real-world problems

   The Haskell type system is good for specifying user intentions and helping the compiler to check code correctness. Unfortunately, there is sometimes a barrier before that level where beginning Haskell programmer can read and write complex type annotations. This is often the case with such libraries as Lens or Servant. With this tutorial, I aim to bring participants behind that barrier. I’ll present several type-level programming tools including type families, GADTs, data kinds, and others all way down to ‘almost’ dependent types. Their description will be given together with practical examples as used in the modern Haskell libraries.

3. 16:20 in Tutorials #2

   Writing Hardware in Haskell

   In this hands-on session, we will write Haskell programs, compile them into digital circuits, and flash them onto an FPGA (field programmable gate array).

   PGAs are computer chips containing logic and memory cells that can be dynamically reconfigured to implement various digital circuits. This allows to iteratively develop processors, highly parallel high-performance computations, networking stacks and more without having to manufacture a custom chip.

   While traditional hardware description languages (HDLs), exist to design these systems, circuit semantics are also nicely captured by purely functional programs. Clash in particular, can compile a subset of Haskell into traditional HDLs, providing powerful high-level abstractions and correctness guarantees. It also allows reusing large parts of the existing Haskell tooling and library ecosystem.

   We will start with an overview of digital circuits and FPGAs, explaining the flexibility and restrictions faced when designing hardware. After a quick demo of how to work with Clash, participants will write their own designs, test them in GHCi and compile them to hardware.

   The tutorial assumes basic proficiency with Haskell, including Functors and Applicatives. FPGAs and some additional hardware are provided, but a laptop is required to run Clash and an open source hardware design toolchain.

   Participants will

   • gain an understanding of the inner workings of digital circuits, which they are surrounded by in their daily lives
   • see examples of how to use types and common abstractions (Functor, …) to model properties of a domain
   • more generally experience the versatility and expressiveness of functional programming, inspiring them to solve problems in a multitude of domains outside of what they thought is possible.

4. 11:45 in Tutorials #2

   MirageOS: building minimized special-purpose unikernels

   Unikernels are specialized services, where the runtime binary (process, virtual machine) only contains the necessary libraries. This reduces the attack surface drastically (around two orders of magnitude). MirageOS is a unikernel project that uses OCaml, which also reduces the attack vectors (memory safety, type safety). MirageOS does not contain any process management, neither virtual memory – the entire unikernel is executed in single address space. The cooperative multitasking library lwt is used at the base.

   MirageOS can be deployed to various modern hypervisors: Xen, Linux KVM, FreeBSD BHyve, OpenBSD VMM, virtio, as well as to the Genode microkernel-based operating system framework and the separation kernel Muen. It can also be run as a unix process with rather restrictive seccomp filters (less than 10 syscalls needed). It runs on X86-64, ARM64 (Raspberry PI), ESP32; RISC-V support is along its way.

   Apart from core Internet Protocols (TCP/IP, DHCP, DNS, HTTP), security protocols (TLS, OpenPGP, OTR), and branchable distributed storage (implementing the git protocol) for persistency, several applications are work-in-progress:

   - Calendar and address book (CalDAV/CardDAV) storing data in a remote git repository
   - EMail (MIME encoding/decoding, SMTP, IMAP)
   - Firewall
   - VPN Gateway
   

   In this tutorial, first I’ll briefly introduce the benefits of MirageOS and the programming environment - the mirage command line utility takes care of target-specific dependency, initialization order, etc. by generating code. Afterwards, we’ll dig deep down further examples.