Inspired by Niels Serups inspirational talk about unspectacular personal failures, here is one about my first excursion into the relm of dependently typed programming.
When learning about dependent types, one is often presented with cannonical examples such as a list that is parameterized with its lenght. However, dependent types turn out to be quite useful for inferring properties about terms. An exapmle of such a property is coarsest grid needed to notate a rhythmic pattern in a drum machine, and in this talk I will explain what that means, and go over an Agda-embeded implementation of a programming language that inferres that.
With some probability, the talk will inspire some of you to start hacking on a project of your own, using Dependent Types in new and cool ways.