update readme (#10)

* update readme

* fix recognition of named type aliases

* update readme and tutorial

README.md

@@ -23,11 +23,17 @@ def f[X, Y]: X ⇒ Y ⇒ X = (x: X) ⇒ (y: Y) ⇒ x
 
 ```
 
-is mapped to the propositional theorem `forall X, Y : X ⇒ (Y ⇒ X)` in the IPL.
+is mapped to the propositional theorem `∀ X : ∀ Y : X ⇒ (Y ⇒ X)` in the IPL.
 
-The `curryhoward` library provides Scala macros that generate code automatically for any such function, based on the function's required type signature.
+The `curryhoward` library provides Scala macros that generate code automatically for any such function, based on the function's required type signature:
+
+```scala
+def f[X, Y]: X ⇒ Y ⇒ X = implement
+
+```
+
+The code is generated by the `implement` macro at compile time.
 
-The code is generated 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).
 
 See the [youtube presentation](https://youtu.be/cESdgot_ZxY) and the [tutorial](docs/Tutorial.md) for more details.
@@ -91,10 +97,16 @@ The current implementation uses an IPL theorem prover based on the sequent calcu
 
 [D. Galmiche, D. Larchey-Wendling. _Formulae-as-Resources Management for an Intuitionistic Theorem Prover_ (1998)](http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.2618). 	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, so that `curryhoward` can generate all possible implementations rather than just some, and also to support case classes (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](https://rd.host.cs.st-andrews.ac.uk/publications/jsl57.pdf).
 
+For a good overview of approaches to IPL theorem proving, see these talk slides:
+
+[R. Dyckhoff, _Intuitionistic Decision Procedures since Gentzen_ (2013)](http://apt13.unibe.ch/slides/Dyckhoff.pdf)
+
 # Unit tests
 
 `sbt test`
@@ -104,9 +116,9 @@ The original presentation of LJT is found in:
 - The theorem prover for the full IPL is working
 - When a type cannot be implemented, signal a compile-time error
 - Debugging options are available
-- Support for `Unit` type, constant types, type parametrs, function types, tuples, sealed traits / case classes / case objects
+- Support for `Unit` type, constant types, type parameters, function types, tuples, sealed traits / case classes / case objects
 - Both conventional Scala syntax `def f[T](x: T): T` and curried syntax `def f[T]: T ⇒ T` can be used
-- 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 
+- 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
 - Tests and a tutorial
 
@@ -119,7 +131,6 @@ The original presentation of LJT is found in:
 # Known bugs
 
 - Limited support for recursive case classes (including `List`): generated code cannot contain recursive functions
-- Type aliases `type MyType[T] = (Int, T)` are not supported - they will silently generate incorrect code or fail
 - No support for the conventional Java-style function types with multiple arguments, e.g. `(T, U) ⇒ T`; tuple types need to be used instead, e.g. `((T, U)) ⇒ T`
 
 # Examples of working functionality
@@ -165,7 +176,7 @@ def eitherAssoc[A, B, C]: Either[A, Either[B, C]] ⇒ Either[Either[A, B], C] =
 
 Case objects (and case classes with zero-argument constructors) are treated as named versions of the `Unit` type.
 
-## Supported syntax in depth
+## Supported syntax
 
 There are three ways in which code can be generated based on a given type:
 
@@ -201,9 +212,12 @@ The "information loss" of a term is defined as an integer number being the sum o
 
 - the number of (curried) arguments that are ignored by some function,
 - the number of tuple parts that are computed but subsequently not used,
-- the number of `case` clauses that do not use their arguments.
+- the number of `case` clauses that do not use their arguments,
+- the number of disjunction or conjunction parts that are inserted out of order,
+- the number of times an input value is used (if more than once).
+
+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).
 
-Choosing the smallest "information loss" is a heuristic that enables automatic choice of the correct implementations for a number of cases.
 For example, here are correct implementations of `pure`, `map`, and `flatMap` for the `State` monad:
 
 ```scala
@@ -233,6 +247,11 @@ Warning:scalac: type (S → (A, S)) → (A → B) → S → (B, S) has 2 impleme
 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.
+
+### Examples of heuristic choice
+
 The "smallest information loss" heuristic allows us to select the "better" implementation in the following example:
 
 ```scala
@@ -246,7 +265,34 @@ 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".
 
-As another heuristic, the algorithm prefers implementations that use more parts of a disjunction.
+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`.
 
-In some cases, there are several inequivalent implementations that all have the same level of "information loss."
-The function `allOfType` returns all these implementations.
+Another heuristic is to prefer implementations that preserve the order of parts in conjunctions and disjunctions.
+
+For example,
+
+```scala
+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
+
+```scala
+def f[X]: Either[X, X] ⇒ Either[X, X] = implement
+
+```
+
+# Revision history
+
+- 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