Maybe it's a good idea to add a concrete example (can't edit the reply anymore):
OCaml:
let x1 = fun y -> (y, y) in
let x2 = fun y -> x1 (x1 y) in
let x3 = fun y -> x2 (x2 y) in
let x4 = fun y -> x3 (x3 y) in
let x5 = fun y -> x4 (x4 y) in
let x6 = fun y -> x5 (x5 y) in
x6 (fun z -> z)
Yes, types are usually represented by a DAG with sharing. OCaml does so, for example, and I assume ghc does something similar.
So, while id id has type ('a -> 'a) -> ('a -> 'a), this is stored in memory by a pointer structure that amounts to let 'b = ('a -> 'a) in ('b -> 'b). The type of id id id would become let 'b = ('a -> 'a) in let 'c = ('b -> 'b) in ('c -> 'c). This grows linearly. If one were to write out the types without sharing then their size would grow exponentially.
There was a bug in ghci (the GHC REPL) for a while which made it take exponential time to print the type of `id id id id id id id id id`. It used the linear representation for type-checking, but the pretty-printer was not implemented so cleverly.
Apparently that's been fixed. I can't confirm because that's not something I ever check the type of.
It seems to me that id id id ... id always has type a -> a. If you're referring to the type of the first id in the sequence, then what you're saying makes sense.
The fact that x1 is \y -> (y, y) is superficial, though. Something like x1 = Just also increases exponentially, and makes clear that using a deduplicated DAG for representing type terms doesn't solve this.
Ah, you're right. If one goes to x_{i+1}, then there will be 2^i Maybes in the type. The number of Maybe-occurrences in the type doubles in each step and sharing won't help there.
Python does not perform static type checking, therefore this problem doesn't apply immediately. You can build a program that takes exponential time to execute, but that is probably not a relevation to you.
I don’t think that’s possible because I don’t think there’s any aspect of the runtime type checker that descends into complex type structures. It just checks if runtime type tags match when you invoke an operator, or that an attribute exists when you try to access it.
There may be some kind of linter that would choke on type inference, but I think you are correct. It is more a just in time type inference at runtime otherwise.
OCaml:
Haskell: If you can compile these, add x7. The effort increases exponentially as one adds x7, x8 and so on.