Brian McKenna - Practical Dependent Types with Practical Examples

[tamascsaba]

speaker: Brian McKenna
topic: Practical Dependent Types with Practical Examples
video: https://www.youtube.com/watch?v=4i7KrG1Afbk
length: 40:55

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.

by Brian McKenna (@puf nfresh)

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.

[bkil-syslogng]

The language sounds interesting, with its C, Javascript and Java backends and functional roots, but I'd like to see how real applications would be developed with it, how it would look like a mixed environment, what kind if IDE support will be feasible in the near future, its performance, comparison to other bleeding edge and establish languages (Rust, Elixir, ....).

[tamascsaba]

I'm glad you have seen the video. I'm really looking forward to see how it works in production environment. :)