Safe Haskell | None |
---|
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.
- Parse a list of declarations using one of two parsers
(
parse
orparse
) or any other suitable parser. Usecheck
to obtain a list of valid declarations. - Optional:
Parse more declarations and validate them against the previously
loaded list of valid declarations with
checkAgainst
. - Extract all valid signatures from a list of valid declarations by
filterSignatures
. - Interpret a signature (
interpret
), transform it to a theorem (asTheorem
) and pretty-print it (prettyTheorem
). - Optional: Specialise relation variables to functions
(
relationVariables
andspecialise
). - Optional: Extract lifted relations to show their definition
(
unfoldLifts
) and pretty-print them (prettyUnfoldedLift
). - Optional: Extract class constraints to show their definition
(
unfoldClasses
) and pretty-print them (prettyUnfoldedClass
). - Optional: Further simplify the Formulas (
simplify
) or UnfoldedLift (simplifyUnfoldedLift
) by syntactic transformations.
- data ValidDeclaration
- data ValidSignature
- rawDeclaration :: ValidDeclaration -> Declaration
- rawSignature :: ValidSignature -> Signature
- filterSignatures :: [ValidDeclaration] -> [ValidSignature]
- type Parsed a = Writer [Doc] a
- type Checked a = Writer [Doc] a
- runChecks :: Checked a -> (a, [Doc])
- check :: [Declaration] -> Checked [ValidDeclaration]
- checkAgainst :: [ValidDeclaration] -> [Declaration] -> Checked [ValidDeclaration]
- data LanguageSubset
- data TheoremType
- data Intermediate
- interpret :: [ValidDeclaration] -> LanguageSubset -> ValidSignature -> Maybe Intermediate
- asTheorem :: Intermediate -> Theorem
- asCompleteTheorem :: Intermediate -> Theorem
- relationVariables :: Intermediate -> [RelationVariable]
- specialise :: Intermediate -> RelationVariable -> Intermediate
- specialiseInverse :: Intermediate -> RelationVariable -> Intermediate
- unfoldLifts :: [ValidDeclaration] -> Intermediate -> [UnfoldedLift]
- unfoldClasses :: [ValidDeclaration] -> Intermediate -> [UnfoldedClass]
- simplify :: Formula -> Formula
- simplifyUnfoldedLift :: UnfoldedLift -> UnfoldedLift
- data PrettyTheoremOption
- prettyDeclaration :: Declaration -> Doc
- prettySignature :: Signature -> Doc
- prettyTheorem :: [PrettyTheoremOption] -> Theorem -> Doc
- prettyRelationVariable :: RelationVariable -> Doc
- prettyUnfoldedLift :: [PrettyTheoremOption] -> UnfoldedLift -> Doc
- prettyUnfoldedClass :: [PrettyTheoremOption] -> UnfoldedClass -> Doc
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
norChar
. - 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
norChar
. - 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 Source
Marks a valid declaration.
data ValidSignature Source
Marks a valid type signature.
rawDeclaration :: ValidDeclaration -> DeclarationSource
Returns the declaration structure hidden in a valid declaration.
rawSignature :: ValidSignature -> SignatureSource
Returns the signature structure hidden in a valid type signature.
filterSignatures :: [ValidDeclaration] -> [ValidSignature]Source
Extracts all type signatures from a list of declarations.
Manufacturing valid declarations
type Parsed a = Writer [Doc] aSource
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] aSource
A wrapper type for a Writer
which stores pretty-printable documents along
with checked values.
check :: [Declaration] -> Checked [ValidDeclaration]Source
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]Source
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 Source
Descriptions of the Haskell language subsets for which free theorems can be generated.
BasicSubset | This subset describes only terms in which no undefinedness may.
This excludes terms defined using general recursion or selective
strictness (as offered by |
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 |
SubsetWithSeq TheoremType | Additionally to the fix subset, this subset allows terms to
be defined using |
data TheoremType Source
The result type for generating free theorems.
EquationalTheorem | An equational free theorem should be generated. |
InequationalTheorem | Two inequational free theorems should be generated. |
data Intermediate Source
A structure describing the intermediate result of interpreting a type expression as a relation.
interpret :: [ValidDeclaration] -> LanguageSubset -> ValidSignature -> Maybe IntermediateSource
Interprets a valid signature as a relation. This is the key point for generating free theorems.
asTheorem :: Intermediate -> TheoremSource
Unfolds an intermediate structure to a theorem.
asCompleteTheorem :: Intermediate -> TheoremSource
Unfolds an intermediate structure to a theorem with _all_ restrictions.
relationVariables :: Intermediate -> [RelationVariable]Source
Creates a list of all bound relation variables in an intermediate structure, which can be specialised to a function.
specialise :: Intermediate -> RelationVariable -> IntermediateSource
Specialises a relation variable to a function variable in an intermediate structure.
specialiseInverse :: Intermediate -> RelationVariable -> IntermediateSource
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]Source
Extracts all lift relations and returns their definition.
unfoldClasses :: [ValidDeclaration] -> Intermediate -> [UnfoldedClass]Source
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.
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 Source
Possible options for pretty-printing theorems.
OmitTypeInstantiations | Omits all instantiations of types. This option makes theorems usually better readable. |
OmitLanguageSubsets | Omit mentioning language subsets explicitly for certain relations. |
prettyDeclaration :: Declaration -> DocSource
Pretty-prints a declaration.
prettySignature :: Signature -> DocSource
Pretty-prints a type signature.
prettyTheorem :: [PrettyTheoremOption] -> Theorem -> DocSource
Pretty-prints a theorem.
prettyRelationVariable :: RelationVariable -> DocSource
Pretty-prints a relation variable.
prettyUnfoldedLift :: [PrettyTheoremOption] -> UnfoldedLift -> DocSource
Pretty-prints an unfolded lift relation.
prettyUnfoldedClass :: [PrettyTheoremOption] -> UnfoldedClass -> DocSource
Pretty-prints an unfolded type class.