10 ms·

I think there's a perhaps irreconcilable disconnect between 2 camps here, but I also think that's ok and different people are allowed to like different things.

• amelius 7y ago
  Yes. Perhaps this is an indication that we actually need automated type annotation. E.g. you initially write/prototype your program in a dynamically typed form, then you click a "magic" button, and a tool converts your program into statically typed style.
  • zitterbewegung 7y ago
    Using Type inference[1] on a language could be able to figure out types in most situations. [1] https://en.wikipedia.org/wiki/Type_inference https://en.wikipedia.org/wiki/Type_inference
    • amelius 7y ago
      Yes, some programming languages take this approach but I don't think that prototyping is as easy in such languages as it is in a dynamically typed language (e.g. Haskell vs Python).
      • rwmj 7y ago
        When writing OCaml, if I'm unsure of the type I set the type to some impossible value, compile it, and the compiler tells me what the type really is.
        • hnra 7y ago
          I Haskell you simply put a "_" in the annotation and the compiler suggests the correct type.
          • dllthomas 7y ago
            You can also do this with values, asking "what goes here?" - it's great.
        • andrepd 7y ago
          Alternatively, merlin can tell you the type of the expression under your cursor, besides also flagging type mismatches like your situation.
      • yakshaving_jgt 7y ago
        In my experience (currently writing Haskell professionally, previously writing Ruby professionally) prototyping is easier in Haskell. How many systems have you prototyped in Haskell?
        • dllthomas 7y ago
          > prototyping is easier in Haskell That's very much my experience, as well. Assuming - and it's a very big assumption - that your use case has equivalent library support.
      • zitterbewegung 7y ago
        What would be neat is if you could take a Python program and run type inference on the program and it would output a type annotated version of the code.
    • azhenley 7y ago
      Yes, but "Type inference has usability problems". http://web.eecs.utk.edu/~azh/blog/typeinference.html http://web.eecs.utk.edu/~azh/blog/typeinference.html
      • leshow 7y ago
        I'm curious why you quote this like it's a fact when it's an opinion. The understanding of type inference used as the basis for making the argument in that blog post is superficial. Type inference doesn't just allow you to leave off type information from variables. A good inference engine will infer the most generic type for variables (and functions!), it's a discovery that you can query the compiler for in order to do type driven development. A full rebuttal of this blog post would take much longer, but suffice to say inference does the exact opposite of what they are claiming; it increases readability and usability.
        • azhenley 7y ago
          I quoted the title of my blog post. Do you have any evidence for your claim that it increases readability or usability? A few human-subjects studies from different labs have recently been ran on this and the findings mostly agree with my opinions. Papers forthcoming.
          • pwm 7y ago
            I don’t agree with readibility (there are pros and cons, ie. terser code vs. implicit types) but, at least in Haskell, it improves usability by inferring the most generic type to your expression.
          • leshow 7y ago
            Agree on what? "Type inference" is a broad feature, feel free to post the resources. edit: In Haskell it goes beyond just locally inferring variables, it enables a new type of development with typed holes that feels more like a back and forth conversation with the compiler. I don't see how "I can leave the types off my C# variables" has anything to do with that.
          • 7y ago
  • chongli 7y ago
    This already exists in Haskell. Firstly, Haskell has type inference so you can write entire programs without any type annotations. Second of all, since type annotations actually help to document your code, it’s recommended as good Haskell style to annotate all top-level definitions. To aid you in the latter task, you can press a key in your editor to fetch an automatically-inferred type for the name under the cursor and insert it into your code, then refine it as necessary if you find it to be too general (inference always gives the most general type possible).
    • hopia 7y ago
      On what editor setup you get this kind of functionality with Haskell? I mean the auto-insert of the inferred types.
      • chongli 7y ago
        I’ve been out of the game for a number of years but I used something called ghc-mod [1] with its associated vim plugin [2] to get this functionality. Moving forward, it seems that all of the effort has moved over to Haskell IDE Engine [3]. It looks like this exact feature hasn’t been brought over yet but it is planned. In the mean time you could still use ghc-mod though. [1] https://github.com/DanielG/ghc-mod https://github.com/DanielG/ghc-mod [2] https://github.com/eagletmt/ghcmod-vim https://github.com/eagletmt/ghcmod-vim [3] https://github.com/haskell/haskell-ide-engine https://github.com/haskell/haskell-ide-engine
        • hopia 7y ago
          Thanks for the tip! Haskell IDE engine is exactly what I've been using til now and would've been very pleased to find out it had such a convenient feature. Ghcide is on my list to try next as it's gotten a lot of attention lately.
          • jose_zap 7y ago
            Yes, it already has a code command to automatically add top level type annotations. The caveat I that it can only work if you add -Wall to your compilations flags.
  • ken 7y ago
    You mean a compiler?
  • pron 7y ago
    Unless your type system is very weak -- and in effect, an untyped language can be considered to already be doing what you said only in a type system that has a single type -- this is generally impossible (halting problem and its extensions). So you have the choice of something that's not very useful or something that's impossible -- take your pick. Type inference, as others have suggested, does not do what you want. If your program is well-typed according to a particular type system which you must have in mind while writing the program, they'll save you from writing explicit type annotations, but they cannot come up with "correct" type for a correct program that's not written for that particular type system.
  • IggleSniggle 7y ago
    TypeScript can come close to this, especially with the latest release with Assertion support. You make assertions about your code, and the downstream types are inferred based on your assertions. Thus, the runtime behavior of your code gives you progressively enhanced type-checking. If you do these assertions at the borders, your "correctness" is dependent on the strength of your runtime assertions.
