11 ms·

Why Type Systems Matter

79 points by somecoder 9y ago

rocky1138 9y ago
Strong typing is great when I've already made sense of how the logic should flow and I'm ready to solidify my work into something stable and extensible over time. It's not so great when I'm trying something new and am still trying to work out if what I want to do is even possible, since I find myself trying to identify the right type to use in a given situation rather than proving that I'm even able to do it. A lot of my daily work is prototyping.
- willtim 9y ago
  There's no reason why static type errors can't be deferred until runtime, GHC Haskell can do this. Personally I find types invaluable when prototyping. I often fill in the implementations after I work out the types.
  - shalabhc 9y ago
    I wish this was adopted more broadly, e.g. by Rust and other newer languages.
    - oconnor663 9y ago
      What would the semantics of that be? Something like "this function contains a type error, so if you call it your code will just panic?"
      - AnimalMuppet 9y ago
        At it's simplest, I could see it being a compiler flag. No annotations needed. Default would be strict compile-time typing. But with a flag, you could turn type errors into warnings (and runtime panics), or even into not-even-warnings, just silence (and runtime panics).
      - willtim 9y ago
        Haskell can defer them by producing thunks (values) containing runtime exceptions. But unlike a dynamic-only language, you still get to know about the errors at compile time, by way of a set of warnings.
      - zbobet2012 9y ago
        Look at Idris to see how this kind of thing works. https://jeremywsherman.com/blog/2015/10/10/idris-metaprogramming-hello-world/ https://jeremywsherman.com/blog/2015/10/10/idris-metaprogram...
      - ziotom78 9y ago
        If I understand well, Ada packages provide the necessary architecture for this kind of stuff. A package is like a Python "module", but it is typically split in two files: a specification, just containing the declaration of all the types and functions exported by the package, and a body, which actually implements the functions working on those types. When writing a program which uses that package, if you only compile it without linking, the compiler will complain about wrong types even if no function has been implemented yet. A poor man's version of the above schema can be achieved in C/C++ as well. Just declare your functions in a header file and include it in your program, then compile without linking.
        willtim 9y ago
        This is not the same thing as deferred type errors though. The programs are still type correct, it's just that some of the implementations are missing / producing errors.
    - Others 9y ago
      If I'm understanding what you want correctly, Rust kinda will get that once the `!` type is stable/used in type inference correctly.
  - gertef 9y ago
    > I often fill in the implementations after I work out the types. OK, but that's the opposite of deffering type errors until runtime. Using "undefined"/bottom as the implemenation of a function is how we wrote Haskell before GHC added support for deferring type-errors.
    - ORioN63 9y ago
      Oops. I still use undefined everywhere, while my code isn't complete. Also, typed holes. Typed holes are awesome for building implementations based on types.
    - willtim 9y ago
      Yes I don't use deferred type errors much. But the parent poster wanted the option to avoid worrying about type correct programs.
- shalabhc 9y ago
  > Strong typing I think you mean 'static' typing, not strong? Python is already strongly typed. > It's not so great when I'm trying something new and am still trying to work out if what I want to do is even possible I completely agree here. I find it very useful when iterating to run the program and verify just the code path that gets executed, without worrying about whether the rest of the program is also correctly typed. Once I have settled on a set of types though, it would be nice if Python told me all the places that now need to be fixed up.
  - msla 9y ago
    The conflation between 'strong' and 'static', and 'weak' and 'dynamic', is probably terminal at this point, but maybe I can do something to, at least, explain the position of the people who don't conflate those terms: Strong typing is about creating, expressing, and enforcing a contract which determines which operations are valid on which values. Not variables, values. Having the semantics of the value in the compiler or the runtime ensures that errors are handled predictably, with explicit detection and possible reporting. Weak typing is a lack of those semantics. In the most extreme case, you have languages such as B, where the only type is the machine word, which isn't a type at all because it doesn't imply anything about semantics: You can do anything to a machine word, so nothing can possibly be invalid, so there's nothing to enforce or detect or report. Similar "size specifications", such as int, or long, or float, are only loosely describable as types for the same reason: They specify how many bits a value has, not what's valid to do to it. So a language such as Python is strongly typed because it can detect violations of the contract inherent in the types it knows about at runtime. C is less strongly typed, because, first, it focuses on its "size specification" types, and, second, you can subvert even that type system totally with nary a peep. Languages such as Ada, which inherited the "size specification" types from Algol, are only strongly typed to the extent you can augment their type system with types which are actually semantic, as opposed to size-based.
    - thanatropism 9y ago
      Honest question: Is Python-with-type-hinting-in-function-definitions (and maybe type assertions) equally as "strong" as common style Python? It's not static typing -- it's not Haskell -- but it's already a step further. Edit: I find myself doing a lot of "assert isinstance(x,foo)".
