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.
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))
// }
implement
)ofType
)def f[T](x: T): T
and curried syntax def f[T]: T ⇒ T
A ⇒ (B, C) ⇒ D
, in addition to using a tuple type, e.g. A ⇒ ((B, C)) ⇒ D
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.
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:
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.
sbt test
Build the tutorial (thanks to the tut plugin):
sbt tut
typeExpr
macro instead of the old test-only API. Detect and use val
s from the immediately enclosing class. Minor performance improvements and bug fixes (alpha-conversion for STLC terms). Tests for automatic discovery of some monads.implement
as well; the JVM bytecode limit is obviated; fixed bug with recognizing Function10
.:@@
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.anyOfType
; minor bug fixes. T
from AST types.allOfType
; use eta-contraction to simplify and canonicalize terms (simplify until stable); cache sequents already seen, limit the search tree by information loss score to avoid exponential blow-up in some examplesimplement
and ofType
; full implementation of LJT calculusscalaz
and cats
libraries, so that one can write implicit val x: Functor[P] = implement
curryhoward
for production code and see what new features may be desirable sealed trait
/ final case class
hierarchies.List
): generated code may fail and, in particular, cannot contain recursive functions. A non-recursive example that fails to generate sensible code: T ⇒ List[T]
(the generated code always returns empty list).ofType[Int ⇒ () ⇒ Int]
will not compile.Option[T]
, heuristics will sometimes fail to produce the desired implementation.The following code examples show how various functions are implemented automatically, given their type.
"Weak" Peirce's law:
def f[A, B]: ((((A ⇒ B) ⇒ A) ⇒ A) ⇒ B) ⇒ B = implement
"Weak" law of tertium non datur:
def f[A, B]: (Either[A, A ⇒ B] ⇒ B) ⇒ B = implement
Automatic implementations of pure
, map
, and flatMap
for the Reader
monad:
def pure[E, A]: A ⇒ (E ⇒ A) = implement
def map[E, A, B]: (E ⇒ A) ⇒ (A ⇒ B) ⇒ (E ⇒ B) = implement
def flatMap[E, A, B]: (E ⇒ A) ⇒ (A ⇒ E ⇒ B) ⇒ (E ⇒ B) = implement
Constant (non-parametric) types are treated as type parameters:
def f[A, B]: A ⇒ Int ⇒ (A, Int) = implement
f("abc")(123) // returns the tuple ("abc", 123)
Tuples, sealed traits, and case classes/case objects are supported, including Option
and Either
:
def eitherCommut[A, B]: Either[A, B] ⇒ Either[B, A] = implement
def eitherAssoc[A, B, C]: Either[A, Either[B, C]] ⇒ Either[Either[A, B], C] = implement
Case objects (and case classes with zero-argument constructors) are treated as named versions of the Unit
type.
Case classes and sealed traits can be nested and can have type parameters.
Type aliases (type P[T] = ...
) are supported as well.
Lambda-terms can be obtained and manipulated symbolically.
type R[X, A] = X ⇒ A
def mapReader[X, A, B]: R[X, A] ⇒ (A ⇒ B) ⇒ R[X, B] = implement
// mapReader is now a compiled function of the required type
val mapReaderTerm = mapReader.lambdaTerm
// mapReaderTerm is a lambda-term representing the code of mapReader
mapReaderTerm.prettyPrint // returns the string "a ⇒ b ⇒ c ⇒ b (a c)"
Symbolic computations with lambda-terms can be used for a rigorous verification of equational laws for the generated code. See the tutorial for some examples of such computations.
Code can be generated based on a given type and possibly on given values:
def f[...](...): ... = implement
-- the type and extra values are specified on the left-hand side ofType[...](...)
-- the type and extra values are specified within an expressionallOfType[...](...)
-- similar to ofType[...](...)
, except that now all inequivalent implementations with the lowest information loss are returned anyOfType[...](...)
- similar to allOfType
except all found implementations are returned, including those with higher information lossimport io.chymyst.ch._
// Conventional Scala syntax for functions.
def f1[T, U](x: T, y: T ⇒ U) : (T, U) = implement
// Fully or partially curried functions are supported.
def f2[T, U](x: T): (T ⇒ U) ⇒ (T, U) = implement
def f3[T, U]: T ⇒ (T ⇒ U) ⇒ (T, U) = implement
// Generating code within expressions.
final case class User(name: String, id: Long)
val f: Int ⇒ Long = _.toLong
ofType[User](123, "abc", f).id // This expression evaluates to `123L`.
If the implement
macro is used as the body of a class method, values from the class constructor and val
members may be used:
import io.chymyst.ch._
final case class User[A](name: String, id: A) {
def map[B](f: A ⇒ B): User[B] = implement
}
The logging options are controlled via the JVM property "curryhoward.log"
.
The value of this property is a comma-separated list of keywords.
The full logging is switched on by putting -Dcurryhoward.log=macros,terms,prover,verbose
on the Java or SBT command line.
The verbose
logging option will print the lambda-term that the macro functions generate, and a warning when more than one term was found.
The macros
logging option will print the code that the macro functions generate.
The prover
logging option will print the steps in the proof search, including the new sequents generated by each applied rule.
The trace
logging option will print more debugging information about the proof search.
The terms
logging option will print the terms generated, in the short notation.
With none of these options given, only minimal diagnostic messages are printed, with terms in a short notation:
If the theorem prover finds several alternative implementations of a type, it attempts to find the implementation with the smallest "information loss".
The "information loss" of a term is defined as an integer number being the sum of:
case
clauses that do not use their arguments,Choosing the smallest "information loss" is a heuristic that enables automatic choice of the correct implementations for a large number of cases (but, of course, not in all cases).
For example, here are correct implementations of pure
, map
, and flatMap
for the State
monad:
def pure[S, A]: A ⇒ (S ⇒ (A, S)) = implement
def map[S, A, B]: (S ⇒ (A, S)) ⇒ (A ⇒ B) ⇒ (S ⇒ (B, S)) = implement
def flatMap[S, A, B]: (S ⇒ (A, S)) ⇒ (A ⇒ S ⇒ (B, S)) ⇒ (S ⇒ (B, S)) = implement
Note that there are several inequivalent implementations for the State monad's map
and flatMap
,
but only one of them loses no information -- and thus has a higher chance of satisfying the correct laws.
The theorem prover does not check any equational laws. It selects the terms with the smallest level of information loss, in hopes that there will be only one term selected, and that it will be the desired term that satisfies equational laws of whatever sort the users expect.
The theorem prover will generate a (compile-time) error when there are two or more implementations with the smallest level of information loss.
If there are several possible implementations but only one implementation with the smallest level of information loss, the theorem prover will choose that implementation but print a warning message such as
Warning:scalac: type (S → (A, S)) → (A → B) → S → (B, S) has 2 implementations (laws need checking?)
This message means that the resulting implementation is probably the right one, but there was a choice to be made. If there exist some equational laws that apply to this function, the laws need to be checked by the user (e.g. in unit tests).
In some cases, there are several inequivalent implementations that all have the same level of "information loss."
The function allOfType
returns all these implementations.
An experimental API is provided for examining the lambda-terms corresponding to the returned implementations. The tutorial gives more detail about using that API.
The lambda-term API is experimental because, in particular, it exposes the internal implementation of STLC, which could change in future versions of curryhoward
.
The "smallest information loss" heuristic allows us to select the "better" implementation in the following example:
def optionId[X]: Option[X] ⇒ Option[X] = implement
optionId(Some(123)) == 123
optionId(None) == None
There are two possible implementations of the type Option[X] ⇒ Option[X]
: the "trivial" implementation (always returns None
), and the "interesting" implementation (returns the same value as given).
The "trivial" implementation is rejected by the algorithm because it ignores the information given in the original data, so it has higher "information loss".
Another heuristic is to prefer implementations that use more parts of a disjunction.
This avoids implementations that e.g. always generate the Some
subtype of Option
and never generate None
.
Another heuristic is to prefer implementations that preserve the order of parts in conjunctions and disjunctions.
For example,
def f[X]: ((X, X, X)) ⇒ (X, X, X) = implement
will generate the code for the identity function on triples, that is, ((a, b, c)) ⇒ (a, b, c)
.
There are many other implementations of this type, for example ((a, b, c)) ⇒ (b, c, a)
.
However, these implementations do not preserve the order of the elements in the input data, which is considered as a "loss of information".
The analogous parts-ordering heuristic is used for disjunctions, which selects the most reasonable implementation of
def f[X]: Either[X, X] ⇒ Either[X, X] = implement