Selective Functors in Lean 4

A formalization of selective applicative functors in Lean 4, based on the paper:

Selective Applicative Functors Andrey Mokhov, Georgy Lukyanov, Simon Marlow, Jeremie Dimino (2019)

I did this while reading the paper, as a way to better engage with the material. The overview and all the lean code was handwritten. The rest of the Readme and the comments in the Lean code where partially AI-generated.

Overview

Selective functors are an intermediate construction between applicative functors and monads. Monads give the most general construct: x >>= f where f is allowed to depend on the value of the result of the computation of x, forcing the effects of x to be emitted before the ones of f and preventing static analysis (one cannot dry-run the computation).

• Functor : transform values
  • <$> : (α → β) → m α → m β : (map) apply a pure function to a value inside m.
• Applicative Functor : combine independent effectful computations
  • <*> : m (α → β) → m α → m β : (seq) both the function and the argument may carry effects, but effects may not depend on the intermediate value (of type α). Derived operators:
    • *> : m α → m β → m β : (seqRight) sequentially runs the two arguments, discarding the result of the first one.
  • pure : α → m α : lifts a value inside m
• Selective applicative functors : conditionally execute effects
  • <*? : m (α ⊕ β) → m (α → β) → m β : (select) effects are determined statically, but whether they’re emitted or skipped depend on a dynamic value.
• Monad : sequence dependent computations
  • >>= : m α → (α → m β) → m β : (bind) uses the result of the first effectful computation to decide on the next computation.

Results depend on parametricity : in Haskell (or in System F), a polymorphic function really cannot depend on the value of its type parameter (which type), so it has a bunch of extra-properties just from the shape of its type.

Structure

Module	Description
Selective.Basic	The Selective typeclass with select : m (α ⊕ β) → m (α → β) → m β, plus monadic (selectM) and applicative (selectA) implementations.
Selective.Combinators	Derived operations: whenS, branch, ifS, <\vert\vert>, <&&>, fromOptionS, anyS, allS, bindBool.
Selective.Laws	The LawfulSelective typeclass: identity (P1), distributivity (P2), associativity (P3), and three parametricity laws (F1–F3).
Selective.Free	The free selective functor via CPS encoding, with LawfulSelective proved by delegation to the target functor.

Laws

A lawful Selective instance satisfies:

• (P1) Identity: x <*? pure y = Sum.elim y id <$> x
• (P2) Distributivity: pure x <*? (y *> z) = (pure x <*? y) *> (pure x <*? z)
• (P3) Associativity: x <*? (y <*? z) = p <*? q <*? r (with appropriate repackaging of the Sum types)
• (F1) Map-select: f <$> (x <*? y) = (Sum.map id f <$> x) <*? ((f . ·) <$> y)
• (F2) Select-app-left: (Sum.map f id <$> x) <*? y = x <*? ((· . f) <$> y)
• (F3) Select-app-right: x <*? (f <$> y) = (Sum.map (flip f) id <$> x) <*? ((· |> ·) <$> y)

References

• Selective Applicative Functors (paper)
• Haskell selective library

AI Disclosure

I used Claude Opus 4.6 to review the style, add documentation comments, and suggest changes in the Free.lean file. The code was hand-written.