Strange Loop

Idris: Practical Dependent Types with Practical Examples

Dependent types turn types into a first-class language construct and allows types to be predicated upon values. Allowing types to be controlled by ordinary values allows us to prove many more properties about our programs and enables some interesting forms of metaprogramming. We can do interesting things like write a type-safe printf or verify algebraic laws of data structures - but while dependent types are quickly gaining in popularity, it can be tricky to find examples which are both useful and introductory.

This talk will demonstrate some practical dependent typing examples (and not sized vectors) using Idris, a language designed for writing executable programs, rather than just proving theorems.

Brian McKenna

Brian McKenna is a small contributor to the Idris and PureScript languages. He also makes video tutorials on writing programs in Idris so that others can get started with dependent types. Brian works professionally as a functional programmer at a startup, using tools such as Scala and Haskell to create products for utility companies.