Abusing the algebra of algebraic data types even further - why does this work?
<p>So I have been reading, how you can convert ADTs into what resembles Real numbers and manipulating them, on pages like <a href="https://stackoverflow.com/questions/9190352/">this SO question</a> and <a href="http://chris-taylor.github.io/blog/2013/02/10/the-algebra-of-algebraic-data-types/" rel="nofollow noreferrer">this 3 part series</a> and <a href="https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types" rel="nofollow noreferrer">especially this</a>.</p>

<p>The "Trouble" section of the last link caught my eyes and I tried to solve for <code>Nat</code> in it even though the article states it's impossible.</p>

<pre><code>Nat = 1 + Nat
Nat - Nat = 1
Nat(1 - 1) = 1
Nat = 1 / (1 - 1)
</code></pre>

<p>This might seem like total nonsense since I just divided by 0 (and you might be right), but if you read any of those links or something similar, then you'll notice that it looks very similar to a definition of a list.</p>

<pre><code>List(x) = 1 / (1 - x)
</code></pre>

<p>So you could write Nat like <code>Nat = List(1) = 1 + 1 + 1 + ...</code>, which is exactly what you would get by repeated substitution in the starting equation. This is also equivalent to defining Natural numbers like this in Haskell:</p>

<pre><code>type Nat = [()]
</code></pre>

<p>Which is definitely a valid encoding of Natural numbers, where <code>0 = []</code> and <code>S(N) = () : N</code>.</p>

<hr>

<p>So my question is how come did I get a valid result out of this? I just divided by zero. Not to mention the starting equation itself is pretty much a contradiction.</p>

<p>So how come I got something that makes sense at the end of this? Is this just pure coincidence or is the division by 0 somehow defined in this context that makes sense?</p>