Warning: Some posts on this platform may contain adult material intended for mature audiences only. Viewer discretion is advised. By clicking ‘Continue’, you confirm that you are 18 years or older and consent to viewing explicit content.
Op here back from the dead. This is in fact not a stab at dynamically typed languages, or at least not only: statically typed languages such as Java also support this kind of construct. In fact, one could develop a technically type safe programming language where an instanceof construct has sound semantics.
What instanceof breaks is something called polymorphic parametricity, i.e. the fact that generic functions don’t know anything specific about the types they are generic over. This is the fundamental condition for what in the community is dubbed “theorems for free”, that is, naturality of generic functions between generic types.
Op here back from the dead. This is in fact not a stab at dynamically typed languages, or at least not only: statically typed languages such as Java also support this kind of construct. In fact, one could develop a technically type safe programming language where an
instanceof
construct has sound semantics.What
instanceof
breaks is something called polymorphic parametricity, i.e. the fact that generic functions don’t know anything specific about the types they are generic over. This is the fundamental condition for what in the community is dubbed “theorems for free”, that is, naturality of generic functions between generic types.