See: Type inference with duck typing - does this work? Why is it not used?
And: General approach for proving decidability/undecidability
Hello, I wanted to ask a theoretical question about type system conversion. The proposition is to suggest or complete static typing for gradually typed languages (or dialects / transpilation targets), at least to some capacity. I'm unqualified on this so please correct me if I mistake or misread anything.
You can simulate dynamic typing, like implicit type inference at compilation. The first issue:
For complex types it has to mention every operation it ever performs on the input objects, you could end up with a type which contains thousands of constraints.
(question at the bottom)
Not sure how accurate the definition: a variable's type is mutable, itself behaving like a variable. A variable's type can change in runtime. The second issue:
Duck typing requires that type checking be deferred to runtime, and is implemented by means of dynamic typing or reflection.
Could this also creatively be yielded to compile time checking? With analysis could you generatively do some sort of mitosis on the (multimorphic) variables? Say myVar is at one time a string and another time it's an int, split it to myVar1 of type string and myVar2 of type int, inserted in the correct positions. Bringing up flow sensitivity: not very familiar with it, not sure if it's syntatic sugar, performs runtime / compiletime, or has implications for this matter.
Thirdly, a larger question for each of the above: Do these pose undecidable problems? If so, for each, could you programmatically detect undecidabilities? (proving or inferring individually without human assistance)