- seanwilson 9y ago
  Can you give an example? I don't find this personally. I find static strong typing speeds me up because I don't have to restart the app, click some buttons etc. to figure out some code was wrong. This is true even for prototypes. Most of the time any type declarations you need are straightforward and once you know your code better you can start introducing more exotic types to capture more errors later.
  - rocky1138 9y ago
    A really basic example would be the "as GameObject" part of this statement in C#: `GameObject gameObject = GameObject.Instantiate(MyGameObject, Vector3.zero, Quaternion.Identity) as GameObject;". It's annoying to have to type "as GameObject" when very clearly I am creating a GameObject type (the first thing in the entire statement). Programming languages should be smart enough to figure out that's what I'm trying to do rather than require me to type that out.
    - argv_empty 9y ago
      Like GP, I often wonder what untyped languages offer over typed languages for prototyping, and this "soooo much annotation!" thing just isn't a satisfying answer anymore. "Typed" does not mean "as verbose as C#/Java."
    - dozzie 9y ago
      First, this annoyance does not come from static typing, it comes from C#'s type system. There are statically typed languages where you just construct the value and assign it to a variable, and compiler infers variable's type for you (e.g. OCaml). Then, typing the class name is a trivial matter. My editor offers me a generic text completion command, so I don't type full "GameObject", I just type "Ga" and hit ^P. Maybe you should try using a good text editor?
    - sqeaky 9y ago
      Have an upvote for being perfectly reasonable and attempting to provide examples and reason, even if I disagree with them. Rather than deflect away from C#, I will take the unpopular stance of defending verbosity. Does typing that really represent a large waste of time? Do you spend more time physically typing than doing anything else while coding? I spend most my time thinking or reading old code. I might type that once and read it 100 times and pass the debugger over it 6 or 7 times and adjust the line a similar amount in the lifespan of that of the code. For reading it is entirely clear and leaves little ambiguity about what kinds of operations are allowed on GameObject (presuming I know something about the GameObject class and the Entity Component System in place). I know its location and its rotation and I know that those are unlikely to be the source of bugs. I might need to reference `MyGameObject` to get the specifics of the behavior, but if I am troubleshooting location or rotation errors, I know what code I am not looking at. If I am troubleshooting any other behavior I again know about whole regions of code I don't need to look at. It can be hard to internalize all that a type system buys for you because none of it is immediate, it is more about all the time you don't spend doing unproductive things. I find that in more dynamically typed languages I spend two the three times as much time debugging than in static languages.
- naasking 9y ago
  > It's not so great when I'm trying something new and am still trying to work out if what I want to do is even possible, since I find myself trying to identify the right type to use in a given situation rather than proving that I'm even able to do it. Finding the right type is solving most of the problem. If you can find the right type, you can solve the problem. If you're having trouble finding the right type, then you don't yet understand the problem well enough, and modelling what you do know with types quickly points out what parts of the problem you haven't fully understood, without having to run broken, half-specified programs that cover only part of the problem space. What makes you think being able to run such half-specified programs for part of the problem will actually help with answering this question?
  - Veedrac 9y ago
    > If you can find the right type, you can solve the problem. Do you actually believe this?
    - jerf 9y ago
      What's the most advanced type system you've used? It's quite difficult to explain how much work a very strong type system can do for you if you're used to something like C as your definition of "static typing". I mean this comment comment completely straight and polite, and I'm trying to help people answer your very reasonable question by asking you for some details that will help calibrate the answer.
      - Veedrac 9y ago
        Technically that would be something like Haskell's, but I only have surface-level fluency. More to the point would be the most complex stuff I've had reason to do with a type system, which caps at around this generic state machine: https://play.rust-lang.org/?gist=3fdb20c34d589a2576c6bb137b9fd359&version=stable&backtrace=0 https://play.rust-lang.org/?gist=3fdb20c34d589a2576c6bb137b9... (TL;DR: A type that encodes a state machine (and is generic over the implementation) that allows you to guarantee reaching a terminating state.) In practice I rather my types looking much plainer, though: https://github.com/llogiq/bytecount/blob/master/src/lib.rs https://github.com/llogiq/bytecount/blob/master/src/lib.rs
- mixedCase 9y ago
  With a good type system, instead of writing algorithms first you would write data structures that convey the ideas behind the software's intent clearly. Then you start writing the algorithms that manipulate these data structures. If what you're trying to do is viable, then you'll be able to express it in the domain model.
  - sk5t 9y ago
    Yes! I've found it quite effective to start new problems with some (mostly composition-based) types as a means of jotting down the core inputs and outputs, then work out towards the edges in both directions with deserializers/readers/parsers in one direction, and repositories and work-doing algorithms in the other direction. A little dependency injection to wire the pieces together in complex systems and you're in business.
  - jmull 9y ago
    I usually start design with a domain model, whatever the type system I'll be working with. (Just pointing out you can go this route regardless of your type system.)
- marcosdumay 9y ago
  Personally, I did never feel that way. Either types come out mechanically and just mean some more typing slowing me down because they don't say anything interesting, or creating the types is exactly "proving that I'm even able to do it". I tried, but I can't recall any single time when thinking about types distracted me from thinking about the problem. Moreover, writing down the types by creating stub functions is a great method of designing.
- JamesBarney 9y ago
  When I'm still prototyping I usually pick the part of the project I am the most uncertain about, then write a big function with lots of anonymous types. Once I feel more familiar with it I refactor into types. But types can also be really useful when you are in the process of learning your domain. If I'm using javascript and I realize I could better represent my code if I did some refactorings I usually don't touch it because I fear breaking something. On the other hand if I'm using a statically typed language I feel free to refactor to my hearts content with the knowledge that the chance I break something is far smaller.
