Executing Computations

This file defines a function runIO for executing a computation via the IO monad.

The semantics mirror evalDist in that the oracle will respond uniformly at random, however we need to limit the oracle set to unifSpec to get computability of the function. In particular we can't choose randomly from arbitrary types. Usually it's possible to reduce to this anyway using SelectableType instances (see unifOracle).

NOTE: OracleComp.failure could instead be an error to allow error msg propogation.

def OracleComp.runIO {α : Type} (oa : ProbComp α) : IO α

Represent an OracleComp via the IO monad, allowing actual execution. NOTE: OracleComp as currently defined doesn't allow specialized error messaging. Changing this would just require adding a String to the failure constructor

Equations

• One or more equations did not get rendered due to their size.

instance OracleComp.instMonadLiftProbCompIO : MonadLift ProbComp IO

Automatic lifting of probabalistic computations into IO.

Equations

• OracleComp.instMonadLiftProbCompIO = { monadLift := fun {α : Type} => OracleComp.runIO }