Chapter 3, addendum 1: Generating code with the Curry-Howard correspondence

Abstract:

I implemented a library for compile-time code generation from Scala type signatures. The library uses (compile-time) reflection, the Curry-Howard correspondence, and a theorem prover for the constructive propositional logic. Using this library, I illustrate how the Curry-Howard correspondence maps types into propositions and proofs into code. I will also explain some details of the algorithm I used for automatic code generation from type signatures. As an illustration of using this library for automatic code generation, I demonstrate working examples such as implementing map and flatMap for the Reader and State monads.

Contents:

How types are interpreted using propositional logic
Deriving the code of functions by hand, based on types of those functions
Using the "curryhoward" library to do the same automatically
The features of the "curryhoward" library
How the theorem prover works: the calculus LJ of Gentzen and the calculus LJT of Vorobieff-Hudelmaier-Dyckhoff
How to interpret the derivation rules for sequents
Building the lambda-calculus proof term from the proof tree
The "obvious" theorem of Vorobieff

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/curryhoward-2017.pdf

Code repository of the "curryhoward" project: https://github.com/Chymyst/curryhoward