Quotation

These are all interesting examples, but is there a practical side to Curry-Howard isomorphism? Probably not in everyday programming. -- Bartosz Milewski (2015), Category Theory for Programmers, Chapter 9: Function types.

The curryhoward library aims to use the Curry-Howard isomorphism as a tool for practical applications.

curryhoward

This is a library for automatic implementation of Scala expressions via the Curry-Howard isomorphism.

Quick start:

// build.sbt
libraryDependencies += "io.chymyst" %% "curryhoward" % "latest.integration"

// Scala
import io.chymyst.ch.implement

// Automatically derive code for this function, based on its type signature:
def f[X, Y]: (X ⇒ Y) ⇒ (Int ⇒ X) ⇒ (Int ⇒ Y) = implement

// The macro `implement` will automatically generate this code for the function body:
// {
//  (g: X ⇒ Y) ⇒ (r: Int ⇒ X) ⇒ (e: Int) ⇒ g(r(e))
// }

AI-generated documentation

See here

Features

Automatically fill in the function body, given the function's type alone (implement)
Automatically generate an expression of a specified type from given arguments (ofType)
Works as a macro at compile time; when a type cannot be implemented, emits a compile-time error
Supports function types, tuples, sealed traits / case classes / case objects
Can use conventional Scala syntax def f[T](x: T): T and curried syntax def f[T]: T ⇒ T
Java-style argument groups can be used, e.g. A ⇒ (B, C) ⇒ D, in addition to using a tuple type, e.g. A ⇒ ((B, C)) ⇒ D
When a type can be implemented in more than one way, heuristics ("least information loss") are used to prefer implementations that are more likely to satisfy algebraic laws
Emits a compile-time error when a type can be implemented in more than one way despite using heuristics
Debugging and logging options are available
DSL for inspecting the generated code (STLC lambda-terms) at run time; facilities are provided for symbolic evaluation and checking equational laws
Tutorial explains how to do that in detail

Usage

There are two main functions, implement and ofType.

The function implement works when defining methods, and is used syntactically as a placeholder for the method's code:

import io.chymyst.ch.implement

def f[X, Y]: X ⇒ Y ⇒ X = implement

// The code `(x: X) ⇒ (y: Y) ⇒ x` is generated for the body of the function `f`.
  
f(123)("abc") // returns 123

// The applicative `map2` function for the Reader monad.
def map2[E, A, B, C](readerA: E ⇒ A, readerB: E ⇒ B, f: A ⇒ B ⇒ C): E ⇒ C = implement
// Generates the code (e: E) ⇒ f(readerA(e), readerB(e))

The function ofType is designed for generating expressions using previously computed values:

import io.chymyst.ch.ofType

case class User(name: String, id: Long)

val x: Int = 123
val s: String = "abc"
val f: Int ⇒ Long = _.toLong // whatever

val userId = ofType[User](f, s, x).id
// Generates the expression User(s, f(x)) from previously computed values f, s, x, and returns the `id`

The generated code is purely functional and assumes that all given values and types are free of side effects.

The code is generated by the implement and ofType macros at compile time.

A compile-time error occurs when there are several inequivalent implementations for a given type, or if the type cannot be implemented at all.

See the tutorial for more details.

How it works

The macros implement and ofType examine the given type expression via reflection (at compile time). The type expression is rewritten as a formula in the intuitionistic propositional logic (IPL) with universally quantified propositions.

This is possible due to the Curry-Howard isomorphism, which maps functions with fully parametric types to theorems in the (IPL) with universally quantified propositions.

For example, the type signature of the function

def f[X, Y]: X ⇒ Y ⇒ X = (x: X) ⇒ (y: Y) ⇒ x

is mapped to the propositional theorem ∀ X : ∀ Y : X ⇒ (Y ⇒ X) in the IPL.

The resulting IPL formula is passed on to an IPL theorem prover. The theorem prover performs an exhaustive proof search to look for possible lambda-terms (terms in the simply-typed lambda-calculus, STLC) that implement the given type. After that, the terms are simplified, so that equivalent terms that are different only by alpha-conversion, beta-conversion, or eta-conversion are eliminated.

