Dependent types are showing up in more and more mainstream languages, but they can still seem like magic. In this workshop, we'll walk through one of the primary techniques for implementing a type checker for dependent types, called normalization by evaluation. We'll be implementing a little dependently typed language called Pie developed by Dan Friedman and myself.

The implementation is written entirely in a very small subset of Scheme, and I'll assume no knowledge beyond that gained by reading The Little Schemer.

Workshop goals:

 * Introduce the ideas behind normalization by evaluation and
   bidirectional type checking

 * Write a type checker for a little dependently typed language

Prerequisites:

 * Basic familiarity with and interest in dependent types, equivalent
   to having worked through the Idris tutorial [1]

 * Know enough Racket or Scheme to write an interpreter for a small
   Lisp-like language

 * Have a recent version of Racket installed on your laptop

[1]: http://docs.idris-lang.org/en/latest/tutorial/

How do systems built in Erlang, Elixir or any other BEAM Language differ from other systems? To start with:+ They are designed from the bottom up to run 'forever.’

  • They are designed from the bottom up to expect, and recover from errors.
  • They are expected to evolve.
  • They scale seamlessly 

 

How is all of this achieved? - the answer is simple - by making systems from sets of isolated communication processes, and by treating errors and code as first class objects that can be sent in messages over a network.

 In this tutorial, Joe Armstrong will introduce what he calls the `Erlang way of thinking.`  He will cover:  

 

  • Basic data types
  • Sequential Programming
  • Concurrent Programming

 

In Basic Data Types & Sequential Erlang he’ll introduce the foundations and talk about Modules, Functions and Pattern Matching. Once you've understood the basic pattern matching mechanism the rest is easy.

In concurrent programming he'll talk about processes and their life span. You will look at sending and receiving messages, selective reception, and passing data in the messages. Joe will conclude this section by introducing the simple but powerful error handling mechanisms in processes which help detect and isolate failure.

Time permitting, he will cover distribution, showing you how, by doing it right form the start or with very few changes, you can write a program intended to run on a single VM and distribute it in a cluster.

Tutorial objectives: To learn the Erlang way of thinking when architecting and developing systems.

Target audience: Developers and Architects interested in the principles which make Erlang, Elixir or other BEAM based languages unique.

Note: We we recommend you take this tutorial in conjunction with the OTP one in the afternoon.

While Erlang is a powerful programming language used to build distributed, fault tolerant systems with requirements of high availability, these complex systems require middleware in the form of reusable libraries, release, debugging and maintenance tools together with design principles and patterns used to style your concurrency model and your architecture.

In this tutorial, Robert will introduce the building blocks that form OTP, the defacto middleware that ships with the Erlang and Elixir distributions. He will cover OTP’s design principles, describing how they provide software engineering guidelines that enable developers to structure systems in a scalable and fault tolerant way, without the need to reinvent the wheel.

Tutorial objectives: To learn the Erlang way of thinking when architecting and developing systems.

Target audience: Developers and Architects interested in the principles which make Erlang, Elixir or other Beam based languages unique.

Level: Beginners and Intermediate

Note: We recommend you take this tutorial in conjunction with the one on thinking concurrently.

In this workshop we will dive into generic programming in Scala using shapeless. We will start by discussing how to use shapeless to automatically create instances of type classes ("JSON encoder", "Equals", "Show", and so on) for any algebraic data type (case class or sealed trait). Once we have experience with the basic techniques, we will discuss the "lemma pattern", which allows us to bundle shapeless code into re-usable building blocks that we can combine at ever more powerful levels of abstraction. We will ground this theory by splitting into groups and developing several complete worked examples.

The workshop is aimed at established Scala developers who haven't yet got to grips with shapeless. It will use material from Dave's book "The Type Astronaut's Guide to Shapeless", which you can download for free from the Underscore web site, http://underscore.io/books/shapeless-guide. You will need: a laptop, a copy of Scala, and a clone of the exercises repo. http://github.com/underscoreio/shapeless-guide-code. Setup instructions are in the README on Github. Please grab the book and code before the workshop to avoid unexpected last minute technical problems.

Tutorial Objectives:

  • Learn how to eliminate Scala boilerplate using generic programming.
  • Demystify one of the most powerful libraries in the Scala ecosystem.
  • Amaze your friends with a new-found mastery of Scala's type system.

 

Live Coding systems encourage us to think extremely differently about programming languages and take ideas such as those found in reactive programming to the next level. For example, in addition to considering standard requirements such as reliability, efficiency and correctness we are also forced to deal with issues such as:

  • liveness,
  • concurrency,
  • coordination
  • determinism
  • time


What is it like to think fluently with such concepts? How might these ideas apply and benefit your development practices? The object of this highly interactive workshop is not to just cover these questions but give you your own initial experiences to draw from. Together, we'll learn how to work with all these imprtant concepts using Sonic Pi - whilst having a lot of productive fun.

Together we'll learn the basics of live coding through time using music as our guiding metaphor. However, we'll continually explore which domains other than music where live interaction and manipulation of running processes is both relevant and important.

Once we have mastered the basics of live coding with time, we will end the workshop by building a live distributed reactive event system that will enable us to collaboratively jam together.

This workshop is friendly and open to everyone. No programming knowledge is required, although the rabbit hole is so deep that seasoned programmers will still find many new things to learn and experience.

Note: this is the only workshop that will explore the principles of reactive programming whilst making sick beats.

Please come along with a laptop with Sonic Pi pre-installed (http://sonic-pi.net)


Workshop Schedule

09:00-12:30 Thinking Concurrently
Joe Armstrong
Implementing Dependent Types
David Christiansen
Type Class Derivation with Shapeless
Dave Gurnell
12:30-13:30   Lunch  
13:30-17:00 OTP, Middleware for
Concurrent Distributed Scalable Architectures

Robert Virding
Distributed Live Coding with Sonic Pi
Sam Aaron
 
 
*Once you have purchased your ticket, we will contact you regarding the workshops
you would like to attend.