Flying Spaghetti Monster (Type Systems and Microservices)

As we move away from monolithic architectures towards systems comprised of cooperating services, we introduce new opportunities and new failure modes. This is especially true of microservice architectures and even more so for function-as-service approaches like AWS Lambda. We achieve simplicity in each component, but at the cost of pushing complexity into the orchestration. And any sufficiently complicated microservice architecture contains an ad-hoc, informally-specified, bug-ridden distributed protocol.

Though we've traditionally used type systems to check correctness within a program, it turns out that expressive type systems can be used to check that a program correctly implements a protocol. The classic example is interacting with a vending machine - the compiler can check that your program doesn't try and take the chocolate bar before you've inserted the coins. This can be scaled up to systems of many cooperating actors and ensure that, for example, there is no chance of a distributed deadlock.

Expressive type systems are fascinating and worth exploring even if your daily employment doesn't require it. "Dependent typing", as the variety of type system implemented by Idris is called, is an emerging area of functional programming. We don't yet understand how to best apply dependent types to everyday programming, but we can see that they offer us solutions to some of today's hard problems. If you enjoy expanding your horizons, learning new tools for thought and participating in the conversation around new ideas, now is a great time to get into Idris. This talk doesn't assume any prior knowledge of Idris or dependent type theory.

Talk objectives:

• To help the audience understand that types can help us at the system level.

Target audience:

• The union of people interested in type systems and microservices.