4 ms·

So because the type system is far far far far less polymorphic than the underlying code, we're to monomorphize the code manually? Angry rant: maybe mypy (and i

So because the type system is far far far far less polymorphic than the underlying code, we're to monomorphize the code manually? Angry rant: maybe mypy (and its PEPs) can be designed well? Maybe tacking java on top of python was a terrible idea, and python is much better than this awful type system. cf. the syntactical catastrophe that is "protocols". Consider that to type `+` correctly, you're writing >dozen lines of python. This is mad, and the type system shouldnt have been designed by people this inexperienced with type systems.

deleted 4y ago
[deleted]
zeckalpha 4y ago
Wait until you use math in OCaML.
- Yoric 4y ago
  I quite enjoyed programming in OCaml.
  - zeckalpha 4y ago
    Same, but the math system is strongly typed and doesn't have what the parent is talking about. There's more than one way to type a math system.
JonChesterfield 4y ago
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.

deleted 4y ago

[deleted]

zeckalpha 4y ago

Wait until you use math in OCaML.

Yoric 4y ago
I quite enjoyed programming in OCaml.
- zeckalpha 4y ago
  Same, but the math system is strongly typed and doesn't have what the parent is talking about. There's more than one way to type a math system.

JonChesterfield 4y ago

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.