Skip to content

Commit

Permalink
Feature/simplify conjunctions (#16)
Browse files Browse the repository at this point in the history 
* add a rule for simplifying conjunctions

* update scalac options using Rob Norris's suggestions

* implement better simplifications

* update readme

* add more tests for coverage

* update tutorial

* more tests for coverage

* update tutorial

* add tests for some tExpr functions

* update tutorial and more tests
  • Loading branch information
@winitzki
winitzki committed Jan 27, 2018
1 parent 13b9a45 commit d92e180
Show file tree
Hide file tree
Showing 9 changed files with 742 additions and 93 deletions.
47 changes: 31 additions & 16 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,12 +32,17 @@ def f[X, Y]: X ⇒ Y ⇒ X = implement

```

The type signature is converted to an IPL formula, a proof search is performed, and if a suitable proof term (using simply-typed lambda-calculus) is found,
it is converted to a Scala expression and substituted instead of `implement` into the right-hand side of the function definition.

The code is generated by the `implement` macro 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 (i.e. when the given propositional formula is not a theorem).
A compile-time error occurs when there are several inequivalent implementations for a given type, or if the type cannot be implemented at all (i.e. when the given propositional formula is not a true theorem).

See the [youtube presentation](https://youtu.be/cESdgot_ZxY) and the [tutorial](docs/Tutorial.md) for more details.

In addition, the `curryhoward` library provides a DSL for computing with the generated lambda-calculus terms symbolically, in order to rigorously verify algebraic laws (at run time).

# Usage

There are two main functions, `implement` and `ofType`.
Expand Down Expand Up @@ -111,6 +116,22 @@ For a good overview of approaches to IPL theorem proving, see these talk slides:

`sbt test`

Build the tutorial (thanks to the [tut plugin](https://github.com/tpolecat/tut)):

`sbt tut`

# Revision history

- 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 the search tree by information loss score to avoid exponential blow-up in some examples
- 0.1.0 Initial release; support case classes and tuples; support `implement` and `ofType`; full implementation of LJT calculus

# Status

- The theorem prover for the full IPL is working
Expand All @@ -121,7 +142,7 @@ For a good overview of approaches to IPL theorem proving, see these talk slides:
- Java-style argument groups can be used, e.g. `A => (B, C) => D`, which is not the same as using a tuple type: `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
- Signal error when a type can be implemented in more than one way despite using heuristics
- Generated lambda-terms can be inspected at run time, and laws checked symbolically
- Generated lambda-terms can be inspected and manipulated at run time, and equational laws can be checked symbolically
- Tests and a tutorial

# To-do items
Expand All @@ -137,11 +158,16 @@ For a good overview of approaches to IPL theorem proving, see these talk slides:

The following code examples show how various functions are implemented automatically, given their type.

"Weak" Peirce's law:

```scala
// "Weak" Peirce's law:
def f[A, B]: ((((A ⇒ B) ⇒ A) ⇒ A) ⇒ B) ⇒ B = implement

// "Weak" law of _tertium non datur_:
```

"Weak" law of _tertium non datur_:

```scala
def f[A, B]: (Either[A, A ⇒ B] ⇒ B) ⇒ B = implement

```
Expand All @@ -155,7 +181,7 @@ def flatMap[E, A, B]: (E ⇒ A) ⇒ (A ⇒ E ⇒ B) ⇒ (E ⇒ B) = implement

```

Constant types are treated as type parameters.
Constant (non-parametric) types are treated as type parameters:

```scala

Expand Down Expand Up @@ -308,14 +334,3 @@ The analogous parts-ordering heuristic is used for disjunctions, which selects t
def f[X]: Either[X, X] ⇒ Either[X, X] = implement

```

# Revision history

- 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 the search tree by information loss score to avoid exponential blow-up in some examples
- 0.1.0 Initial release; support case classes and tuples; support `implement` and `ofType`; full implementation of LJT calculus
116 changes: 85 additions & 31 deletions build.sbt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,62 +7,116 @@ lazy val common = Seq(
)
)

// Uncomment this and the tut dependency in plugin.sbt in order to build the tutorial.
// Do `sbt tut` to build the tutorial.
enablePlugins(TutPlugin)

tutSourceDirectory := (sourceDirectory in curryhoward in Compile).value / "tut"
tutTargetDirectory := baseDirectory.value / "docs" //(crossTarget in core).value / "tut"
scalacOptions in Tut := scalacOptions.value.filterNot(disableWarningsForTut.contains)

lazy val disableWarningsForTut = Set("-Ywarn-unused", "-Xlint", "-Ywarn-unused-import")
lazy val disableWarningsForTut = Set("-Ywarn-unused", "-Xlint", "-Ywarn-unused-import", "-Ywarn-unused:imports")

lazy val errorsForWartRemover = Seq(Wart.EitherProjectionPartial, Wart.Enumeration, Wart.ExplicitImplicitTypes, Wart.FinalCaseClass, Wart.FinalVal, Wart.LeakingSealed, Wart.Return, Wart.StringPlusAny, Wart.TryPartial)

lazy val warningsForWartRemover = Seq(Wart.Equals, Wart.JavaConversions, Wart.IsInstanceOf, Wart.OptionPartial, Wart.TraversableOps) //Seq(Wart.Any, Wart.AsInstanceOf, Wart.ImplicitConversion, Wart.Option2Iterable, Wart.NoNeedForMonad, Wart.Nothing, Wart.Product, Wart.Serializable, Wart.ToString, Wart.While)

// See http://tpolecat.github.io/2017/04/25/scalac-flags.html
lazy val scalacOptionsRobNorris = Seq(
"-deprecation", // Emit warning and location for usages of deprecated APIs.
"-encoding", "UTF-8", // Specify character encoding used by source files.
"-explaintypes", // Explain type errors in more detail.
"-feature", // Emit warning and location for usages of features that should be imported explicitly.
"-language:existentials", // Existential types (besides wildcard types) can be written and inferred
"-language:experimental.macros", // Allow macro definition (besides implementation and application)
"-language:higherKinds", // Allow higher-kinded types
"-language:implicitConversions", // Allow definition of implicit functions called views
"-unchecked", // Enable additional warnings where generated code depends on assumptions.
"-Xcheckinit", // Wrap field accessors to throw an exception on uninitialized access.
// "-Xfatal-warnings", // Fail the compilation if there are any warnings.
"-Xfuture", // Turn on future language features.
"-Xlint:adapted-args", // Warn if an argument list is modified to match the receiver.
"-Xlint:by-name-right-associative", // By-name parameter of right associative operator.
"-Xlint:delayedinit-select", // Selecting member of DelayedInit.
"-Xlint:doc-detached", // A Scaladoc comment appears to be detached from its element.
"-Xlint:inaccessible", // Warn about inaccessible types in method signatures.
"-Xlint:infer-any", // Warn when a type argument is inferred to be `Any`.
"-Xlint:missing-interpolator", // A string literal appears to be missing an interpolator id.
"-Xlint:nullary-override", // Warn when non-nullary `def f()' overrides nullary `def f'.
"-Xlint:nullary-unit", // Warn when nullary methods return Unit.
"-Xlint:option-implicit", // Option.apply used implicit view.
"-Xlint:package-object-classes", // Class or object defined in package object.
"-Xlint:poly-implicit-overload", // Parameterized overloaded implicit methods are not visible as view bounds.
"-Xlint:private-shadow", // A private field (or class parameter) shadows a superclass field.
"-Xlint:stars-align", // Pattern sequence wildcard must align with sequence component.
"-Xlint:type-parameter-shadow", // A local type parameter shadows a type already in scope.
"-Xlint:unsound-match", // Pattern match may not be typesafe.
"-Yno-adapted-args", // Do not adapt an argument list (either by inserting () or creating a tuple) to match the receiver.
"-Ypartial-unification", // Enable partial unification in type constructor inference
"-Ywarn-dead-code", // Warn when dead code is identified.
"-Ywarn-inaccessible", // Warn about inaccessible types in method signatures.
"-Ywarn-infer-any", // Warn when a type argument is inferred to be `Any`.
"-Ywarn-nullary-override", // Warn when non-nullary `def f()' overrides nullary `def f'.
"-Ywarn-nullary-unit", // Warn when nullary methods return Unit.
"-Ywarn-numeric-widen", // Warn when numerics are widened.
"-Ywarn-value-discard" // Warn when non-Unit expression results are unused.
)

