free-theorems: Automatic generation of free theorems.

[ language, library, public-domain ] [ Propose Tags ] [ Report a vulnerability ]

The free-theorems library allows to automatically generate free theorems from Haskell type expressions. It supports nearly all Haskell 98 types except of type constructor classes, and in addition it can also handle higher-rank functions. Free theorems are generated for three different sublanguages of Haskell, a basic one corresponding to the polymorphic lambda-calculus of Girard-Reynolds, an extension of that allowing for recursion and errors, and finally a sublanguage additionally allowing seq. In the last two sublanguages, also inequational free theorems may be derived in addition to classical equational results.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.2, 0.2.1, 0.3, 0.3.1, 0.3.1.1, 0.3.1.2, 0.3.1.3, 0.3.2.0, 0.3.2.1
Dependencies base (>=1), containers (>=0.1.0.1), haskell-src (>=1.0), mtl (>=1.0), pretty (>=1.0.0.0), syb (>=0.1.0.0) [details]
Tested with ghc ==7.6.1
License LicenseRef-PublicDomain
Author Sascha Boehme
Maintainer voigt@tcs.inf.tu-dresden.de
Category Language
Uploaded by JoachimBreitner at 2022-12-21T12:50:49Z
Distributions
Reverse Dependencies 3 direct, 0 indirect [details]
Downloads 6678 total (27 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2022-12-21 [all 1 reports]

Readme for free-theorems-0.3.2.1

[back to package description]
  DESCRIPTION

This library may be used to automatically generate free theorems
[1,2] from Haskell type signatures. It supports Haskell 98 and 
additionally higher-rank functions. Beside primitive Haskell types
(Int, Integer, Float, Double, Char), it already includes lists and
tuples. The library provides means to add other data types.



  DEPENDENCIES

See the file `free-theorems.cabal' for dependencies. Note that there,
two parser libraries are listed. If only one is needed, the library
is easily adjustable by commenting out the corresponding dependencies
and exported modules.


  
  INSTALL

Since this library is cabalised, it uses the standard installation
process.
  
  runhaskell Setup.lhs configure
  runhaskell Setup.lhs build
  runhaskell Setup.lhs install



  USAGE

See the Haddock-generated documentation for detailed information on
how to use this library.



  DOCUMENTATION

If Haddock is available, documentation may be 
generated automatically from the sources.
  
  runhaskell Setup.lhs haddock



-------

[1] Philip Wadler, Theorems for free!, In Functional Programming
    Languages and Computer Architecture, Proceedings, 1989.

[2] Patricia Johann and Janis Voigtländer, The Impact of seq on Free
    Theorems-Based Program Transformations, In Fundamenta 
    Informaticae, 2006.