Chymyst/curryhoward

Uses compile-time macros to derive function implementations by translating Scala type signatures into intuitionistic propositional logic formulas, then exhaustively searching for lambda-calculus terms that satisfy the proof via the LJT sequent calculus. Supports function types, tuples, sealed traits, and case classes; when multiple valid implementations exist, applies heuristics based on "information loss" to select the most likely correct solution. Integrates directly into Scala code as the `implement` and `ofType` macros, enabling zero-boilerplate generation of Reader monad operations, function composition, and other polymorphic utilities at compile time.

262 stars. No commits in the last 6 months.