rdtsc 9y ago
Good post, but note all those things you don't need a statically typed language. Erlang for example is a dynamically typed language but it has Dialyzer - a type checker. The more precisely you define the types the more discrepancies and issues it will find in the code, exactly the kind of stuff the author mentions. http://learnyousomeerlang.com/dialyzer http://learnyousomeerlang.com/dialyzer That's technically called "success typing" http://www.it.uu.se/research/group/hipe/papers/succ_types.pdf http://www.it.uu.se/research/group/hipe/papers/succ_types.pd... Python has that too with MyPy. That came much later than Erlang and I haven't used yet so not sure how well it works http://mypy-lang.org/ http://mypy-lang.org/ They seemed to have copied success typing but don't actually mention it anywhere.
- napsterbr 9y ago
  Erlang with dialyzer is a great "mix", it allows you to move as quickly you would with a dynamic language and, as long as you define the type specs, have a reassuring type safety. Of course it's nowhere near haskell's or elms type safety because, as you said, dialyzer follows the success typing model, sort of like an optimistic one ("you are correct until I prove you otherwise"), and haskell and elm follow the opposite way ("you are wrong until you prove me otherwise "). It's a tradeoff, as everything else in computer science, and one that has worked for us. Can't recommend both erlang and dialyzer enough :)
  - zsd 9y ago
    Success typing really seems both ideal for me and the only sane way to do optional, progressive typing. I wonder if Ruby could do it? I think there are too many ways for an expression to be invoked from friggin anywhere in Ruby to make that possible.
  - dom0 9y ago
    The funny thing about "moving quickly in dynamic languages" is that it doesn't last. Refactoring code in a dynamic language gets difficult fast and is an entirely hopeless endeavour without a huge test suite (you obviously need tests on every level, because you can't refactor an interface and its test at the same time and still think it's working as intended). Typed code may be slower and more cumbersome (to some) to write in the first place, but is usually much easier to maintain in my experience.
AnimalMuppet 9y ago
A line from a novel by Georgette Heyer: "I look for trouble. I don't wait to have it brought to my attention." That is, if there's a type problem, I want to know at compile time, not at run time. But I'm in embedded systems. My stuff looks like just a machine to the customer. They don't want a type error at runtime messing them up. That may not be your world. If you'd rather things go happily along until the circumstances actually occur in execution, and if that ever happens, you then find out about the type problem, well, that's what is reasonable to you in your environment and circumstances, and that's fine. Use dynamic typing, and don't feel guilty.
gumby 9y ago
Some languages mix static and dynamic typing. For example MACLISP used this to great effect to make MACSYMA super fast. All the numeric code was statically typed and the compiler built code that was as fast as hand crafted assembly. Yet you could write conventional Lisp code that called this static code just like any other code. MACLISP derivatives like lisp machine lisp also implemented this stuff and used it for system code. I used it heavily. All that survived into Common Lisp but I am not up on the current state of lisp implementations and have no idea if people bother to take advantage of it any more.
- shakna 9y ago
  C++ is in this boat now. Most of the time I'd recommend the new type-safe union std::variant, but std::any is there. It is kinda a static type, but as a container-type of anything in the type system, it may as well be a dynamic type. --- > All that survived into Common Lisp but I am not up on the current state of lisp implementations and have no idea if people bother to take advantage of it any more. Typed Racket uses the early guard theories from CL [1], and it does have an optimiser [2], though it has some quirks. And though I can't find it now, there was a fairly recent research paper on using a macro system to static type check at compile-time and optimise for Scheme. But, I should point out that Scheme doesn't need it for optimisation - compiling Scheme to C is easy, and easy to make the result fast. Its more about safety. And there's always Shen which uses sequent calculus [3] for their optional static type system. [0] https://docs.racket-lang.org/ts-guide/ https://docs.racket-lang.org/ts-guide/ [1] http://www.cs.utexas.edu/users/boyer/ftp/diss/akers.pdf http://www.cs.utexas.edu/users/boyer/ftp/diss/akers.pdf [2] https://docs.racket-lang.org/ts-guide/optimization.html https://docs.racket-lang.org/ts-guide/optimization.html [3] http://shenlanguage.org/learn-shen/index.html#10%20Sequent%20Calculus http://shenlanguage.org/learn-shen/index.html#10%20Sequent%2...
  - gumby 9y ago
    > Most of the time I'd recommend the new type-safe union std::variant Neither g++ 7 nor Clang/LLVM 4.0.1 support std::variant yet :-(. We started a new (blank buffer) codebase earlier this year and decided to use C++17 as the implementation language, which has exposed us to the gaps...which are surprisingly few! But sadly this is one of them.
simplify 9y ago
If you haven't thought much about type systems but want to understand what the big deal is, I wrote a post specifically for you [1]. It draws motivation for wanting a good static type system from first principles. [1] http://gilbert.ghost.io/type-systems-for-beginners-an-introduction/ http://gilbert.ghost.io/type-systems-for-beginners-an-introd... (I posted this on a similar story and it was received very well, so I thought I might post it again for those who haven't seen it.)
benhoyt 9y ago
Counterpoint I wrote a while back that focuses on compilation speed: http://benhoyt.com/writings/language-speed/ http://benhoyt.com/writings/language-speed/ I've used Scala a fair bit recently, and the compiler is so dog slow it's painful. Maybe it's just my relative fluency with Python, but I find I'm much more productive with Python's almost instant edit-compile-run sequence. Edit: I do like many of the benefits of static typing, though. I think mypy is coming into its own in the Python community, especially now with Guido behind it. Maybe this kind of optional typing is the best of both worlds...
- zem 9y ago
  that's one of the things go got right - they had fast compilation speed as a first-class goal right from the beginning.
  - jerf 9y ago
    They also have a really, really simple type system that can't play very many of the games that type system experts would like to play, so it doesn't cost them a lot of runtime at compile time. I'm sort of curious what the abstract minimum penalty is for the very advanced type systems. Are GHC (Haskell) and rustc already within, say, 5x of the optimal possible speed, or might we be able to have a very advanced type system and faster compiling? Time shall tell, I suppose.
