Do you know of a type checking algorithm which is likely to deal with something like the second case? I'd say it would need to decompose the function body into cases and typecheck them individually - I think typed racket called the pattern occurance typing.
Push it a little harder though and you're into the domain of automatic theorem provers. Which is indeed an answer to how to write a dynamically typed program that doesn't need manual proof annotation - a great trick to have, but not one that exists yet as far as I know.
For what it's worth I quite like abort and apologize for a type check that takes too long. The termination requirement is probably flexible in practice.
I dont, but as far as practical compilation for python goes, i'm fairly happy with a type system that panics -- we dont need proofs, we need to model the underlying lang in a way 95% close to its actual semantics
For me, above, we can observe that all functions either return or implicitly return None. Therein lies a straightforward alg: are the types of all the returns consistent with the keys of the specified dict? etc. etc.
You may, for sure, need to run compile-time user-supplied fns to augemtn the type system. That's fine.
You can even, if needed, call run-time fns with generic args -- in order to determine their type.
"static" analysis need not presume the absense of a runtime.. only not a particular state of the runtime
Push it a little harder though and you're into the domain of automatic theorem provers. Which is indeed an answer to how to write a dynamically typed program that doesn't need manual proof annotation - a great trick to have, but not one that exists yet as far as I know.
For what it's worth I quite like abort and apologize for a type check that takes too long. The termination requirement is probably flexible in practice.