Finally, the terms are measured according to their "information loss score", and sorted so that one or more terms with the least information loss are returned (and all other terms ignored). The Scala macro then converts the lambda-term(s) into a Scala expression, which is substituted instead of implement into the right-hand side of the function definition.

All this happens at compile time, so compilation may take longer if a lot of terms are being generated.

If there are additional values available for constructing the expression, the types of those additional values are added as extra function arguments.

For example, if required to implement a type Option[B] given value x of type Option[A] and value f of type A ⇒ Option[B], the library will first rewrite the problem as that of implementing a function type Option[A] ⇒ (A ⇒ Option[B]) ⇒ Option[B] with type parameters A and B. Having obtained a solution, i.e. a term of that type, the library will then apply this term to arguments x and f. The resulting term will be returned as Scala code that uses the given values x and f.

In addition, the curryhoward library provides a DSL for manipulating the generated lambda-calculus terms symbolically. This DSL can be used to rigorously verify algebraic laws (at run time).

The current implementation uses an IPL theorem prover based on the sequent calculus called LJT as presented in:

D. Galmiche, D. Larchey-Wendling. Formulae-as-Resources Management for an Intuitionistic Theorem Prover (1998). In 5th Workshop on Logic, Language, Information and Computation, WoLLIC'98, Sao Paulo.

Some changes were made to the order of LJT rules, and some trivial additional rules implemented, in order to generate as many as possible different implementations, and also in order to support Scala case classes and case objects (i.e. named conjunctions).

The original presentation of LJT is found in:

R. Dyckhoff, Contraction-Free Sequent Calculi for Intuitionistic Logic, The Journal of Symbolic Logic, Vol. 57, No. 3, (Sep., 1992), pp. 795-807.

For a good overview of approaches to IPL theorem proving, see these talk slides:

R. Dyckhoff, Intuitionistic Decision Procedures since Gentzen (2013)

See the youtube presentation for more details about how curryhoward works.

This lecture is a pedagogical explanation of the Curry-Howard correspondence in the context of functional programming.

Unit tests

sbt test

Build the tutorial (thanks to the tut plugin):

sbt tut

Revision history

0.3.7 Implement the typeExpr macro instead of the old test-only API. Detect and use vals from the immediately enclosing class. Minor performance improvements and bug fixes (alpha-conversion for STLC terms). Tests for automatic discovery of some monads.
0.3.6 STLC terms are now emitted for implement as well; the JVM bytecode limit is obviated; fixed bug with recognizing Function10.
0.3.5 Added :@@ and @@: operations to the STLC interpreter. Fixed a bug whereby Tuple2(x._1, x._2) was not simplified to x. Fixed other bugs in alpha-conversion of type parameters.
0.3.4 Reduced verbosity by default. Fixed a bug uncovered during the demo in the February 2018 meetup presentation.
0.3.3 Automatic renaming of type variables in lambda-terms; anyOfType; minor bug fixes.
0.3.2 More aggressive simplification of named conjunctions; a comprehensive lambda-term API with a new tutorial section.
0.3.1 Code cleanups, minor fixes, first proof-of-concept for symbolic law checking via lambda-terms API.
0.3.0 Experimental API for obtaining lambda-terms. Simplified the internal code by removing the type parameter T from AST types.
0.2.4 Support named type aliases and ordering heuristics for conjunctions and disjunctions; bug fixes for conventional function types not involving type parameters and for eta-contraction
0.2.3 Fix stack overflow when using recursive types (code is still not generated for recursive functions); implement loop detection in proof search; bug fixes for alpha-conversion of type-Lambdas
0.2.2 Bug fix for back-transform in rule named-&R
0.2.1 Checking monad laws for State monad; fix some problems with alpha-conversion of type-Lambdas
0.2.0 Implement allOfType; use eta-contraction to simplify and canonicalize terms (simplify until stable); cache sequents already seen, limit

Curryhoward

Install / Use

README