4 ms·

Python always had a type system. It's not checked ahead of time but it's there. You can do things like return different types based on values read from a text

Python always had a type system. It's not checked ahead of time but it's there. You can do things like return different types based on values read from a text file at runtime, that is it's a dependent type system. Python is not a total language - no termination proof of given functions to be found. It's also not pure, the calculation that picked a type can pick a different one next time it runs on the same arguments. A dependent type system in a pure language with no user provided termination proof is in the ballpark of academia hasn't made it work yet. Python's dynamic type system _cannot_ be checked at compile time, however much care goes into the design. What can be done is cripple python to some subset that can be statically typed, combining the elegance of java with the performance of python, with some end goal that doesn't make any sense to me.

zeckalpha 4y ago
This definition of dependent type system is a bit controversial. There was a conflict between Julia language maintainers and FP researchers a few years back.
- JonChesterfield 4y ago
  Well, sort of. There's the (dominant?) school of thought that believes that types encode a program that runs before your actual program runs (and may thus be deleted at some point). This is often characterized by writing the type in a more awkward language than the usual one, C++'s separate languages for example. Dependent Type Theory is quite strongly associated with the compiletime/runtime phase separation assumption, where the weirdness is that values from the runtime world leak into the compiletime one. This is magic in the static/AoT type world and trivial in the dynamic/JIT one. So, strictly you're right, python is not dependently typed, as that term is owned by a different branch. However if you were to put an ahead of time type system on arbitrary python, that would need to be dependently typed to be able to describe the programs people write in python today. It would also be prone to failing to terminate during type checking.
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 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 ago
    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

zeckalpha 4y ago

This definition of dependent type system is a bit controversial. There was a conflict between Julia language maintainers and FP researchers a few years back.

JonChesterfield 4y ago
Well, sort of. There's the (dominant?) school of thought that believes that types encode a program that runs before your actual program runs (and may thus be deleted at some point). This is often characterized by writing the type in a more awkward language than the usual one, C++'s separate languages for example. Dependent Type Theory is quite strongly associated with the compiletime/runtime phase separation assumption, where the weirdness is that values from the runtime world leak into the compiletime one. This is magic in the static/AoT type world and trivial in the dynamic/JIT one. So, strictly you're right, python is not dependently typed, as that term is owned by a different branch. However if you were to put an ahead of time type system on arbitrary python, that would need to be dependently typed to be able to describe the programs people write in python today. It would also be prone to failing to terminate during type checking.

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 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 ago
  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