What the article describes is a simple consequence of the Curry-Howard equivalence, that function types correspond to logical implication, and constructors are just a special case of function types.
back
2 comments
I wouldn't say it's a "simple consequence" or "just" this-or-that. Yes, Curry-Howard gives us a logical perspective on our code; but there are still better and worse ways to represent things from a logical perspective.
For example, we could reframe the author's point from the logic side, and complain that lots of mathematics suffers from defining things as sets-with-contraints, when it may be simpler to follow a more algebraic approach.
Actually, my aim was to give a broader perspective and draw attention to the fact that the inference rules as presented in the article are not limited to constructors, but can apply to any function. Thinking in those terms, you want to give functions a return type that matches the guarantees you want the function to give the caller (and argument types that match the guarantees the caller should give to the function). Furthermore, it means that using types in terms of a deductive system is not restricted to languages with ML/Haskell-like data constructors, but generally useful in any statically-typed language that supports user-defined types.
Yes, and the author knows that, but most programmers don’t. Hence, the article is valuable as introductory and educational material.