Data.Recursion.Free

(source)

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.

Definitions

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

  Syntax for a program using general recursion

Totality: total
Visibility: public export
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.

Hints:

Applicative (General a b)
Functor (General a b)
Monad (General a b)

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

  Type of functions using general recursion

Totality: total
Visibility: public export

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

  Recursor for General

Totality: total
Visibility: public export

call : PiG a b

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

Totality: total
Visibility: public export

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
Visibility: public export

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
Visibility: public export

already : General a b x -> Maybe x

  Check whether we are ready to return a value

Totality: total
Visibility: public export

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
Visibility: public export

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

  Recursively call expand a set number of times.

Totality: total
Visibility: public export

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
Visibility: public export

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
Visibility: public export

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
Visibility: public export

Domain : PiG a b -> (i : a) -> Code b (b i)

  Compute, as a Dybjer-Setzer code for an inductive-recursive type, the domain
  of a function defined by general recursion.

Totality: total
Visibility: public export

evaluate : (f : PiG a b) -> (i : a) -> Mu (Domain f) i -> b i

  If a given input is in the domain of the function then we may evaluate
  it fully on that input and obtain a pure return value.

Totality: total
Visibility: public export

totally : (f : PiG a b) -> ((i : a) -> Mu (Domain f) i) -> (i : a) -> b i

  If every input value is in the domain then the function is total.

Totality: total
Visibility: public export

data Layer : PiG a b -> General a b (b i) -> Type

Totality: total
Visibility: public export
Constructors:

MkTell : (o : b i) -> Layer f (Tell o)

  A computation returning a value is trivially terminating

MkAsk : (j : a) -> (jprf : Domain f j) -> (k : (b j -> General a b (b i))) -> Layer f (k (evaluate f j jprf)) -> Layer f (Ask j k)

  Performing a call to the oracle is termnating if the input is in its
  domain and if the rest of the computation is also finite.

view : (d : General a b (b i)) -> (0 l : Layer f d) -> View l

  Function computing the view by pattern-matching on the computation and
  inverting the proof. Note that the proof is runtime irrelevant even though
  the resulting view is not: this is possible because the relevant constructor
  is uniquely determined by the shape of `d`.

Totality: total
Visibility: public export

totally : (f : PiG a b) -> (0 _ : ((i : a) -> Domain f i)) -> (i : a) -> b i

  If a function's domain is total then it is a pure function.

Totality: total
Visibility: public export

irrelevantDomain : (f : PiG a b) -> (i : a) -> (p : Domain f i) -> (q : Domain f i) -> p = q

  Domain is a singleton type

Totality: total
Visibility: export

evaluateLayerIrrelevance : (f : PiG a b) -> (d : General a b (b i)) -> (0 p : Layer f d) -> (0 q : Layer f d) -> evaluateLayer f d p = evaluateLayer f d q

  The result of `evaluateLayer` does not depend on the specific proof that
  `i` is in the domain of the layer of computation at hand.

Totality: total
Visibility: export

evaluateIrrelevance : (f : PiG a b) -> (i : a) -> (0 p : Domain f i) -> (0 q : Domain f i) -> evaluate f i p = evaluate f i q

  The result of `evaluate` does not depend on the specific proof that `i`
  is in the domain of the function at hand.

Totality: total
Visibility: export

totallyIrrelevance : (f : PiG a b) -> (0 p : ((i : a) -> Domain f i)) -> (0 q : ((i : a) -> Domain f i)) -> (i : a) -> totally f p i = totally f q i

  The result computed by a total function is independent from the proof
  that it is total.

Totality: total
Visibility: export