Last updated: 2018-06-02 15:24:59 +0100

Upstream URL: git clone http://chriswarbo.net/git/mlspec.git

Repo

View repository

View issue tracker

Contents of README follows

MLSpec: Machine Learning for QuickSpec

This project constructs “theories” for the QuickSpec system to explore.

It reads from stdin or a filename argument, and parses a JSON array of arrays of function descriptions.

A function description looks like:

{
    "package" : "foo"
  , "module"  : "Bar.Baz"
  , "name"    : "quux"
  , "type"    : "Bar.T a -> Baz.U b"
  , "arity"   : 1
}

Each array will be turned into a QuickSpec signature and explored.

Equations found by all of these explorations are printed to stdout as JSON objects, one per line.

Formatting

Equations

Each equation is an object with the following fields:

• relation: This has no real meaning, it’s basically a tag for distinguishing that this is an equation. The value will be "~=", to indicate that it was found by QuickSpec and is hence only tested rather than formally proven.
• lhs: a term representing the left-hand-side of the equation. There’s no conceptual difference between the left and right, they’re just names.
• rhs: a term representing the right-hand-side of the equation. Again, no real difference from the left hand side except the name.

Terms

A term is an object, with a role field containing one of "constant", "variable" or "application". The other fields depend on the term’s role:

• 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. Variables are automatically added to a signature to be used as arguments to the given functions. For example "[Int]".
  • "id": A numeric ID for the variable. IDs start at 0. Three variables are added for each argument type. 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 use the nix-eval package to run QuickSpec with all of the required packages available. If some packages aren’t in the default GHC package database, nix-eval will call the nix-shell command, so you’ll need a working installation of Nix in your path.

We include a Cabal test suite to check internal function behaviour. We also include an executable mlspec-test-quickspec for integration tests which use QuickSpec. We also have a test.sh script which invokes these as well as running various examples through the MLSpec executable.