lazy val scalacOptionsRobNorris212AndAbove = Seq(
"-Xlint:constant", // Evaluation of a constant arithmetic expression results in an error.
"-Ywarn-extra-implicit", // Warn when more than one implicit parameter section is defined.
"-Ywarn-unused:implicits", // Warn if an implicit parameter is unused.
"-Ywarn-unused:imports", // Warn if an import selector is not referenced.
"-Ywarn-unused:locals", // Warn if a local definition is unused.
"-Ywarn-unused:params", // Warn if a value parameter is unused.
"-Ywarn-unused:patvars", // Warn if a variable bound in a pattern is unused.
"-Ywarn-unused:privates" // Warn if a private member is unused.
)

lazy val myScalacOptions = Seq(
"-deprecation",
"-unchecked",
"-encoding", "UTF-8",
"-feature",
"-language:existentials",
"-language:higherKinds",
"-language:implicitConversions",
"-Ydelambdafy:inline",
"-Xlint",
"-Yno-adapted-args", // Makes calling a() fail to substitute a Unit argument into a.apply(x: Unit)
"-Ywarn-dead-code", // N.B. doesn't work well with the ??? hole
"-Ywarn-numeric-widen",
"-Ywarn-value-discard",
"-Xfuture",
"-Ywarn-unused",
"-Ywarn-unused-import",
"-Xexperimental",
"-target:jvm-1.8"
)

