Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Feature/simplify conjunctions #16

Merged
merged 10 commits into from
Jan 27, 2018
Merged

Feature/simplify conjunctions #16

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
70ac642
add a rule for simplifying conjunctions
winitzki Jan 27, 2018
c404b17
update scalac options using Rob Norris's suggestions
winitzki Jan 27, 2018
45b2782
implement better simplifications
winitzki Jan 27, 2018
34b94fe
update readme
winitzki Jan 27, 2018
f09a69e
add more tests for coverage
winitzki Jan 27, 2018
0624e4b
update tutorial
winitzki Jan 27, 2018
15b6ea7
more tests for coverage
winitzki Jan 27, 2018
c3a3609
update tutorial
winitzki Jan 27, 2018
75aa6af
add tests for some tExpr functions
winitzki Jan 27, 2018
5b2238d
update tutorial and more tests
winitzki Jan 27, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 31 additions & 16 deletions README.md
View file
Open in desktop
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
Open in desktop
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