1 files changed, 24 insertions, 0 deletions
diff --git a/content/zettel/3b6a.md b/content/zettel/3b6a.md
new file mode 100644
index 0000000..d9faa24
--- /dev/null
+++ b/content/zettel/3b6a.md
@@ -0,0 +1,24 @@
++++
+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