BFPG Meetup - August 2025 - Explicit Substitutions pt2 + Nix Flakes

​Agenda

• ​18:00: Welcome and setup

• ​Presentation #1: Explicit Substitutions Part 2 - Donovan Crichton

• ​Presentation #2: Overview of flake-parts and haskell-flake - Jack Kelly

• ​20:00ish: Pack down, head to Criterion pub.

​Explicit Substitutions Part 2

​During Part 1 (April) we covered the syntax for expression grammars, typing rules, and the simply typed lambda calculus, finishing off with an extended syntax for explicit substitutions.

​This talk will extend Part 1 by showing how to read (the syntax) and understand the intended behavior (semantics) of the new substitution combinators in our extended lambda calculus. We will then extend this approach to dependent types and show how to we may read presentations found in modern papers on dependent type systems.

​Overview of flake-parts and haskell-flake

​Nix Flakes are the modern Nix method for describing the outputs (build artifacts, development shells, etc.) of a project. flake-parts is a framework for DRYing up the common code in many flakes, and modularising it into separate slices of functionality (e.g., pre-commit hooks, Haskell project, services to run). haskell-flake is my default way of setting up a flake for "normal" Haskell projects. I'll give an overview of how the pieces fit together, and how to set up a real project with this framework.