Hedgehog.Internal.Function

Definitions

interface Cogen : Type -> Type

  An interface for co-generators, somewhat an inverse of a generator
  
  Generators, roughly, using a random seed produce a value of a certain type.
  Co-generators conversly, roughtly speaking, produce a random seed using
  a value of a certain type.
  
  Due to technical properties of a seed type, instead of generating a seed
  value from stratch we perturb some existing value.
  Thus, a function of this interface produces a `StdGen -> StdGen` function
  being given a value of an appropriate type.
  
  In some understanding, co-generators classify values of a given type, which
  allow to tune generators of other types.
  This gives an ability to generate functions of type `a -> b` being given
  a generator of type `b` and a co-generator of type `a`.
  Having a value of type `a`, co-generator can deterministically tune
  the generator of type `b` by perturbing a random seed that is used by the
  generator and use its output as an output for a function.

Parameters: a
Constructor: 

MkCogen

Methods:

perturb : a -> StdGen -> StdGen

Implementations:

Cogen ()

Cogen (x = y)

Cogen Bool

Cogen Nat

Cogen Integer

Cogen Bits64

Cogen Bits16

Cogen Bits8

Cogen Int64

Cogen Int16

Cogen Int8

Cogen Int

Cogen Char

Cogen Void

Cogen a => Cogen b => Cogen (a, b)

Cogen a => Cogen b => Cogen (Either a b)

Cogen a => Cogen (Maybe a)

Cogen a => Cogen (List a)

Cogen String

perturb : Cogen a => a -> StdGen -> StdGen

Totality: total
Visibility: public export

shiftArg : StdGen -> StdGen

  This function perturbs the given seed both with `variant` and `split`.
  
  This function is meant to be used between successive perturbations
  of different arguments of the same constructor.
  
  It is designed to not commute when perturbation actions of a constructor's
  arguments do the same.
  Consider if `Cogen` interface is implemented for `Maybe a` and `Bool`
  in the following way:
  
  ```
  Cogen a => Cogen (Maybe a) where
    perturb (Just x) = perturb x . variant 0
    perturb Nothing  = variant 1
  
  Cogen Bool where
    perturb False = variant 0
    perturb True  = variant 1
  ```
  
  In this case values `Nothing` and `Just True` would give the same
  perturbation to a seed, which is not optimal. Insertion of `shiftArg`
  before each call for `perturb` of a constructor argument would give
  different perturbations for different combinations of constructors and
  their arguments (unless you are very unlucky).
  Combination of both `variant` and `split` in the `shiftArg` function
  gives relative independence on how `perturb` of a constructor argument
  type is implemented.

Totality: total
Visibility: export

cogen : Cogen a => a -> Gen b -> Gen b

  Changes random distribution of a generator of type `b`
  based on a value of type `a`
  
  Change of distribution is done by a perturbation of a random seed,
  which is based on a `Cogen` implementation for the type `a`.

Totality: total
Visibility: export

function_ : Cogen a => Gen b -> Gen (a -> b)

  Generates a random function being given a generator of codomain type
  
  This function takes a co-generator of domain type using `auto`-argument
  based on the type.
  This generator does not shrink.
  
  Notice that this generator returns a non-showable value (unless you invent
  your own implementation).
  If you need a showable function, you have to use a shrinkable version,
  which requires more strict implementation on the domain type.

Totality: total
Visibility: export

depfun_ : Cogen a => {0 b : a -> Type} -> ((x : a) -> Gen (b x)) -> Gen ((x : a) -> b x)

  Generates a random dependently typed function being given a generator
  of codomain type family
  
  This function takes a co-generator of domain type using `auto`-argument
  based on the type.
  This generator does not shrink.
  
  Notice that this generator returns a non-showable value (unless you invent
  your own implementation).

Totality: total
Visibility: export

