BFPG Meetup - August 2023
Details
Agenda
- 18:00: Welcome and setup
- Presentation #1: Donovan Crichton - Towards Palatable Functional Programming with Dependent Type Theories
- Presentation #2: George Wilson - FP in Industry
- 20:00ish: Pack down, exit, head to Criterion pub.
Towards Palatable Functional Programming with Dependent Type Theories
This talk examines one of the idiosyncrasies of dependently typed programming, the requirement for totality. We will see why we have this requirement and how the current approach to satisfying this requirement is distinctly unpalatable for programmers.
Donovan will introduce the main thrust of his research, namely using a type-theoretic approach to ensuring totality and outline the steps needed to take this idea to a working implementation.
Along the way, we will (briefly) examine concepts such as dependent types, type theories, extensionality, intensionality, induction, co-induction, formalisation or mechanisation, and semantics.
FP in Industry
With its heavy use of Scala, REA is Australia's largest commercial user of Functional Programming (as far as George knows). Functional Programming is one of REA Group's Core Engineering Practices alongside TDD and CD. What does this look like in practice? How did this come to be? Where to from here?
In this talk, we will discuss how REA makes FP work across many teams of varying FP skill levels, including contributors from around the world. We'll learn some of the ten year history of FP at REA, including the challenges faced and lessons learnt along the way. We will discuss current state of FP adoption and usage at REA, which has expanded from Scala into TypeScript and beyond, Finally, we will discuss plans for the future of FP at REA.