Data.Recursion.Free

Module partially based on McBride's paper:
Turing-Completeness Totally Free

It gives us a type to describe computation using general recursion
and functions to run these computations for a while or to completion
if we are able to prove them total.

The content of the Erased section is new. Instead of producing the
domain/evaluation pair by computing a Dybjer-Setzer code we build a
specialised structure that allows us to make the domain proof runtime
irrelevant.

data General : (a : Type) -> (a -> Type) -> Type -> Type

  Syntax for a program using general recursion

Totality: total
Constructors:

Tell : x -> General a b x

  We can return a value without performing any recursive call.

Ask : (i : a) -> (b i -> General a b x) -> General a b x

  Or we can pick an input and ask an oracle to give us a return value
  for it. The second argument is a continuation explaining what we want
  to do with the returned value.

PiG : (a : Type) -> (a -> Type) -> Type

  Type of functions using general recursion

Totality: total

already : General a b x -> Maybe x

  Check whehther we are ready to return a value

Totality: total

bind : General a b x -> (x -> General a b y) -> General a b y

  Monadic bind (defined outside of the interface to be able to use it for
  map and (<*>)).

Totality: total

call : PiG a b

  Perform a recursive call and return the value provided by the oracle.

Totality: total

engine : PiG a b -> Nat -> General a b x -> General a b x

  Recursively call expand a set number of times.

Totality: total

expand : PiG a b -> General a b x -> General a b x

  Use a function using general recursion to expand all of the oracle calls.

Totality: total

fold : (x -> y) -> ((i : a) -> (b i -> y) -> y) -> General a b x -> y

  Recursor for General

Totality: total

late : PiG a b -> General a b x -> Late x

  Rely on an oracle using general recursion to convert a function using
  general recursion into a process returning a value in the (distant) future.

Totality: total

lazy : PiG a b -> (i : a) -> Late (b i)

  Interpret a function using general recursion as a process returning
  a value in the (distant) future.

Totality: total

monadMorphism : Monad m => ((i : a) -> m (b i)) -> General a b x -> m x

  Given a monadic oracle we can give a monad morphism interpreting a
  function using general recursion as a monadic process.

Totality: total

petrol : PiG a b -> Nat -> (i : a) -> Maybe (b i)

  Check whether recursively calling expand a set number of times is enough
  to produce a value.

Totality: total