4 ms·
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
by JonChesterfield 4y ago
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.
- mjburgess 4y agoI 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