- MrRadar 9y ago
  Check out D (https://dlang.org/ https://dlang.org/). It has a reasonably powerful static type system and the dmd compiler is lighting fast.
- mahyarm 9y ago
  I would prefer mandatory typing with a dev mode that makes it optional for speed. With optional typing, you end up with the third party ecosystem not having typing, which makes it hard to enforce type safety with a codebase that is fully type safe itself.
- willtim 9y ago
blauditore 9y ago
I thought this was quite clear, and it's what I've always been missing in languages like Python or JS. Yet I meet many devs, especially coming from such languages, making fun of Java for its verbosity and clumsiness. On the other hand, it leads to some people abusing the static type system: They just randomly change types until it somehow compiles, without thinking about what their doing.
- captainmuon 9y ago
  > They just randomly change types until it somehow compiles, without thinking about what their doing. I did that, too, when I was inexperienced with C++. Especially with const, but also with * and &. But somehow it "clicked" at one point and I don't have that problem anymore. In recent times, I've found static type systems to helpfully nudge me in the direction of correct code. I was pleasantly surprised by TypeScript. Also, in modern C++, if you use unique_ptr, shared_ptr, try to get rid of naked pointers, and use value types and RAII if possible, the code ends up a lot cleaner. I've found a couple of places where ownership was unclear, and I previously had circular references or dangling pointers as a result. And anecdotically, the way people program in Haskell is basically, write what you mean, and then fix it until it compiles; it will likely also be correct.
- mcphage 9y ago
  > making fun of Java for its verbosity and clumsiness Java has a particularly verbose and clumsy type system.
  - shock 9y ago
    What do you mean it has a verbose type system?
    - mcphage 9y ago
      Person myPerson = new Person("My", "Name") You need to specify the class twice on the same line, because Java can't figure it out on its own.
falcolas 9y ago
There is never a person more zealous (and vocal in their zealotry) than a new convert. You don't see the bad points, just the good. That's how this post comes across: "Types are so awesome, let me show you how awesome types are!" Come back in two years, show us how the types feel after the honeymoon is over.
- jamescostian 9y ago
  While I agree that type systems often get in the way, and that the author is only pointing out bad points and not good ones, aren't you doing the same? At least the author is trying to back up their claims (e.g. they provide an example where someone decided to put sizes in strings). The honeymoon part is also an unfair assumption, not to mention incorrect. I just clicked on "About me", clicked on the author's github link, and after some scrolling and clicks, I found a rust commit from August 2015 the author made - thus, the author has been here for 2 years, and is not some newbie. You should provide a list of cons involved with type systems that aren't so glaringly obvious that the author has probably already ran into them, and that will serve as a much stronger argument (e.g. you could bring up the fact that in large codebases with lots of generics, type systems drastically increase time spent typing, as well as cognitive overhead when there are <T>s and <T, E>s and so on all over the place).
  - falcolas 9y ago
    Because my comment was not about type systems, it was about the fervor and lack of usefulness of the post itself. Plus, I'd just be repeating myself and others much more eloquent than I - why do that? Plus, arguments about typed languages rank up there with vi vs Emacs (or is it now vi/emacs vs. Atom/VSC?) in terms of my interest in joining them. I like statically typed languages. I like dynamically typed languages. I dislike weakly typed languages. What more to add?
    - sqeaky 9y ago
      You may be entirely correct, but the way you have presented your position looks extremely unconvincing. What I can see: You chime in on a discussion with a strongly critical viewpoint, then refuse to back it up saying you don't want to be part of certain kinds of arguments. Implying religious level flamewars, while the rest of us are keeping a level head and discussing these things based on technical merit. It looks like you are making excuses because it looks like you have no point. Even if that wasn't what you intended and you have strong points, that isn't what it looks like from the outside. Please remember that not everyone has exactly your experience so if you have examples you should share them because they will make your points stronger even if someone attempts to rebut them. It also artificially weakens your point to try to back out with what from the outside look like excuses instead of substance. Again, I must say you might be entirely correct, I just can't see that from here.
mamcx 9y ago
My dream is a static-first (like with inmutable-first) language with a way to do dynamic. The thing is not available (as far I know) is to build a dynamic object and "close it" for further modification so the compiler can optimize well. Other, that requiere good metaprograming, is to build a dynamic object AT COMPILE TIME (macro?) and close it, then the type-system work after that (F# type provider is almost this) A use case is reflect a database/data storage like JSON or relational table. I wish, like with python, to do: class Customer = @build(table("Customer")) and after this line : c = Customer() print c.name to 'c' be a static type. If at compile time, it check the type, let say the field change to c.fullname, to mark as a type error. If in runtime, like a interpreter, to "close" Customer and be certain that it never will mutate. AKA: Inmutable types/clases, but the posibility to mutate it in some discret places. Make sense?
- h_r 9y ago
  This sounds similar to F# type providers.
- 62747478182 9y ago
  You may be interested in Crystal. https://crystal-lang.org/ https://crystal-lang.org/
dmux 9y ago
I'd be interested in hearing what the community has to say regarding static types and whether or not they're compatible with object-oriented programming. I've posted this link a couple times before, but it hasn't been actively discussed: https://essencesharp.wordpress.com/2014/07/17/static-typing-and-interoperability/ https://essencesharp.wordpress.com/2014/07/17/static-typing-... From that article: "Static typing inhibits interoperability. It does so between class libraries and their clients, and also between programming languages. The reason is simply because static typing violates encapsulation in general, and improperly propagates constraints that aren’t justifiable as architectural, design or implementation requirements in particular. It does so either by binding too early, or by binding (requiring) more than it should."
- evincarofautumn 9y ago
  Many OOP languages don’t make it easy to achieve encapsulation and composability in the presence of their particular static type systems. It sounds like he’s just arguing that nominal typing is worse than structural typing, and early binding is worse than late binding; the comparison to static type systems is a false equivalence.

79 points by somecoder 9y ago

Strong typing is great when I've already made sense of how the logic should flow and I'm ready to solidify my work into something stable and extensible over time. It's not so great when I'm trying something new and am still trying to work out if what I want to do is even possible, since I find myself trying to identify the right type to use in a given situation rather than proving that I'm even able to do it. A lot of my daily work is prototyping.

willtim 9y ago
There's no reason why static type errors can't be deferred until runtime, GHC Haskell can do this. Personally I find types invaluable when prototyping. I often fill in the implementations after I work out the types.
- shalabhc 9y ago
  I wish this was adopted more broadly, e.g. by Rust and other newer languages.
  - oconnor663 9y ago
    What would the semantics of that be? Something like "this function contains a type error, so if you call it your code will just panic?"
    - AnimalMuppet 9y ago
      At it's simplest, I could see it being a compiler flag. No annotations needed. Default would be strict compile-time typing. But with a flag, you could turn type errors into warnings (and runtime panics), or even into not-even-warnings, just silence (and runtime panics).
    - willtim 9y ago
      Haskell can defer them by producing thunks (values) containing runtime exceptions. But unlike a dynamic-only language, you still get to know about the errors at compile time, by way of a set of warnings.
    - zbobet2012 9y ago
      Look at Idris to see how this kind of thing works. https://jeremywsherman.com/blog/2015/10/10/idris-metaprogramming-hello-world/ https://jeremywsherman.com/blog/2015/10/10/idris-metaprogram...
    - ziotom78 9y ago
      If I understand well, Ada packages provide the necessary architecture for this kind of stuff. A package is like a Python "module", but it is typically split in two files: a specification, just containing the declaration of all the types and functions exported by the package, and a body, which actually implements the functions working on those types. When writing a program which uses that package, if you only compile it without linking, the compiler will complain about wrong types even if no function has been implemented yet. A poor man's version of the above schema can be achieved in C/C++ as well. Just declare your functions in a header file and include it in your program, then compile without linking.
      - willtim 9y ago
        This is not the same thing as deferred type errors though. The programs are still type correct, it's just that some of the implementations are missing / producing errors.
  - Others 9y ago
    If I'm understanding what you want correctly, Rust kinda will get that once the `!` type is stable/used in type inference correctly.
- gertef 9y ago
  > I often fill in the implementations after I work out the types. OK, but that's the opposite of deffering type errors until runtime. Using "undefined"/bottom as the implemenation of a function is how we wrote Haskell before GHC added support for deferring type-errors.
  - ORioN63 9y ago
    Oops. I still use undefined everywhere, while my code isn't complete. Also, typed holes. Typed holes are awesome for building implementations based on types.
  - willtim 9y ago
    Yes I don't use deferred type errors much. But the parent poster wanted the option to avoid worrying about type correct programs.
shalabhc 9y ago
> Strong typing I think you mean 'static' typing, not strong? Python is already strongly typed. > It's not so great when I'm trying something new and am still trying to work out if what I want to do is even possible I completely agree here. I find it very useful when iterating to run the program and verify just the code path that gets executed, without worrying about whether the rest of the program is also correctly typed. Once I have settled on a set of types though, it would be nice if Python told me all the places that now need to be fixed up.
- msla 9y ago
  The conflation between 'strong' and 'static', and 'weak' and 'dynamic', is probably terminal at this point, but maybe I can do something to, at least, explain the position of the people who don't conflate those terms: Strong typing is about creating, expressing, and enforcing a contract which determines which operations are valid on which values. Not variables, values. Having the semantics of the value in the compiler or the runtime ensures that errors are handled predictably, with explicit detection and possible reporting. Weak typing is a lack of those semantics. In the most extreme case, you have languages such as B, where the only type is the machine word, which isn't a type at all because it doesn't imply anything about semantics: You can do anything to a machine word, so nothing can possibly be invalid, so there's nothing to enforce or detect or report. Similar "size specifications", such as int, or long, or float, are only loosely describable as types for the same reason: They specify how many bits a value has, not what's valid to do to it. So a language such as Python is strongly typed because it can detect violations of the contract inherent in the types it knows about at runtime. C is less strongly typed, because, first, it focuses on its "size specification" types, and, second, you can subvert even that type system totally with nary a peep. Languages such as Ada, which inherited the "size specification" types from Algol, are only strongly typed to the extent you can augment their type system with types which are actually semantic, as opposed to size-based.
  - thanatropism 9y ago
    Honest question: Is Python-with-type-hinting-in-function-definitions (and maybe type assertions) equally as "strong" as common style Python? It's not static typing -- it's not Haskell -- but it's already a step further. Edit: I find myself doing a lot of "assert isinstance(x,foo)".
seanwilson 9y ago
Can you give an example? I don't find this personally. I find static strong typing speeds me up because I don't have to restart the app, click some buttons etc. to figure out some code was wrong. This is true even for prototypes. Most of the time any type declarations you need are straightforward and once you know your code better you can start introducing more exotic types to capture more errors later.
- rocky1138 9y ago
  A really basic example would be the "as GameObject" part of this statement in C#: `GameObject gameObject = GameObject.Instantiate(MyGameObject, Vector3.zero, Quaternion.Identity) as GameObject;". It's annoying to have to type "as GameObject" when very clearly I am creating a GameObject type (the first thing in the entire statement). Programming languages should be smart enough to figure out that's what I'm trying to do rather than require me to type that out.
  - argv_empty 9y ago
    Like GP, I often wonder what untyped languages offer over typed languages for prototyping, and this "soooo much annotation!" thing just isn't a satisfying answer anymore. "Typed" does not mean "as verbose as C#/Java."
  - dozzie 9y ago
    First, this annoyance does not come from static typing, it comes from C#'s type system. There are statically typed languages where you just construct the value and assign it to a variable, and compiler infers variable's type for you (e.g. OCaml). Then, typing the class name is a trivial matter. My editor offers me a generic text completion command, so I don't type full "GameObject", I just type "Ga" and hit ^P. Maybe you should try using a good text editor?
  - sqeaky 9y ago
    Have an upvote for being perfectly reasonable and attempting to provide examples and reason, even if I disagree with them. Rather than deflect away from C#, I will take the unpopular stance of defending verbosity. Does typing that really represent a large waste of time? Do you spend more time physically typing than doing anything else while coding? I spend most my time thinking or reading old code. I might type that once and read it 100 times and pass the debugger over it 6 or 7 times and adjust the line a similar amount in the lifespan of that of the code. For reading it is entirely clear and leaves little ambiguity about what kinds of operations are allowed on GameObject (presuming I know something about the GameObject class and the Entity Component System in place). I know its location and its rotation and I know that those are unlikely to be the source of bugs. I might need to reference `MyGameObject` to get the specifics of the behavior, but if I am troubleshooting location or rotation errors, I know what code I am not looking at. If I am troubleshooting any other behavior I again know about whole regions of code I don't need to look at. It can be hard to internalize all that a type system buys for you because none of it is immediate, it is more about all the time you don't spend doing unproductive things. I find that in more dynamically typed languages I spend two the three times as much time debugging than in static languages.
naasking 9y ago
> It's not so great when I'm trying something new and am still trying to work out if what I want to do is even possible, since I find myself trying to identify the right type to use in a given situation rather than proving that I'm even able to do it. Finding the right type is solving most of the problem. If you can find the right type, you can solve the problem. If you're having trouble finding the right type, then you don't yet understand the problem well enough, and modelling what you do know with types quickly points out what parts of the problem you haven't fully understood, without having to run broken, half-specified programs that cover only part of the problem space. What makes you think being able to run such half-specified programs for part of the problem will actually help with answering this question?
- Veedrac 9y ago
  > If you can find the right type, you can solve the problem. Do you actually believe this?
  - jerf 9y ago
    What's the most advanced type system you've used? It's quite difficult to explain how much work a very strong type system can do for you if you're used to something like C as your definition of "static typing". I mean this comment comment completely straight and polite, and I'm trying to help people answer your very reasonable question by asking you for some details that will help calibrate the answer.
    - Veedrac 9y ago
      Technically that would be something like Haskell's, but I only have surface-level fluency. More to the point would be the most complex stuff I've had reason to do with a type system, which caps at around this generic state machine: https://play.rust-lang.org/?gist=3fdb20c34d589a2576c6bb137b9fd359&version=stable&backtrace=0 https://play.rust-lang.org/?gist=3fdb20c34d589a2576c6bb137b9... (TL;DR: A type that encodes a state machine (and is generic over the implementation) that allows you to guarantee reaching a terminating state.) In practice I rather my types looking much plainer, though: https://github.com/llogiq/bytecount/blob/master/src/lib.rs https://github.com/llogiq/bytecount/blob/master/src/lib.rs
mixedCase 9y ago
With a good type system, instead of writing algorithms first you would write data structures that convey the ideas behind the software's intent clearly. Then you start writing the algorithms that manipulate these data structures. If what you're trying to do is viable, then you'll be able to express it in the domain model.
- sk5t 9y ago
  Yes! I've found it quite effective to start new problems with some (mostly composition-based) types as a means of jotting down the core inputs and outputs, then work out towards the edges in both directions with deserializers/readers/parsers in one direction, and repositories and work-doing algorithms in the other direction. A little dependency injection to wire the pieces together in complex systems and you're in business.
- jmull 9y ago
  I usually start design with a domain model, whatever the type system I'll be working with. (Just pointing out you can go this route regardless of your type system.)
marcosdumay 9y ago
Personally, I did never feel that way. Either types come out mechanically and just mean some more typing slowing me down because they don't say anything interesting, or creating the types is exactly "proving that I'm even able to do it". I tried, but I can't recall any single time when thinking about types distracted me from thinking about the problem. Moreover, writing down the types by creating stub functions is a great method of designing.
JamesBarney 9y ago
When I'm still prototyping I usually pick the part of the project I am the most uncertain about, then write a big function with lots of anonymous types. Once I feel more familiar with it I refactor into types. But types can also be really useful when you are in the process of learning your domain. If I'm using javascript and I realize I could better represent my code if I did some refactorings I usually don't touch it because I fear breaking something. On the other hand if I'm using a statically typed language I feel free to refactor to my hearts content with the knowledge that the chance I break something is far smaller.

rdtsc 9y ago

Good post, but note all those things you don't need a statically typed language. Erlang for example is a dynamically typed language but it has Dialyzer - a type checker. The more precisely you define the types the more discrepancies and issues it will find in the code, exactly the kind of stuff the author mentions. http://learnyousomeerlang.com/dialyzer http://learnyousomeerlang.com/dialyzer That's technically called "success typing" http://www.it.uu.se/research/group/hipe/papers/succ_types.pdf http://www.it.uu.se/research/group/hipe/papers/succ_types.pd... Python has that too with MyPy. That came much later than Erlang and I haven't used yet so not sure how well it works http://mypy-lang.org/ http://mypy-lang.org/ They seemed to have copied success typing but don't actually mention it anywhere.

napsterbr 9y ago
Erlang with dialyzer is a great "mix", it allows you to move as quickly you would with a dynamic language and, as long as you define the type specs, have a reassuring type safety. Of course it's nowhere near haskell's or elms type safety because, as you said, dialyzer follows the success typing model, sort of like an optimistic one ("you are correct until I prove you otherwise"), and haskell and elm follow the opposite way ("you are wrong until you prove me otherwise "). It's a tradeoff, as everything else in computer science, and one that has worked for us. Can't recommend both erlang and dialyzer enough :)
- zsd 9y ago
  Success typing really seems both ideal for me and the only sane way to do optional, progressive typing. I wonder if Ruby could do it? I think there are too many ways for an expression to be invoked from friggin anywhere in Ruby to make that possible.
- dom0 9y ago
  The funny thing about "moving quickly in dynamic languages" is that it doesn't last. Refactoring code in a dynamic language gets difficult fast and is an entirely hopeless endeavour without a huge test suite (you obviously need tests on every level, because you can't refactor an interface and its test at the same time and still think it's working as intended). Typed code may be slower and more cumbersome (to some) to write in the first place, but is usually much easier to maintain in my experience.

AnimalMuppet 9y ago

A line from a novel by Georgette Heyer: "I look for trouble. I don't wait to have it brought to my attention." That is, if there's a type problem, I want to know at compile time, not at run time. But I'm in embedded systems. My stuff looks like just a machine to the customer. They don't want a type error at runtime messing them up. That may not be your world. If you'd rather things go happily along until the circumstances actually occur in execution, and if that ever happens, you then find out about the type problem, well, that's what is reasonable to you in your environment and circumstances, and that's fine. Use dynamic typing, and don't feel guilty.

gumby 9y ago

Some languages mix static and dynamic typing. For example MACLISP used this to great effect to make MACSYMA super fast. All the numeric code was statically typed and the compiler built code that was as fast as hand crafted assembly. Yet you could write conventional Lisp code that called this static code just like any other code. MACLISP derivatives like lisp machine lisp also implemented this stuff and used it for system code. I used it heavily. All that survived into Common Lisp but I am not up on the current state of lisp implementations and have no idea if people bother to take advantage of it any more.

shakna 9y ago
C++ is in this boat now. Most of the time I'd recommend the new type-safe union std::variant, but std::any is there. It is kinda a static type, but as a container-type of anything in the type system, it may as well be a dynamic type. --- > All that survived into Common Lisp but I am not up on the current state of lisp implementations and have no idea if people bother to take advantage of it any more. Typed Racket uses the early guard theories from CL [1], and it does have an optimiser [2], though it has some quirks. And though I can't find it now, there was a fairly recent research paper on using a macro system to static type check at compile-time and optimise for Scheme. But, I should point out that Scheme doesn't need it for optimisation - compiling Scheme to C is easy, and easy to make the result fast. Its more about safety. And there's always Shen which uses sequent calculus [3] for their optional static type system. [0] https://docs.racket-lang.org/ts-guide/ https://docs.racket-lang.org/ts-guide/ [1] http://www.cs.utexas.edu/users/boyer/ftp/diss/akers.pdf http://www.cs.utexas.edu/users/boyer/ftp/diss/akers.pdf [2] https://docs.racket-lang.org/ts-guide/optimization.html https://docs.racket-lang.org/ts-guide/optimization.html [3] http://shenlanguage.org/learn-shen/index.html#10%20Sequent%20Calculus http://shenlanguage.org/learn-shen/index.html#10%20Sequent%2...
- gumby 9y ago
  > Most of the time I'd recommend the new type-safe union std::variant Neither g++ 7 nor Clang/LLVM 4.0.1 support std::variant yet :-(. We started a new (blank buffer) codebase earlier this year and decided to use C++17 as the implementation language, which has exposed us to the gaps...which are surprisingly few! But sadly this is one of them.

simplify 9y ago

If you haven't thought much about type systems but want to understand what the big deal is, I wrote a post specifically for you [1]. It draws motivation for wanting a good static type system from first principles. [1] http://gilbert.ghost.io/type-systems-for-beginners-an-introduction/ http://gilbert.ghost.io/type-systems-for-beginners-an-introd... (I posted this on a similar story and it was received very well, so I thought I might post it again for those who haven't seen it.)