dargfun_ : {0 b : a -> Type} -> Cogen (b x) => Gen c -> Gen (b x -> c)

  Generates a random function with dependently typed domain being given a
  generator of codomain type
  
  This function takes a co-generator of domain type family using
  `auto`-argument based on the type.
  This generator does not shrink.
  
  Notice that this generator returns a non-showable value (unless you invent
  your own implementation).

Totality: total
Visibility: export

dargdepfun_ : {0 b : a -> Type} -> {0 c : b x -> Type} -> Cogen (b x) => ((y : b x) -> Gen (c y)) -> Gen ((y : b x) -> c y)

  Generates a random dependently typed function with dependently typed domain
  being given a generator of codomain type family
  
  This function takes a co-generator of domain type family using
  `auto`-argument based on the type.
  This generator does not shrink.
  
  Notice that this generator returns a non-showable value (unless you invent
  your own implementation).

Totality: total
Visibility: export

data (:->) : Type -> Type -> Type

  A type of reified partial functions that can be represented isomorphic
  to a function defined by pattern matching of an ADT
  or any type that *can* implement `Generic` (but does not have to).
  
  This type describes internal structure of such functions,
  e.g. storing separately "vertical" and "horizontal" matching,
  thus allowing to inspect, modify and simplify them,
  for example, for showing and shrinking.

Totality: total
Visibility: public export
Constructors:

FUnit : c -> () :-> c

FNil : a :-> c

FPair : Lazy (a :-> (b :-> c)) -> (a, b) :-> c

FSum : Lazy (a :-> c) -> Lazy (b :-> c) -> Either a b :-> c

FMap : (a -> b) -> (b -> a) -> Lazy (b :-> c) -> a :-> c

Hint: 

Functor ((a :->))

Fixity Declaration: infixr operator, level 5

interface ShrCogen : Type -> Type

Parameters: a
Constraints: Cogen a
Constructor: 

MkShrCogen

Methods:

build : (a -> c) -> a :-> c

Implementations:

ShrCogen Void

ShrCogen ()

ShrCogen a => ShrCogen b => ShrCogen (a, b)

ShrCogen a => ShrCogen b => ShrCogen (Either a b)

ShrCogen a => ShrCogen (Maybe a)

ShrCogen Bool

ShrCogen a => ShrCogen (List a)

ShrCogen (x = x)

ShrCogen Integer

ShrCogen Nat

ShrCogen Int

ShrCogen Int8

ShrCogen Int16

ShrCogen Int64

ShrCogen Bits8

ShrCogen Bits16

ShrCogen Bits64

ShrCogen Char

ShrCogen String

build : ShrCogen a => (a -> c) -> a :-> c

Totality: total
Visibility: public export

via : ShrCogen b => (a -> b) -> (b -> a) -> (a -> c) -> a :-> c

  Implements `build` function for a type through isomorphism
  to a type that implements `ShrCogen`
  
  Notice that `via f g` will only be well-behaved if
  `g . f` and `f . g` are both identity functions.

Totality: total
Visibility: export

data Fn : Type -> Type -> Type

  The type for a total randomly-generated function

Totality: total
Visibility: export
Constructor: 

MkFn : b -> a :-> Cotree b -> Fn a b

Hint: 

Show a => Show b => Show (Fn a b)

function : ShrCogen a => Gen b -> Gen (Fn a b)

  Generates a random function being given a generator of codomain type
  
  The generated function is returned in a showable type `Fn a b`.
  
  This function takes a co-generator of domain type using `auto`-argument
  based on the type.
  This generator is shrinkable. For this, it requires additional `Arg`
  argument.

Totality: total
Visibility: export

apply : Fn a b -> a -> b

  Coverts a showable randomly generated function to an actual function

Totality: total
Visibility: export

function' : ShrCogen a => Gen b -> Gen (a -> b)

  Generates a random function being given a generator of codomain type
  
  This generator is shrinkable
  
  This is a wrapper of a `function` generator.
  It may be useful sometimes, however, it returnes a non-showable type.
  To use functions generator in `forAll` in a property, use `function`
  generator.

Totality: total
Visibility: public export