First: > whenever you introduce a new linguistic abstraction to your language, it may reside either on the statics level, on the dynamics level, or on the both

First: > whenever you introduce a new linguistic abstraction to your language, it may reside either on the statics level, on the dynamics level, or on the both levels. In the first two cases, where the abstraction is located only on one particular level, you introduce inconsistency to your language; in the latter case, you inevitably introduce the feature biformity (...) Then: > One possible solution I have seen is dependent types. With dependent types, we can parameterise types not only with other types but with values, too. In a dependently typed language Idris (...) Great article overall!