# Reduce Equations #

This package provides a command `reduce-equations` which reads in a list of
equations from stdin, performs some simplification, and writes the results to
stdout.

For example, given the equations `a = b`, `b = c` and `a = c`, one of these will
be removed as it can be inferred from the other two. Similarly, given equations
`f a = g`, `f b = g` and `a = b`, one of the first equations will be removed as
it can be recovered by subtitution.

All of the real work is done by [QuickSpec](https://hackage.haskell.org/package/quickspec)
This package just provides stdio and machine-friendly formatting.

## Formats ##

All IO is encoded in JSON. Both stdin and stdout should contain a single array
of equations. The following example gives a single equation, which if written in
a more human-friendly form, would be `plus x x = times x 2`:

```
[
 {"relation": "~=",
  "lhs":      {"role": "application",
               "lhs":  {"role": "application",
                        "lhs":  {"role":   "constant",
                                 "type":   "Int -> Int -> Int",
                                 "symbol": "plus"},
                        "rhs":  {"role": "variable",
                                 "type": "Int",
                                 "id":   0}},
               "rhs":  {"role": "variable",
                        "type": "Int",
                        "id":   0}},
  "rhs":      {"role": "application",
               "lhs":  {"role": "application",
                        "lhs":  {"role":   "constant",
                                 "type":   "Int -> Int -> Int",
                                 "symbol": "times"},
                        "rhs":  {"role": "variable",
                                 "type": "Int",
                                 "id":   0}},
               "rhs":  {"role":   "constant",
                        "type":   "Int",
                        "symbol": "two"}}}
]
```

### Equations ###

An equation is an object with the following values:

 - `relation`: This is used mostly to identify that we've got an equation. In
   practice, this is always `"~="` (what that means is up to you).
 - `lhs`: this is a `term`, supposedly the left-hand-side of the equation,
   although the only difference from `rhs` is the name.
 - `rhs`: this is a `term`, just like `lhs` except it's the right-hand-side.

Example:

```
{"relation": "~=",
  "lhs":     {"role": "application",
              "lhs":  {"role":   "constant",
                       "type":   "Bool -> Bool",
                       "symbol": "not"},
              "rhs":  {"role": "application",
                       "lhs": {"role":   "constant",
                               "type":   "Bool -> Bool",
                               "symbol": "not"},
                       "rhs": {"role": "variable",
                               "type": "Bool",
                               "id": 0}}},
  "rhs":     {"role": "variable",
              "type": "Bool",
              "id":   0}}
```

### Terms ###

A term is an object containing a `role`, which is one of `"constant"`,
`"variable"` or `"application"`. The other fields depend on what the term's
`role` is:

 - Constants
    - `type`: The type of the constant, a string written in Haskell's type
      notation. This is taken from the given function descriptions. For example
      `"Int -> (Int -> Bool) -> IO Float"`
    - `symbol`: The name of the constant, as a string. For example `"reverse"`.
 - Variables
    - `type`: The type of the variable, a string written in Haskell's type
      notation. The types can be made up, but they should be consistent (e.g.
      both sides of an equation should have the same type; application should be
      well-typed; etc.). Unification of polymorphic types isn't supported; types
      are identified syntactically. For example `"[Int]"`.
    - `"id"`: A numeric ID for the variable. IDs start at `0`. Used to
      distinguish between multiple variables of the same type. Variable ID only
      matters within a single equation. For example, to represent three integer
      variables we might use `{"role": "variable", "type": "Int", "id":0}`,
      `{"role": "variable", "type": "Int", "id":1}` and
      `{"role": "variable", "type": "Int", "id":2}`.
 - Applications
    - `lhs`: A term representing a function to apply.
    - `rhs`: A term representing the argument to apply the `lhs` function to.
      Functions are curried, so calling with multiple arguments should be done
      via a left-leaning tree.

## Implementation Notes ##

We co-opt the equation-reducing machinery of the
[QuickSpec](https://hackage.haskell.org/package/quickspec-0.9.6) library to do
the actual reduction. This relies heavily on existential types and Haskell's
[Typeable](https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-Typeable.html)
mechanism.

Since the incoming equations may have arbitrary types, and GHC doesn't let us
define custom `Typeable` instances, we perform a conversion step:

 - Once an array of equations has been parsed, we recurse through the terms and
   switch out each distinct type with a freshly-generated replacement, of the
   form `Z`, `S Z`, `S (S Z)`, etc. (these are just Peano numerals, e.g. see
   https://en.wikipedia.org/wiki/Successor_function )
 - We provide special functions `getRep` and `getVal` to plumb these Peano types
   into QuickSpec's machinery, convincing it that we have a signature of
   well-typed terms.
 - We reduce the given equations, with their switched-out types, to get a
   reduced set.
 - We switch back the types for presentation purposes, pretty-printing to JSON.