reduce-equations: Simplify a set of equations by removing redundancies

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.


Simplify a set of equations by removing redundancies

[Skip to ReadMe]


Change logNone available
Dependenciesaeson, base (>=4.8 && <4.10), bytestring, containers, haskell-src-exts (>=1.18.2), mtl, QuickCheck, quickspec (==0.9.6), reduce-equations, stringable, text, transformers [details]
AuthorChris Warburton
Home page
Source repositoryhead: git clone
UploadedSat Nov 12 20:26:56 UTC 2016 by chriswarbo




Maintainers' corner

For package maintainers and hackage trustees

Readme for reduce-equations-

[back to package description]
# 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

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](
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.


{"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]( library to do
the actual reduction. This relies heavily on existential types and Haskell's

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 )
 - 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.