Presentation: A Zero Cost Type System

[exterm]

Why static types

• people write code that contains bugs
• the earlier these bugs are found, the cheaper they are
  • dynamic language:
  • local tests
  • tophatting
  • CI
  • production
  • costs increase because
  • loss of context
  • cost of infrastructure
  • time spent going back and forth
  • production / consumer impact

Type systems can be very different

Java

Map<Integer, Integer> memoized = new HashMap<Integer, Integer>();

• practically no type inference
• verbose, as type annotations are mandatory
• nullable types (-> NullPointerException 🙄 )
• lots of work for OK effect

Ruby

memoized = {}

• succinct
• neither expressive nor safe

Haskell

memoized = empty
-- or
memoized = empty :: Map Integer Integer

• Hindley-Milner
• complex inferred types
• tries to prove program correct / find all run time type errors
• theoretically great
• type annotations sometimes necessary
• may reject valid programs

Erlang

Memoized = dict:new()
% or
-spec memoized() -> dict:dict(integer(), integer()).
memoized() -> dict:new().

• success typing
• type annotations fully optional
• tries to find bugs without ever rejecting valid code
• misses some run time type errors
• virtually a zero-cost type system

[exterm]

This talk heavily inspired by https://learnyousomeerlang.com/dialyzer

[exterm]

Hindley-Milner type inference

and(true, true) -> true;
and(false,   _) -> false;
and(_,   false) -> false.

% inferred type

(bool(),bool()) -> bool()

Wrong!

TODO why is this wrong? And why is the Hindley-Milner example in Erlang? Did I insert the wrong example?

[exterm]

placeholder

[exterm]

placeholder

[exterm]

Subtyping for Erlang

Erlang types overlap, so Hindley-Milner is not applicable.

Haskell guys (Phil Wadler and Simon Marlow) developed a subtyping system for erlang, but...

and(true,true) -> true;
and(false,X)   -> false;
and(X,false)   -> false.

% inferred type:
(1, false) -> false | true

in order to ensure that the function can never fail it is necessary to restrict the second argument to being false only.

They tried to keep their type system simple at the cost of accuracy, but still try to ensure that the program can never fail.

Also,

very little existing code needed to be changed to get through the typechecker

Code needs to be changed to satisfy the type checker, even if it is correct.

[exterm]

Dialyzer

Success types for Erlang.

Our method is simple because we address the type inference problem directly using constraint-based type inference techniques and without imposing any restrictions on function uses which are error-free in the operational semantics of the language.

Our method is also [...] able to automatically infer accurate types [...] without requiring any type information or guidance by the user.

Starts with the assumption that the program is correct, i.e. all functions accept all types - or: all values are of the top type.

It then goes through the code to find type constraints, reducing the set of acceptable values.

↪️ $ make example-1

If it is unsure, Dialyzer will accept the program. Take a look at the inferred types if you're curious.

↪️ $ dialyzer example-2.erl ↪️ $ typer example-2.erl

[exterm]

And?

So back to the and function example from earlier. What types are inferred via subtyping?

↪️ $ typer and_fun.erl

[exterm]

Let's find a few bugs

↪️ $ dialyzer discrepancy_1.erl

Dialyzer infers types through multiple levels of the call stack with ease: ↪️ $ dialyzer discrepancy_2.erl

If the behavior is complex enough though, it gives up. In this case, it doesn't understand what's going on, so it's optimistic and will assume the code works. ↪️ $ dialyzer discrepancy_3.erl

[exterm]

Type definitions and function specs

Only using type inference is boring. Let's construct a complex type ourselves and use it!

↪️ $ dialyzer cards.erl

There is a bug in there, but we need to help dialyzer find it.

[exterm]

More broken contracts

↪️ $ dialyzer type_definitions.erl

What does dialyzer think is wrong here?

[exterm]

Fancy types

Singleton types are interesting because they blur the distinction between types and values. They let us find very advanced bugs:

↪️ $ typer fancy_types.erl ↪️ $ dialyzer fancy_types.erl

They can even be used to detect race conditions! Erlang has a builtin global key-value store. If we know the type of a key to be written to to be a singleton type, we know the exact key that is written to. So, dialyzer can throw an error if two processes write to the same key. Sometimes.

[exterm]

There are other kinds of errors that can be found because success typing is a form of subtyping. Because we're starting with the top type any(), the set of all values, and every time we apply a type constraint we reduce the set, resulting in a subset.

↪️ $ ghc implicit_enum.hs

↪️ $ dialyzer implicit_enum.erl

[exterm]

Bonus

Polymorphic types (AKA generics)

↪️ $ dialyzer zoo.erl

↪️ $ dialyzer safe_zoo.erl

[exterm]

Links

Paper on success types, introducing dialyzer and typer Erlang type spec docs Paper looking back at getting dialyzer widely adopted

Also, a great resource on erlang in general https://learnyousomeerlang.com

[exterm]

Appendix

Why is ruby not expressive?

Ruby will run programs without complaining that are semantically wrong. Every language does that. But in some languages, types can be used to be more specific about the intended behavior. This way, errors can be caught by the type checker.

[exterm]

use something like https://yhatt.github.io/marp/ to build slides? Or https://gitpitch.com .

[exterm]

To Do:

• [ ] add haskell example for and function
• [ ] add sorbet examples