Building Almost Dependent Types in Swift

> For now, let’s talk about the type we’re going to generate for a particular value in terms of a generating function, $$F(x)$$ where $$x$$ can vary over our input domain of valid values for our dependent type system.

"Generating function" normally refers to a certain kind of power series in mathematics. The usage here is completely non-standard. An appropriate term would be "type constructor", "type operator", or "type-level function".

> To state this mathematically the function must satisfy the following rule $$\forall x_{0},x_{1} \in X, F(x_{0}) \neq F(x_{1})$$.

The rule contradicts the "idempotency" requirement given earlier in the article. The correct rule is: $$\forall x_{0},x_{1} \in X, x_{0} \neq x_{1} \implies F(x_{0}) \neq F(x_{1})$$. Speaking of idempotency...

> The first property is that a given type must be idempotent based on $$x$$ - that is, the type generated for a given input must remain the same and compare as equal regardless of how many times we call the generating function. Another way to state this is that we have to guarantee that $$F(x)$$ is a pure function, that is, it causes no observable side effects, and relies on no external state.

This is a super weird usage of the word "idempotent". Idemptency would mean $$\forall x. F(F(x)) = F(x)$$. Here, the author actually means $$\forall x, y. x = y \implies F(x) = F(y)$$, which is a totally different statement.

It's just really hard to get past these weird usages of terms. It feels like the author is just trying to sound smarter by (mis)using terms and concepts that are not familiar to him/her. Also, this article really misses the benefit of true dependent types, which is that you can encode mathematical propositions in them (where values of those types are proofs of the proposition).

I really appreciate the author's attempt to tackle this challenging material, but I think the presentation was poor.