Copyright	(c) Nils Anders Danielsson 2004-2022
License	See the file LICENCE.
Maintainer	http://www.cse.chalmers.se/~nad/
Stability	experimental
Portability	non-portable (GHC-specific)
Safe Haskell	None
Language	Haskell2010

Test.ChasingBottoms.Approx

Description

Synopsis

class Approx a where
- approxAll :: Nat -> a -> a
- approx :: Nat -> a -> a

Documentation

class Approx a where Source #

Approx is a class for approximation functions as described in The generic approximation lemma, Graham Hutton and Jeremy Gibbons, Information Processing Letters, 79(4):197-201, Elsevier Science, August 2001, http://www.cs.nott.ac.uk/~gmh/bib.html.

Instances are provided for all members of the Data type class. Due to the limitations of the Data.Generics approach to generic programming, which is not really aimed at this kind of application, the implementation is only guaranteed to perform correctly, with respect to the paper (and modulo any bugs), on non-mutually-recursive sum-of-products datatypes. In particular, nested and mutually recursive types are not handled correctly with respect to the paper. The specification below is correct, though (if we assume that the Data instances are well-behaved).

In practice the approxAll function can probably be more useful than approx. It traverses down all subterms, and it should be possible to prove a variant of the approximation lemma which approxAll satisfies.

Methods

approxAll :: Nat -> a -> a Source #

approxAll n x traverses n levels down in x and replaces all values at that level with bottoms.

approx :: Nat -> a -> a Source #

approx works like approxAll, but the traversal and replacement is only performed at subterms of the same monomorphic type as the original term. For polynomial datatypes this is exactly what the version of approx described in the paper above does.

Instances

Instances details

Data a => Approx a Source #
Instance details Defined in Test.ChasingBottoms.Approx Methods approxAll :: Nat -> a -> a Source # approx :: Nat -> a -> a Source #