Past Meetup

Type-directed search with dependent types

This Meetup is past

14 people went

Location image of event venue

Details

Types have the potential to be, all at once, specifications, documentation, and proofs of correctness. Because Haskell's got a powerful type system, Hoogle (http://www.haskell.org/hoogle/), a tool for finding terms by approximate type signature, proves rather valuable. But in a dependently typed language, types reach their pinnacle. The combined variety and precision of types in such languages means that type-directed search is a really enticing proposition.

So I decided to create such a type-directed search! I wrote the :search function for Idris (http://www.idris-lang.org), a dependently typed programming language inspired by Haskell. I took an approach guided by type isomorphism (which is somewhat different from Hoogle): when :search matches two types, one can be constructed from the other.

In this talk, I'll explain Idris's :search functionality. I'll talk about type-driven development, type isomorphism, and how :search works. I may include a brief introduction to Idris. Along the way, I hope to convince you that types are our salvation, dependent types are the future of programming, and that type-directed search is cool!

- Ben