Correct and Efficient Code using Dependent Types and Gadts

Presenter: Michael Kerekes, creator of the Mana programming language

Dependently typed languages have two major novel features: (1) types are first class, and (2) types can depend on arbitrary values. First class types can be passed as parameters, returned from functions, and stored in data structures just like any other value. Types can be calculated from other types or normal values. These features allow almost any property of code to be checked statically at compile time, which in turn allows runtime checking of those properties to be removed.

I have recently added dependent types to the Mana language and I will give a few examples of their use:

• an efficient interpreter for an expression language. The strongly typed AST makes it possible to remove all runtime type checks.
• length indexed lists that require no runtime bounds checks
• a strongly typed implementation of printf that statically calculates it parameter types from the format string at compile time