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