lazy val curryhoward: Project = (project in file("."))
.settings(common)
.settings(
organization := "io.chymyst",
version := "0.3.1",
version := "0.3.2",

licenses := Seq("Apache License, Version 2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0.txt")),
homepage := Some(url("https://github.com/Chymyst/curryhoward")),
description := "Automatic code generation from function types using the Curry-Howard correspondence",

// scalacOptions += "-Ymacro-debug-lite",
scalacOptions ++= Seq(
"-deprecation",
"-unchecked",
"-encoding", "UTF-8",
"-feature",
"-language:existentials",
"-language:higherKinds",
"-language:implicitConversions",
"-Ydelambdafy:inline",
// "-Xfatal-warnings",
"-Xlint",
"-Yno-adapted-args", // Makes calling a() fail to substitute a Unit argument into a.apply(x: Unit)
"-Ywarn-dead-code", // N.B. doesn't work well with the ??? hole
"-Ywarn-numeric-widen",
"-Ywarn-value-discard",
"-Xfuture",
"-Ywarn-unused",
"-Ywarn-unused-import", "-Xexperimental",
"-target:jvm-1.8"
),
scalacOptions ++= (
if (scalaBinaryVersion.value != "2.11") Seq(
"-target:jvm-1.8",
"-opt:l:inline",
"-Ypartial-unification",
"-Yvirtpatmat"
)
scalacOptions ++= (scalacOptionsRobNorris ++ myScalacOptions ++ (
if (scalaBinaryVersion.value != "2.11")
scalacOptionsRobNorris212AndAbove ++ Seq(
"-opt:l:inline",
"-Ypartial-unification",
"-Yvirtpatmat"
)
else Nil
), // (SI-2712 pertains to partial-unification),
)).distinct, // (SI-2712 pertains to partial-unification)

wartremoverWarnings in(Compile, compile) ++= warningsForWartRemover,
wartremoverErrors in(Compile, compile) ++= errorsForWartRemover,
scalacOptions in (Compile, console) --= Seq("-Ywarn-unused:imports", "-Ywarn-unused-import", "-Xfatal-warnings"),

libraryDependencies ++= Seq(
// We need scala-reflect because we use macros.
Expand Down
Loading

0 comments on commit d92e180

Please sign in to comment.