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.