This repo contains code and pdfs for the talks I give on an ad-hoc or one-off basis. In order from the most recent to least recent. I started collating my talks during the middle of my PhD in early 2023.
- [Enforcing a discipline of Total Functional Programming through Dependent Types](
- Why is so much of FP about Types instead of Functions?
- Towards Palatable Functional Programming With Dependent Type Theories
- Introduction to Idris and GADTs
The link to each talk is usually the first word of the description.
This was a short talk given to the Brisbane Functional Programming Group about how dependent types can be used to practice total functional programming without wrapping all our types in eithers/maybes.
This was a short and informal introductory talk given to the Brisbane Functional Programming Group which introduces the notion of a function and describes their limitations, and why types tend to take up a surprising amount of the discussion space in functional programming communities. I cover Sets, Relations, Functions, Algebraic Data Types, Type Classes, and Dependent Types.
This was a short and informal talk given to the Brisbane Functional Programming Group which served as a reintroduction of myself to the group after an approximate three year absence while I resided in Canberra. The talk gives a gentle introduction to the limitations of syntactic totality checking in Idris at the time of writing, and motivates my broad PhD topic: The need to investigate type-based approaches to totality and guarded recursion, and how this necessitates the proposal of a construction of a guarded, observational, linear, dependent type theory to allow us to experiment with improving dependently typed languages for programmers.
This was a short guest lecture given to the 2023 Semester 1 students of the Australian National University's COMP1130 course. I introduce Generalised Algebraic Data Type (GADT) syntax in Haskell, motivate them, and then describe why the move to a friendlier language (Idris) is necessary. I finish with some examples of dependent types and GADTs in Idris.