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)

  • 4
    It sounds like you may be after something like TypeScript's structural typing? - typescriptlang.org/docs/handbook/type-compatibility.html Dec 15, 2022 at 0:11
  • As a note, in duck typed languages a variable's type is generally immutable. The construct you're describing where symbols can be rebound, so 'var1 = 1; var1 = 'hello';' will work, is also found in static languages like Rust and C++ and is a quite different idea. Dec 19, 2022 at 22:50
  • ^I meant object where I said variable here, and my use of the word symbol is confusing XD but other than that the point stands, redefining things does not a dynamic language make (and if that was the only difference then yes you could make it static - see rust). Dec 19, 2022 at 22:59

5 Answers 5


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.

  • 1
    "is not in the bytes stored" - that's an interesting point, because the difference between int and char is in what they represent, and by implication, how they are properly used and manipulated. There is not, inherently, any difference in the structure of the storage of these two, in the way that the distinction between int and other numeric types typically consists of there being additional structure. (1/2)
    – Steve
    Dec 18, 2022 at 10:52
  • 2
    Pithily, shape is not type. A type system typically defines that certain shapes should be handled as indivisible units or scalars, but it also has a further (conflated) role as a naming scheme for what the data represents (not merely as a naming scheme for shapes). Hence, two types can share a shape. (2/2)
    – Steve
    Dec 18, 2022 at 10:52
  • 1
    All agreed --- except that in TypeScript a shape is a type, at least at runtime. foo: {field: string} and bar: {field: string} will be treated identically at runtime. Dec 19, 2022 at 13:20

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.


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.


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.

  • "Sounds like the halting problem" is part of my question, but also relevant subtler details I mentioned. I'm trying to understand the possible extent of coverage, in perhaps a generous hypothetical. Moreso than practicality or usefulness, as this is a theoretical question. There's a lot to say about mis/conceptions, but also there's interesting possibilities along with new research to consider for, not only safety. I received interesting comments from a type theory forum, I'll update this soon. For completion could you elaborate on those corner cases? Dec 15, 2022 at 12:30
  • 1
    Yes, I must admit I answered a bit quickly without really reading in depth - my fault :-( You already mentioned the case where due to the number of operations on an input object, you get a huge number of constraints. As long as you can find a concrete type that satisfies these constraints, all is well - unless by more detailed analysis you find that there exist more concrete types that each fulfill only some of the constraints, and which of these is used where depends on some information that isn't available statically. The type theory folks might indeed have some deeper insights here. Dec 15, 2022 at 13:26
  • 1
    A colleague of mine on the Hack language team refers to this problem as "crossing the uncanny valley of typing". On the left side of the valley there is no type discipline and programmers doing whatever they please. On the right side there is full, reliable static typing where you have clearly expressed guarantees of whatever type safety promise the compiler makes. In the middle you have the valley of adding the costs of typing without the benefits of safety. Getting a language across that valley is a tricky problem in design! Dec 16, 2022 at 17:09
  • 1
    @EricLippert, glad to see your return. Your appearance prompted me to check your blog which had been on long hiatus. Now Facebook is over, you can return to what's important: being one of the foremost public intellectuals in computer science!
    – Steve
    Dec 18, 2022 at 12:28
  • @Steve: That is very kind of you to say but I am far from that! I'm just a guy who likes programming languages. :) I am looking forward to doing more writing. Dec 19, 2022 at 0:01

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')
>>> eval('True or False')
>>> 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.

Not the answer you're looking for? Browse other questions tagged or ask your own question.