Language.Haskell.FreeTheorems

Data structures and functions to automatically generate free theorems.

This library is based on the following papers:

• Theorems For Free!, Philip Wadler, in Functional Programming Languages and Computer Architecture Proceedings, 1989. http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps
• The Impact of seq on Free Theorems-Based Program Transformations, Patricia Johann and Janis Voigtländer, Fundamenta Informaticae, 2006. http://www.orchid.inf.tu-dresden.de/~voigt/seqFinal.pdf

The intended usage of this library is as follows.

1. Parse a list of declarations using one of two parsers (parse or parse) or any other suitable parser. Use check to obtain a list of valid declarations.
2. Optional: Parse more declarations and validate them against the previously loaded list of valid declarations with checkAgainst.
3. Extract all valid signatures from a list of valid declarations by filterSignatures.
4. Interpret a signature (interpret), transform it to a theorem (asTheorem) and pretty-print it (prettyTheorem).
5. Optional: Specialise relation variables to functions (relationVariables and specialise).
6. Optional: Extract lifted relations to show their definition (unfoldLifts) and pretty-print them (prettyUnfoldedLift).
7. Optional: Extract class constraints to show their definition (unfoldClasses) and pretty-print them (prettyUnfoldedClass).
8. Optional: Further simplify the Formulas (simplify) or UnfoldedLift (simplifyUnfoldedLift) by syntactic transformations.

Valid declarations

The restrictions on valid declarations and valid type signatures, above what is already ensured by the stucture of declarations (see Language.Haskell.FreeTheorems.Syntax), are as follows:

For data and newtype declarations:

• The declared type constructor is not a primitive type, i.e. it is not equal to Int, Integer, Float, Double nor Char.
• The variables occurring on the right-hand side have to be mentioned on the left-hand side, and the left-hand side variables are pairwise distinct.
• There is at least one data constructor in the declaration of an algebraic data type.
• The declaration is not nested, i.e. if the declared type constructor occurs on the right-hand side, it has only type variables as arguments.
• No FixedTypeExpression occurs in any type expression on the right-hand side.
• After replacing all type synonyms: No function type constructor and no type abstraction occurs on the right-hand side.

For type declarations:

• The declared type constructor is not a primitive type, i.e. it is not equal to Int, Integer, Float, Double nor Char.
• The variables occurring on the right-hand side have to be mentioned on the left-hand side, and the left-hand side variables are pairwise distinct.
• The declaration is not recursive, i.e. if the declared type constructor occurs nowhere on the right-hand side.
• There is no group of type declarations which are mutually recursive.
• No FixedTypeExpression occurs in the type expression on the right-hand side.

For class declarations:

• The declared type class does not equal a primitive type.
• The names of the class methods are pairwise distinct.
• The class variable occurs in the type expression of every class method.
• The name of the class does not occur in a type expression of any class method.
• No FixedTypeExpression occurs in a type expression of any class method.
• The type class hierarchy is acyclic.

For type signatures:

• No FixedTypeExpression occurs in the type expression of a signature.

Additionally, the following global restrictions need to hold:

• There may be at most one declaration only for every name.
• Every type class occurring in any type expression is declared.
• Every type constructor occurring in any type expression is declared. Furthermore, the number of arguments to every type constructor has to match the number of type variables the given on the left-hand side of the declaration of that type constructor.

Type synonyms do not occur in type expressions of valid declarations. Every type expression of a valid declaration is closed. A special case are class methods. Their types have the class variable as the only free type variable.

data ValidDeclaration

Marks a valid declaration.

data ValidSignature

Marks a valid type signature.

rawDeclaration :: ValidDeclaration -> Declaration

Returns the declaration structure hidden in a valid declaration.

rawSignature :: ValidSignature -> Signature

Returns the signature structure hidden in a valid type signature.

filterSignatures :: [ValidDeclaration] -> [ValidSignature]

Extracts all type signatures from a list of declarations.

Manufacturing valid declarations

type Parsed a = Writer [Doc] a

A wrapper type for Writer which stores pretty-printable documents along with parsed values. This type is provided as standard return type for parsers.

type Checked a = Writer [Doc] a

A wrapper type for a Writer which stores pretty-printable documents along with checked values.