benhoyt 9y ago

Counterpoint I wrote a while back that focuses on compilation speed: http://benhoyt.com/writings/language-speed/ http://benhoyt.com/writings/language-speed/ I've used Scala a fair bit recently, and the compiler is so dog slow it's painful. Maybe it's just my relative fluency with Python, but I find I'm much more productive with Python's almost instant edit-compile-run sequence. Edit: I do like many of the benefits of static typing, though. I think mypy is coming into its own in the Python community, especially now with Guido behind it. Maybe this kind of optional typing is the best of both worlds...

zem 9y ago
that's one of the things go got right - they had fast compilation speed as a first-class goal right from the beginning.
- jerf 9y ago
  They also have a really, really simple type system that can't play very many of the games that type system experts would like to play, so it doesn't cost them a lot of runtime at compile time. I'm sort of curious what the abstract minimum penalty is for the very advanced type systems. Are GHC (Haskell) and rustc already within, say, 5x of the optimal possible speed, or might we be able to have a very advanced type system and faster compiling? Time shall tell, I suppose.
MrRadar 9y ago
Check out D (https://dlang.org/ https://dlang.org/). It has a reasonably powerful static type system and the dmd compiler is lighting fast.
mahyarm 9y ago
I would prefer mandatory typing with a dev mode that makes it optional for speed. With optional typing, you end up with the third party ecosystem not having typing, which makes it hard to enforce type safety with a codebase that is fully type safe itself.
willtim 9y ago

blauditore 9y ago

I thought this was quite clear, and it's what I've always been missing in languages like Python or JS. Yet I meet many devs, especially coming from such languages, making fun of Java for its verbosity and clumsiness. On the other hand, it leads to some people abusing the static type system: They just randomly change types until it somehow compiles, without thinking about what their doing.

captainmuon 9y ago
> They just randomly change types until it somehow compiles, without thinking about what their doing. I did that, too, when I was inexperienced with C++. Especially with const, but also with * and &. But somehow it "clicked" at one point and I don't have that problem anymore. In recent times, I've found static type systems to helpfully nudge me in the direction of correct code. I was pleasantly surprised by TypeScript. Also, in modern C++, if you use unique_ptr, shared_ptr, try to get rid of naked pointers, and use value types and RAII if possible, the code ends up a lot cleaner. I've found a couple of places where ownership was unclear, and I previously had circular references or dangling pointers as a result. And anecdotically, the way people program in Haskell is basically, write what you mean, and then fix it until it compiles; it will likely also be correct.
mcphage 9y ago
> making fun of Java for its verbosity and clumsiness Java has a particularly verbose and clumsy type system.
- shock 9y ago
  What do you mean it has a verbose type system?
  - mcphage 9y ago
    Person myPerson = new Person("My", "Name") You need to specify the class twice on the same line, because Java can't figure it out on its own.

falcolas 9y ago

There is never a person more zealous (and vocal in their zealotry) than a new convert. You don't see the bad points, just the good. That's how this post comes across: "Types are so awesome, let me show you how awesome types are!" Come back in two years, show us how the types feel after the honeymoon is over.

jamescostian 9y ago
While I agree that type systems often get in the way, and that the author is only pointing out bad points and not good ones, aren't you doing the same? At least the author is trying to back up their claims (e.g. they provide an example where someone decided to put sizes in strings). The honeymoon part is also an unfair assumption, not to mention incorrect. I just clicked on "About me", clicked on the author's github link, and after some scrolling and clicks, I found a rust commit from August 2015 the author made - thus, the author has been here for 2 years, and is not some newbie. You should provide a list of cons involved with type systems that aren't so glaringly obvious that the author has probably already ran into them, and that will serve as a much stronger argument (e.g. you could bring up the fact that in large codebases with lots of generics, type systems drastically increase time spent typing, as well as cognitive overhead when there are <T>s and <T, E>s and so on all over the place).
- falcolas 9y ago
  Because my comment was not about type systems, it was about the fervor and lack of usefulness of the post itself. Plus, I'd just be repeating myself and others much more eloquent than I - why do that? Plus, arguments about typed languages rank up there with vi vs Emacs (or is it now vi/emacs vs. Atom/VSC?) in terms of my interest in joining them. I like statically typed languages. I like dynamically typed languages. I dislike weakly typed languages. What more to add?
  - sqeaky 9y ago
    You may be entirely correct, but the way you have presented your position looks extremely unconvincing. What I can see: You chime in on a discussion with a strongly critical viewpoint, then refuse to back it up saying you don't want to be part of certain kinds of arguments. Implying religious level flamewars, while the rest of us are keeping a level head and discussing these things based on technical merit. It looks like you are making excuses because it looks like you have no point. Even if that wasn't what you intended and you have strong points, that isn't what it looks like from the outside. Please remember that not everyone has exactly your experience so if you have examples you should share them because they will make your points stronger even if someone attempts to rebut them. It also artificially weakens your point to try to back out with what from the outside look like excuses instead of substance. Again, I must say you might be entirely correct, I just can't see that from here.

mamcx 9y ago

My dream is a static-first (like with inmutable-first) language with a way to do dynamic. The thing is not available (as far I know) is to build a dynamic object and "close it" for further modification so the compiler can optimize well. Other, that requiere good metaprograming, is to build a dynamic object AT COMPILE TIME (macro?) and close it, then the type-system work after that (F# type provider is almost this) A use case is reflect a database/data storage like JSON or relational table. I wish, like with python, to do: class Customer = @build(table("Customer")) and after this line : c = Customer() print c.name to 'c' be a static type. If at compile time, it check the type, let say the field change to c.fullname, to mark as a type error. If in runtime, like a interpreter, to "close" Customer and be certain that it never will mutate. AKA: Inmutable types/clases, but the posibility to mutate it in some discret places. Make sense?

h_r 9y ago
This sounds similar to F# type providers.
62747478182 9y ago
You may be interested in Crystal. https://crystal-lang.org/ https://crystal-lang.org/

dmux 9y ago

I'd be interested in hearing what the community has to say regarding static types and whether or not they're compatible with object-oriented programming. I've posted this link a couple times before, but it hasn't been actively discussed: https://essencesharp.wordpress.com/2014/07/17/static-typing-and-interoperability/ https://essencesharp.wordpress.com/2014/07/17/static-typing-... From that article: "Static typing inhibits interoperability. It does so between class libraries and their clients, and also between programming languages. The reason is simply because static typing violates encapsulation in general, and improperly propagates constraints that aren’t justifiable as architectural, design or implementation requirements in particular. It does so either by binding too early, or by binding (requiring) more than it should."

evincarofautumn 9y ago
Many OOP languages don’t make it easy to achieve encapsulation and composability in the presence of their particular static type systems. It sounds like he’s just arguing that nominal typing is worse than structural typing, and early binding is worse than late binding; the comparison to static type systems is a false equivalence.