4 ms·

Tests are not the only way to ensure correctness (and they aren’t even the only thing you should use, even when they’re mandated by policy) – did you consider u

Tests are not the only way to ensure correctness (and they aren’t even the only thing you should use, even when they’re mandated by policy) – did you consider using strong types encoding exactly the assumptions you spot-check with tests?

klibertp 12y ago
> did you consider using strong types encoding exactly the assumptions you spot-check with tests? Good luck encoding this simple contract (in Racket) exactly in your type system: (define/contract (fun numbers) (-> (listof (and/c (integer-in 0 255) even?)) any) ;; do something with a list of even integers in a given range null) I hope you like your Zero and Succ n and are proficient with Agda or ATS or something like this.
- Shish2k 12y ago
  I have no idea what you just said. Given that we're talking about type checking in python, care to give an example of a weakness of type checking in python?
  - klibertp 12y ago
    We're even, because I don't know about what "weakness" you're talking and why the heck you're bringing Python into abstract discussion on static typing. Basically, my parent said that static typing can express many things that testing (which is not static, because it runs the code) can. This is true, but there are things you can't express in any of the commonly used[1] static type systems and I just gave an example of such thing. Other than this there's nothing wrong with static typing in general and I'd be happy if Python got some kind of (optional) static type system, maybe in the vein of Typed Clojure and Typed Racket or Erlang's Dialyzer. Still, static type systems are not silver bullets and have their drawbacks - and that's all I wanted to convey in my comment. Edit: [1] the type system feature which would let you encode the example contract I posted is called "dependent typing" and is available only in a very few languages.
- marcosdumay 12y ago
  Pycontracts does that. Racket is more powerful, but that is a bad example.
  - klibertp 12y ago
    This is an example of a thing you can't encode in (most) static type systems, not something that can't be done in Python! On the contrary, it is very much possible to do in Python thanks to its dynamicity... I really don't understand what's going on in this thread; I'm stating an obvious fact that you can't encode things like "is even" in a static type systems without dependent types and that this is a drawback of such systems and I get downvoted. I never complained about my downvotes before, but this time I seriously don't understand what's happening. Did I fail that miserably in an effort to explain my position, or is this position controversial? For the record, I replied to this: > [dynamic in nature] Tests are not the only way to ensure correctness (and they aren't even the only thing you should use, even when they’re mandated by policy) – did you consider using strong [static?] types encoding exactly the assumptions you spot-check with tests? With an example of dynamic test (a contract) which you'd have a problem expressing in any but the most advanced type systems. Did claudius mean strong, but dynamic typing and I misunderstood? But then there is no difference at all between ensuring something in unit tests and in a type system as they are both executed at runtime. I honestly have no idea and I really would like to know which part of what I wrote deserved downvotes to avoid writing such things in the future if for no other reason.
    - marcosdumay 12y ago
      There are some people around here that think a downvote is the appropriate answer to a post they disagree with, what's very unfortunate. Looks like I misunderstood you, that's why my reply does not make much sense. But it is possible to verify such kind of constraints statically if you accept a certain amount of false errors, what all static type systems generate, to varying degrees. Your example and the equivalent pycontract are static types that miss a static time verifier, not dynamic ones (pycontracts can only create static types AFAIK).

klibertp 12y ago

> did you consider using strong types encoding exactly the assumptions you spot-check with tests? Good luck encoding this simple contract (in Racket) exactly in your type system: (define/contract (fun numbers) (-> (listof (and/c (integer-in 0 255) even?)) any) ;; do something with a list of even integers in a given range null) I hope you like your Zero and Succ n and are proficient with Agda or ATS or something like this.

Shish2k 12y ago
I have no idea what you just said. Given that we're talking about type checking in python, care to give an example of a weakness of type checking in python?
- klibertp 12y ago
  We're even, because I don't know about what "weakness" you're talking and why the heck you're bringing Python into abstract discussion on static typing. Basically, my parent said that static typing can express many things that testing (which is not static, because it runs the code) can. This is true, but there are things you can't express in any of the commonly used[1] static type systems and I just gave an example of such thing. Other than this there's nothing wrong with static typing in general and I'd be happy if Python got some kind of (optional) static type system, maybe in the vein of Typed Clojure and Typed Racket or Erlang's Dialyzer. Still, static type systems are not silver bullets and have their drawbacks - and that's all I wanted to convey in my comment. Edit: [1] the type system feature which would let you encode the example contract I posted is called "dependent typing" and is available only in a very few languages.
marcosdumay 12y ago
Pycontracts does that. Racket is more powerful, but that is a bad example.
- klibertp 12y ago
  This is an example of a thing you can't encode in (most) static type systems, not something that can't be done in Python! On the contrary, it is very much possible to do in Python thanks to its dynamicity... I really don't understand what's going on in this thread; I'm stating an obvious fact that you can't encode things like "is even" in a static type systems without dependent types and that this is a drawback of such systems and I get downvoted. I never complained about my downvotes before, but this time I seriously don't understand what's happening. Did I fail that miserably in an effort to explain my position, or is this position controversial? For the record, I replied to this: > [dynamic in nature] Tests are not the only way to ensure correctness (and they aren't even the only thing you should use, even when they’re mandated by policy) – did you consider using strong [static?] types encoding exactly the assumptions you spot-check with tests? With an example of dynamic test (a contract) which you'd have a problem expressing in any but the most advanced type systems. Did claudius mean strong, but dynamic typing and I misunderstood? But then there is no difference at all between ensuring something in unit tests and in a type system as they are both executed at runtime. I honestly have no idea and I really would like to know which part of what I wrote deserved downvotes to avoid writing such things in the future if for no other reason.
  - marcosdumay 12y ago
    There are some people around here that think a downvote is the appropriate answer to a post they disagree with, what's very unfortunate. Looks like I misunderstood you, that's why my reply does not make much sense. But it is possible to verify such kind of constraints statically if you accept a certain amount of false errors, what all static type systems generate, to varying degrees. Your example and the equivalent pycontract are static types that miss a static time verifier, not dynamic ones (pycontracts can only create static types AFAIK).