Converting Dynamic Typing To Static Programatically

Question

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)

Answer 1

Having worked extensively in both C++ and Typescript, one of the biggest issues with compile-time duck-typing is in the transition between "structural" types and "nominal" types; that is, types that are defined by their structure vs types that are defined by their names -- I/O is always inherently structurally, be it I/O that comes in over a network connection or from a file on disk. By that I mean, we determine what we can do with it by whether the data is "shaped" the right way. Conversely, the internal definitions of pieces of software (and human reasoning) tend to want to work in nominal types -- the difference between integer value 65 and ASCII value a is not in the bytes stored but rather in what name we give to the mapping between bytes and meaning.

Different languages handle this in different ways; IMO the right tradeoff tends to be that if we're mostly dealing with untrusted I/O (as in a network call, or files we didn't create ourselves) we should deal with the cognitive overhead of living with structural typing within the code (and therefore mostly deferring resolution of duck-typing to runtime), while when we are in control of the I/O it tends to be more feasible and valuable to enumerate all the possibilities at build-time, as you're asking about; this is closer to what C++ would want to do.

Answer 2

I worked on Hack, as @EricLippert mentions in an adjacent comment. It was designed to migrate dynamic PHP to a statically typed language.

In general, you can do some of this static analysis at compile time in most languages. It looks very similar to other static analysis to detect buffer overflows or parallelism misuse. If you see a variable assigned a string, then you know it is a string until another mutation happens (or it is passed to a function in true pass by reference languages) (or any reflection assignment happens).

This becomes more challenging when other (potentially dynamic) variables get involved, and it becomes more challenging with operations like + which can take multiple types and return multiple types.

It becomes more challenging with branching, where a variable might be string or int depending on which path it took. There are particular scenarios which are exponentially complex (eg. a loop around a switch statement).

And in practice, non-trivial programs are undecidable because the type information lies outside of the program. Anything coming from disk or network will just be dynamic in a dynamic language. Dynamic language libraries will be untyped. Consider interop using JSON. A dynamic language will just treat the value as an int or a float or a string or a structure or a collection of JSON elements. This sort of recursive sum type also is a huge pain in the ass for static typing.

tl;dr - you can do it, but it will only be complete for trivial programs.

Answer 3

As others have pointed out, this problem cannot be solved in general. However, there are some interesting attempts to solve it in practice.

One system I've studied is Microsoft's Dynamic Language Runtime (DLR). They took an approach similar to what you describe. For a function that sometimes takes an integer and sometimes takes a string, you can make a function that takes an integer and a function that takes a string. Associated with each function is a small second function which tests whether the static typing guarantees requried by the function are met.

It does this opportunistically, rather than trying to solve the problem in general. To avoid the halting problem, they can always fall back on the original dynamic operations by running it through the correct interpreter. In practice, the most time intensive operations are the ones where typing is easiest to infer, so this actually works out pretty well.

The opportunistic approach is key. Decidability is one of those frustrating problems where it is easy to prove something is decidable (by deciding it in finite time), but painfully difficult or impossible to prove something is undecidable. By only focusing on the low hanging fruit where the proof of decidability is easy, they avoid having to solve the larger undecidable problems.

Answer 4

Having worked with Smalltalk for a long time, which is a very dynamically typed language, and recently with Rust, which is pretty much at the other end of the spectrum, I would say from experience that accurately mapping duck typed programs into statically typed programs is hard, and in corner cases impossible (or equivalent to the halting problem). There have been several approaches to "improve" Smalltalk by adding static type handling, and none of them have really gained much traction probably because it was perceived that the added weight of maintaining type information didn't correspond to a significant advantage in type safety, which is one of the main arguments for having static typing. In a language such as Rust, I see where the type system allows one to walk closer to the edge of memory safety, as the types enable the compiler to accurately know that the operations that I wrote are actually safe. In dynamically typed systems, this is ensured by the runtime; out-of-bounds errors or dangling pointers are impossible in Smalltalk, unless you rely on C language libraries which are unsafe in Rust as well.

Answer 5

I think a few people have mentioned that this isn't always possible (beyond simple code). But I think a minimal example might help.

In python there is a function called 'eval' which takes a string which has a python expression in it, evaluates it, and returns the result.

>>> eval('1 + 2')
3
>>> eval('True or False')
True
>>> eval('"hello, " + "world!"')
"hello, world!"

The type signature of this function is impossible to describe, the return value doesn't depend on the type of the input (which is always string) it depends on the value in a non-trivial way. You'd need a full python interpreter to figure out the result.

'eval' isn't used much in normal python code, but lesser magics (like getattr, setattr, and some decorators) are used quite often, and wherever they are used, static analysis / type inference will break down.