runChecks :: Checked a -> (a, [Doc])

A wrapper function for runWriter.

check :: [Declaration] -> Checked [ValidDeclaration]

Checks a list of declarations. It returns a list of all declarations which are valid and an error message for all those declarations which are not valid.

checkAgainst :: [ValidDeclaration] -> [Declaration] -> Checked [ValidDeclaration]

Checks a list of declarations against a given list of valid declarations. It returns a list of all declarations from the second argument which are valid. Moreover, the result contains an error message for all those declarations which are not valid.

The declarations given in the second argument may be based on those of the first argument. For example, if the first argument contains a valid declaration of a type "Foo" and if the second argument contains the following declaration

 type Bar = Foo

then also the declaration of "Bar" is valid.

Generating free theorems

data LanguageSubset

Descriptions of the Haskell language subsets for which free theorems can be generated.

Constructors

BasicSubset

This subset describes only terms in which no undefinedness may. This excludes terms defined using general recursion or selective strictness (as offered by seq).

SubsetWithFix TheoremType

This subset describes terms in which undefined values may occur such as introduced by a fixpoint combinator or possibly failing pattern matches (if not all cases are covered). This excludes any term based on seq.

SubsetWithSeq TheoremType

Additionally to the fix subset, this subset allows terms to be defined using seq.

Instances

Eq LanguageSubset

Data LanguageSubset

Typeable LanguageSubset

data TheoremType

The result type for generating free theorems.

Constructors

EquationalTheorem

An equational free theorem should be generated.

InequationalTheorem

Two inequational free theorems should be generated.

Instances

Eq TheoremType

Data TheoremType

Typeable TheoremType

data Intermediate

A structure describing the intermediate result of interpreting a type expression as a relation.

interpret :: [ValidDeclaration] -> LanguageSubset -> ValidSignature -> Maybe Intermediate

Interprets a valid signature as a relation. This is the key point for generating free theorems.

asTheorem :: Intermediate -> Theorem

Unfolds an intermediate structure to a theorem.

asCompleteTheorem :: Intermediate -> Theorem

Unfolds an intermediate structure to a theorem with _all_ restrictions.

relationVariables :: Intermediate -> [RelationVariable]

Creates a list of all bound relation variables in an intermediate structure, which can be specialised to a function.

specialise :: Intermediate -> RelationVariable -> Intermediate

Specialises a relation variable to a function variable in an intermediate structure.

specialiseInverse :: Intermediate -> RelationVariable -> Intermediate

Specialises a relation variable to an inverse function variable. This function does not modify intermediate structures in subsets with equational theorems.

unfoldLifts :: [ValidDeclaration] -> Intermediate -> [UnfoldedLift]

Extracts all lift relations and returns their definition.

unfoldClasses :: [ValidDeclaration] -> Intermediate -> [UnfoldedClass]

Extracts all class constraints and returns their definition.

Simplifications

These syntactic transformations are only valid for equational theorems in the basic subset or the subset with fix, as eta reduction will be tried.

simplify :: Formula -> Formula

simplifyUnfoldedLift :: UnfoldedLift -> UnfoldedLift

Pretty printing

The pretty printer is based on the module "Text.PrettyPrint" which is usually implemented by "Text.PrettyPrint.HughesPJ". See there for information on how to modify documents.

data PrettyTheoremOption

Possible options for pretty-printing theorems.

Constructors

OmitTypeInstantiations

Omits all instantiations of types. This option makes theorems usually better readable.

OmitLanguageSubsets

Omit mentioning language subsets explicitly for certain relations.

Instances

Eq PrettyTheoremOption

prettyDeclaration :: Declaration -> Doc

Pretty-prints a declaration.

prettySignature :: Signature -> Doc

Pretty-prints a type signature.

prettyTheorem :: [PrettyTheoremOption] -> Theorem -> Doc

Pretty-prints a theorem.

prettyRelationVariable :: RelationVariable -> Doc

Pretty-prints a relation variable.

prettyUnfoldedLift :: [PrettyTheoremOption] -> UnfoldedLift -> Doc

Pretty-prints an unfolded lift relation.

prettyUnfoldedClass :: [PrettyTheoremOption] -> UnfoldedClass -> Doc

Pretty-prints an unfolded type class.