• pron 7y ago
  Not all untyped languages are the same. E.g. Clojure now encourages specifying assumptions with spec annotations, some of them are stronger than those that can be expressed by Haskell's type system: i.e. they can succinctly express more about the "entire code" than Haskell's types. Types are not the only way to write formal assertions and assumptions about code. The difference between the two is in the level of sound inference that can be made (stronger with types) and the strength and expressivity of the assertions (stronger with contracts). Of course, one could say we should have both, and some languages -- like Java with JML, C with ACSL, and SPARK, as well as some research languages like Whiley and Dafny -- do. But this could add complexity, and the interesting question is, if you could just have one, what are the relative merits of either? My guess is that types would be better for enforcing code organization and for tooling (more efficient AOT code generation, safe automatic refactoring, code completion), because automatic transformations require automatic and sound inference, while contracts are better for correctness because they can more easily express stronger properties of interest, and require less effort to verify them (types require formal deductive proofs, while contracts can use those or a range of other techniques that vary in their cost and their soundness). In short, types are not the only form of formal specification, but the different forms do have different practical characteristics. What matters is not just what we want to know about the rest of the code, but how we want to use that information and how certain we need to be. Unfortunately, theoretical results tell us that we cannot have a perfect system that is always correct, cheap to use, and can allow us to express rich properties.
  • capableweb 7y ago
    Also, the following part isn't necessarily because of dynamic typing vs static > what types all the variables are, what expectations are attached to them, what mutation, if any, each method call performs But more about what the language offers. Clojure for example, goes beyond types with it's abstractions (like seq, that can be applied to strings, lists, maps and so on) and normally stays away from mutation, but when needed, makes it really explicit and easy to find those mutations.
    • pron 7y ago
      Java's JML contract system [1] allows you to explicitly state which mutations a method performs as part of its contract. [1]: https://www.openjml.org/ https://www.openjml.org/
• nhumrich 7y ago
  Your comment is spot on. But the opposite can also be true. I totally have the same issues you do at times by trying to understand types (which I feel type hinting, editors, and good variables names go a long way to help with). But I also find myself using a lot of cognitive load trying to get a correct type definition, etc (for the non simple tasks). Whether its trying to figure out how to get a certain object, because of the interfaces, factories, etc. Or trying to create a new object and trying to map things correctly. What if I just want to have a hash map full of varying object structures? (I am not saying its not possible, I am saying its a use of cognitive load)
  • UglyToad 7y ago
    Agreed, perhaps it's something like the difference between top-down vs bottom-up learning in teaching. People don't all use the same mental models and allowances need to exist for both groups. But I suspect this is true of most contentious topics in programming. For what it's worth I definitely agree there can be a lot of overhead added by typed code especially in Java or C#, but I suspect it might have less to do with the type system and more with the enterprise-ness or otherwise of those code-bases. Designing a good typed API for other people maintaining the same code-base is difficult
• kazinator 7y ago
  If you don't have to think about what mutation each method performs, if any, when switching to static typing, you're not just switching to static typing.
• zmmmmm 7y ago
  > To my mind if I return to a piece of dynamically typed code written any time other than in the same session I have to load a whole mental model of the entire code, what types all the variables are This is one reason my favorite model is the "egg model" - hard outer shell (static typed signature) of a function with a soft gooey center - dynamic code internally. It lets you use the convenience of dynamic typing but confines the scope of the mental budget to understanding just a few lines of dynamically typed code. Languages like groovy are pretty good for this type of code.