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.