5 ms·

Didn't go through it all yet, but its premise seems kind of off: you can't really discuss "types in isolation of the language"! Just a basic example of two dyn

• klmr 9y ago
  > In Python I can get a lot done and really don't miss types at all No wonder, because Python has types (well … most everything does; but Python isn’t unityped [1]). It’s even relatively strongly typed. It’s just not statically typed (what the video calls “typed”). That said, I do miss static type checking in Python, and a lot of the tooling and methodology around Python (pylint, TDD…) are a direct consequence of that lack of static checking. — You seem to be aware of this but the distinction between “has types” and “has static typing” is actually fairly important. APIs in general often take advantage of Python’s extensible type system. [1] See e.g. https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/ https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...
  • kqr 9y ago
    The things in Python you call types are traditionally referred to as tags. Tagged values are values of one type (the type in Python) but which can still be distinguished based on a run-time check of their tag.
    • Retra 9y ago
      They are types and they are traditionally called types. Tags are an implementation detail.
      • kazinator 9y ago
        Moreover, a tag is an implementation detail which rarely represents everything about a type. E.g. a tag might tell us that some object is a function. But to know how many arguments it has, whether some are optional, and so on, we have to inspect fields beyond the tag.
      • willtim 9y ago
        Python only has one type. To quote from the article by professor Harper: "And this is precisely what is wrong with dynamically typed languages: rather than affording the freedom to ignore types, they instead impose the bondage of restricting attention to a single type! Every single value has to be a value of that type, you have no choice! Even if in a particular situation we are absolutely certain that a particular value is, say, an integer, we have no choice but to regard it as a value of the “one true type” that is classified, not typed, as an integer."
      • clhodapp 9y ago
        Python programmers call them "types" but type system people don't.
  • franey 9y ago
    Python has optional static typing since at least 3.6[1]. apistar[2], a REST framework, uses modern Python's typing to serialize data, which is neat. [1] https://docs.python.org/3/whatsnew/3.6.html#pep-526-syntax-for-variable-annotations https://docs.python.org/3/whatsnew/3.6.html#pep-526-syntax-f... [2] https://github.com/encode/apistar https://github.com/encode/apistar
  • hyperpape 9y ago
    Robert Harper is saying the exact opposite of what you’re quoting him to say. He would 100% call Python unityped (at least prior to the new type annotations, and probably even with them).
    • klmr 9y ago
      Yes, thanks for correcting me. I completely misremembered the article.
  • hnzix 9y ago
    > TDD…) are a direct consequence of that lack of static checking. Static checking gives you basic unit testing. TDD is far more expansive than unit testing. Static checking is not going to integration test your app for you.
    • carlmr 9y ago
      Yeah, but you can use a lot fewer tests for the same test coverage.
  • willtim 9y ago
    Read the article again. He says Python is unityped. The word "type" in mathematics and computer science has a meaning which is not the same as your usage of the word. Well-typed programs should not go wrong. Python programs can crash at runtime due to simple type errors (expected integer but got a string). A crash is a crash, from a theoretical point of view it matters not that the error is prettier than a segmentation fault. Python is not strongly typed, it just has good error messages.
    • klmr 9y ago
      Blah you’re right. That’s quite a serious oversight on my part, it’s been too long since I’ve read that article and I had apparently forgotten its core idea.
• skohan 9y ago
  I don't know, I have not written a ton of Python, but after spending a significant amount of time with Rust and Swift, which give you adequate tools to provably eliminate an overwhelming majority of runtime exceptions, I never want to go back.
  • simplify 9y ago
    I feel the same with ReasonML / OCaml. I've spent hours on a refactor and everything work beautifully after fixing all the type errors.
• flavio81 9y ago
  My experience is the same with Common Lisp: it is very strongly typed, so type mismatches never pass without an explicit error.
• seanwilson 9y ago
  > And static typing is great, as long as it doesn't require you to type variables and anonymous or small utility functions/methods... eg. it sucks without inference! > Some languages work better with types, some don't gain much from them... When you have proper type inference (which has been around for literally decades), what advantages do dynamic languages really have? I don't see any significant benefits personally. If you you're having trouble justifying at compile type a property holds, more than likely you've got a bug that's going to bite you later.
  • yorwba 9y ago
    When you're having trouble justifying at compile time that a property holds, it's not always because you don't know why it holds, but frequently a problem with the type system you have to write the justification in. Some type systems are so limited that you can't even express the conditions under which the property holds, let alone prove them. Others are powerful enough to prove anything, but that makes type inference intractable, because the inferencer might have to prove arbitrary theorems. The advantage of dynamically typed languages is that you are not glued to one specific proof language and don't have to provide proofs for trivial properties, or one-off programs you only need to run once. There are some type systems that attempt to provide similar benefits, e.g. success typing puts the burden of proof on the compiler which will only reject a program if it can prove that the program is incorrect [1]. But as far as I know, that approach has not been included in any mainstream programming languages. [1] https://arxiv.org/abs/1502.01278 https://arxiv.org/abs/1502.01278
    • kazinator 9y ago
      > e.g. success typing puts the burden of proof on the compiler which will only reject a program if it can prove that the program is incorrect That describes any dynamic language that does type inference. Type is taken into account for diagnosis and better code, but not as an excuse for rejecting the program just because it isn't fully analyzed.
    • seanwilson 9y ago
      > When you're having trouble justifying at compile time that a property holds, it's not always because you don't know why it holds, but frequently a problem with the type system you have to write the justification in. Do you have any realistic concrete examples of this? I find this happens very rarely myself (maybe once every few thousand lines of code) and just involves adding a small amount of code along the lines of "throw 'Unexpected error' // this should never happen because ...". > The advantage of dynamically typed languages is that you are not glued to one specific proof language and don't have to provide proofs for trivial properties, or one-off programs you only need to run once. For me, type errors for where you've mixed up e.g. string, number or object variables or where you've forgotten to check if a variable is null/undefined before you use it are incredibly common compared to the rare times the type system gets in your way. You would have to (and most wouldn't) write many automated tests to catch all those potential errors if you weren't using a type system for similar robustness. Throwing all that away because of the rare case the type system obstructs you doesn't make any sense to me. I still think if you're regularly writing code that is hard to justify to a mainstream type checker you're more than likely doing something very wrong and writing code that is hard for others to understand. I'd love to see a realistic counterexample.
• mikelward 9y ago
  String versus list of string continues to be a rough edge in Python, both being iterable.
  • carlmr 9y ago
    Yep, that one caught me a few times.
  • erokar 9y ago
    > both being iterable Which is a great thing.
    • nnq 9y ago
      Yeah, but this is a place where consistency bites your ass (in the absence of types): when you're iterating over characters in a string you usually do something very very different then when you're iterating over a random list. It could be solved by having a `string.get_iterator()` method (or `string.iterator` `@property`) for when you want to iterate over chars of a string to make it obvious (in the usual pythonic style). But probably this would break too much backward compatibility and only catch a few very easy to track bugs anyway. Ironically, Javascript almost got this right with `string.charAt()`, but then it shoot itself in the foot by also adding `[]` operator access in its typical "let's add more ways to do it to be sure at least one of them is bound to be wrong in some context" style...
    • mikelward 9y ago
      Both being iterable is great. String iteration yielding individual characters as strings is debatable. A function or method having no way to specify that a parameter must be a list of string, then acting strangely when passed a single string is a problem that types can help with.
• carlmr 9y ago
  >And static typing is great, as long as it doesn't require you to type variables and anonymous or small utility functions/methods... eg. it sucks without inference! F# does this amazingly well. Rust and Scala to a certain degree.