X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/c96460c21e54996496235f12effaf8fffbd6b9e8..38c607cc6b1d382018217f12459685b2ab0d4c22:/ralf/_drafts/typeclasses-exponential-blowup.md

diff --git a/ralf/_drafts/typeclasses-exponential-blowup.md b/ralf/_drafts/typeclasses-exponential-blowup.md
deleted file mode 100644
index ec6e6dd..0000000
--- a/ralf/_drafts/typeclasses-exponential-blowup.md
+++ /dev/null
@@ -1,13 +0,0 @@
----
-title: "Exponential blowup when using typeclasses with nested indices"
-categories: research coq
----
-
-When formalizing a proof in an interactive theorem prover like [Coq](https://coq.inria.fr/), one reoccuring issue is handling algebraic hierarchies.
-Such hierarchies are everywhere:  Some operations are associative, while others also commute; some types have an equivalence relation, while others also have a (pre-)order or maybe even a well-ordering; and so on.
-So the question arises:  What is the best way to actually encode these hierarchies in Coq?
-Coq offers two mechanism that are suited to solve this task: typeclasses and canonical structures.
-Both can be instrumented in different ways to obtain a (more or less) convenient-to-use algebraic hierarchy.
-A common approach using typeclasses is the ["unbundled" approach by Bas Spitters and Eelis van der Weegen](https://arxiv.org/abs/1102.1323).
-However, as [has been observed before](https://pastel.archives-ouvertes.fr/pastel-00649586), and as learned the hard way in the Coq formalization of the [original Iris paper](http://iris-project.org/pdfs/2015-popl-iris1-final.pdf), this approach quickly leads to terms that seem to be exponential in size.
-