Collection of slides, notes, and posters for public talks I've given.
Functional programming conference in Boulder, CO.
Let’s scratch the surface of the power of Richard Eisenberg’s singletons library and peek through the doors of opportunity that it opens for us. Learn things you can directly apply now, and also build a foundation for future learning.
Look past the hype and see how the singletons library can benefit your programs today through type safety and dependently typed programming!
A Case Study With Neural Networks
Dependently-typed Haskell is all about pushing the limits of how much power your types have to verify that your code is correct, direct you in writing code, enhance your productivity, and encode meaning in type signatures. In this session, we will explore its practical benefits by applying these principles to building verified neural networks. We look at neural networks with and without dependent types, show how to add dependently typed benefits incrementally, and clearly show the benefits that we can directly apply to many different applications. This session is geared less toward the theoretical idea of dependent types and more toward hitting the ground running with immediate benefits in existing code bases.
Developers will learn the basic concepts of dependent types, existential types, type-level proofs, and working with the “singletons” library, as well as high-level concepts in dependently typed development.
Super-charge the correctness of your code incrementally and find new ways to make the compiler work for you today!