Search.HDecidable

The content of this module is based on the paper
Applications of Applicative Proof Search
by Liam O'Connor
https://doi.org/10.1145/2976022.2976030

Definitions

record HDec : Type -> Type

  Half a decider: when the search succeeds we bother building the proof

Totality: total
Visibility: public export
Constructor: 

MkHDec : (isTrue : Bool) -> (So isTrue -> a) -> HDec a

Projections:

.evidence : ({rec:0} : HDec a) -> So (isTrue {rec:0}) -> a

.isTrue : HDec a -> Bool

Hints:

Alternative HDec

AnHDec HDec

Applicative HDec

Functor HDec

Monad HDec

Show f => Show (HDec f)

.isTrue : HDec a -> Bool

Totality: total
Visibility: public export

isTrue : HDec a -> Bool

Totality: total
Visibility: public export

.evidence : ({rec:0} : HDec a) -> So (isTrue {rec:0}) -> a

Totality: total
Visibility: public export

evidence : ({rec:0} : HDec a) -> So (isTrue {rec:0}) -> a

Totality: total
Visibility: public export

yes : a -> HDec a

  Happy path: we have found a proof!

Totality: total
Visibility: public export

no : HDec a

  Giving up

Totality: total
Visibility: public export

fromDec : Dec a -> HDec a

Totality: total
Visibility: public export

fromMaybe : Maybe a -> HDec a

Totality: total
Visibility: public export

toMaybe : HDec a -> Maybe a

Totality: total
Visibility: public export

interface AnHDec : (Type -> Type) -> Type

  A type constructor satisfying AnHdec is morally an HDec i.e. we can
  turn values of this type constructor into half deciders
  It may be more powerful (like Dec) or more basic (like Maybe).

Parameters: t
Methods:

toHDec : t a -> HDec a

Implementations:

AnHDec Dec

AnHDec HDec

AnHDec Maybe

toHDec : AnHDec t => t a -> HDec a

Totality: total
Visibility: public export

(&&) : (AnHDec l, AnHDec r) => l a -> r b -> HDec (a, b)

  Half deciders are closed under product

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 5

(||) : (AnHDec l, AnHDec r) => l a -> r b -> HDec (Either a b)

  Half deciders are closed under sum

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

not : (AnHDec l, Negates na a) => l na -> HDec (Not a)

  Half deciders are closed negation. Here we use the `Negates` interface
  so that we end up looking for *positive* evidence of something which is
  much easier to find than negative one.

Totality: total
Visibility: public export

(==>) : (AnHDec l, (AnHDec r, Negates na a)) => l na -> r b -> HDec (a -> b)

  Half deciders are closed under implication

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 3

any : AnHDec l => (xs : List a) -> ((x : a) -> l (p x)) -> HDec (Any p xs)

  Half deciders are closed under the list quantifier any

Totality: total
Visibility: public export

all : AnHDec l => (xs : List a) -> ((x : a) -> l (p x)) -> HDec (All p xs)

  Half deciders are closed under the list quantifier all

Totality: total
Visibility: public export

any : AnHDec l => (xs : LazyList a) -> ((x : a) -> l (p x)) -> HDec (Any p xs)

  Half deciders are closed under the lazy list quantifier any

Totality: total
Visibility: public export