3 ms·
Just make types functions which are executed at compile time: @type def Monoid(T: type): return {'+': type[T, T].to(T) } def add(left: Mon
by mjburgess 4y ago
Just make types functions which are executed at compile time:
@type
def Monoid(T: type):
return {'+': type[T, T].to(T) }
def add(left: Monoid(int), right: Monoid(int)): Monoid(int)
return left + right
...if it takes too long to compile, terminate and report an error.
As for this kind of dependence, that seems straightforward:
@type
def Dependent():
return {0: int, 1: str, "Hello": bool}
def rtn_dependent(x: Dependent().keys): Dependent().values
if x == 0:
return x
elif x == 1:
return "message"
else:
return x == "Hello"
- JonChesterfield 4y agoDo 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