+++
title = "Represent external functions as non-deterministic"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b6"]
forwardlinks = ["3b6"]
zettelid = "3b6a"
+++

By representing external function as being non-deterministic, one can
better reason about the basic properties that the OCaml function gives,
such as not allowing the property proven in `cong` in ([\#3b6]).

To do this in the Coq type-system, one can represent return values as
the type of all predicates of the function type. The return value of
non-deterministic computations which may return a value `A` can be
represented as $\mathcal{P}(A)$, which represents `A -> Prop`, all the
predicates of `A`.

This *may-return* monad is encoded in the [Impure Library].

  [\#3b6]: /zettel/3b6
  [Impure Library]: https://github.com/boulme/Impure