Building Almost Dependent Types in Swift(sectionfive.net)
sectionfive.net
Building Almost Dependent Types in Swift
https://sectionfive.net/blog/2015/08/11/building-almost-dependent-types-in-swift/
1 comments
Thanks for the feedback - all totally valid points - I'll make some corrections based on this and credit you in article. Sorry if it came off as though I was trying to sound smarter, I wasn't, I just misused the terms in question and didn't catch it in my copy editing.
As noted in the last paragraph, this is very much ignoring a lot of the core reasons that dependent type systems are actually valuable in favor of explaining how you can get something _of the same flavor_ of dependent ML using Swift (though admittedly, it is still not _really_ dependent) - I'll be doing another one on type systems that goes into more on this topic (also very relevant name, nice).
Edit: Changes made - thanks again :D
As noted in the last paragraph, this is very much ignoring a lot of the core reasons that dependent type systems are actually valuable in favor of explaining how you can get something _of the same flavor_ of dependent ML using Swift (though admittedly, it is still not _really_ dependent) - I'll be doing another one on type systems that goes into more on this topic (also very relevant name, nice).
Edit: Changes made - thanks again :D
> 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.