7 ms·

Ditto on generic methods both changing the game for Dart and being necessary. I spend most of my time in Dart, Swift and ObjC, and I've built serious applicatio

• willtim 9y ago
  As a far as I can tell, an "optional type system" is just an unsound type system with a marketing name. Any decent static type system would allow one to progressively increase the level of typing, the weakest form being using a Variant type to hold all other types. The advantage here is that any invariants/proofs that are captured in the system are not compromised by unsoundness.
  • munificent 9y ago
    > As a far as I can tell, an "optional type system" is > just an unsound type system with a marketing name. It is a term with a specific meaning. The key bit separating it from both gradual typing and a static type system with a dynamic type (like Scala or C#) is that in an optionally typed language, the type system has zero runtime effect. If you were to take a source file and mechanically strip out all of the type annotations, the resulting program behaves identically to the original one. Dart 1.0 was an optionally typed language. Dart 2.0 is not -- we've gone to a mandatory static type system (with lots of inference and a dynamic type). The limitations of optional typing are simply too onerous, and it's just not what users expected or want. > Any decent static type system would allow one to > progressively increase the level of typing, the weakest > form being using a Variant type to hold all other types. That's the dream of optional typing and gradual typing. In practice, I have yet to see a language that does this harmoniously. It sounds simple, but things quickly get very complex when you start working with generic types and first-class functions because the boundary between the untyped and typed code gets very strange. To keep the guarantees you expect inside your typed code, you have to figure out how to handle untyped data that flows into it. That gets nasty very quickly when that untyped data may be an instance of a generic class or a function.
    • willtim 9y ago
      > To keep the guarantees you expect inside your typed code, you have to figure out how to handle untyped data that flows into it. This would be solved in a conventional static type system by forcing the user to eliminate the variant, and forcing the user to deal with the case that it has an unexpected value. So I cannot see why even C# dynamic is necessary, except to perhaps save some thinking, but this isn't a good thing IMHO.
      • avip 9y ago
        The dynamic type was added to C# to facilitate interoperability (ex. DLR), not so much to encourage lazy devs to get their bugs at runtime rather than compile time.
        • pjmlp 9y ago
          Additionally to simplify dynamic dispatch calls on COM.
        • willtim 9y ago
          I still do not understand why this cannot be done via a Variant type. Also it doesn't explain why Dart 2 has a similar feature.
          • barrkel 9y ago
            Think of dynamic as a different word for Variant. The semantic differences for OLE2 Variants vs C# dynamic mostly only exist in implementation protocols.
          • masklinn 9y ago
            > I still do not understand why this cannot be done via a Variant type. Makes little difference, either way you need a magical type since it has to allow any method call at compile time, and then requires enough RTTI that it can check for and dispatch method calls at runtime. Whether you call it Variant or dynamic has no relevance.
      • 9y ago
  • geofft 9y ago
    I don't think I've seen a Variant type in any language that doesn't store some form of type information at runtime (unless you count C void pointers, which I don't), and "any decent static type system" incurs no runtime overhead in the common case.
    • willtim 9y ago
      Of course variants would need to tag their payload, but this is what all dynamic languages need to do anyway. My point was that such dynamic behaviour can be done without resorting to an unsound "optional type system".
      • geofft 9y ago
        Isn't Dart compiled to JavaScript? As far as I can tell by playing around with DartPad, a normal int in Dart carries no runtime information indicating that it is an int (other than the fact that it is a JavaScript-level int). If you wanted to add variants to Dart, you'd either need to add this runtime information, or limit the Dart typesystem to be no more and no less than what the JavaScript typesystem already stores dynamically.
        • tome 9y ago
          Surely JavaScript itself tags ints?!
          • geofft 9y ago
            It tags numbers, yes, but actually it doesn't tag ints in particular - there is no integer type in javascript, just a 64-bit floating point one. (This is why asm.js code sticks |0 after every arithmetic operation involving integers: that forces rounding the number as if it were an integer, and therefore allows optimizing the expression to use integer instead of floating-point arithmetic.) If Dart wants to distinguish ints and doubles, it needs to keep track of that on its own; if it has a JavaScript variable x and needs to know calculates x/2, it won't know whether to round it as if it were integer arithmetic, or return a floating-point value. Usually it is enough to do this at compile time (the function calculating x/2 knows whether it's halving a Dart-level double or a Dart-level int), and so there's no need to make x an object that remembers its own Dart type. Also, even if JavaScript distinguished ints and doubles, a higher-level language is likely to want to have multiple kinds of things with an int representation: bools, enums, bitfields, Unicode scalar values, etc. Again, ideally that information is tracked at compile time and the knowledge of what to do with an int representation is inserted into the compiled code, and so no metadata needs to be stored at runtime.
  • rbehrends 9y ago
    No, there's more to it. There's been some research in recent years on the actual benefits of types and the results are less straightforward than some people think. An important aspect of type annotations, for example, seems to be that they help document the API of a module, regardless of whether they're statically checked. This is especially relevant with respect to maintenance tasks. Conversely, the benefits of static type checking to get correct code initially seem to be a lot murkier. There seems to be a cost associated with static types and that is that it takes longer to write code; time that can be spent in a dynamically typed language on other validation work (remember that types do not even remotely capture all software defects). This means that it is definitely worth exploring the benefits of optional/gradual/soft typing vs. static typing and/or runtime type checking vs. compile-time type checking. Conversely, the assumption that static types are an unalloyed good is not currently borne out by the evidence (in part, of course, that is because the evidence is inconclusive).
    • adrianratnapala 9y ago
      There seems to be a cost associated with static types and that is that it takes longer to write code; But this is not the only cost that matters, indeed might not even be a cost. I've gone from being neutral about static vs. dynamic types to being pro-static types -- and the change happened when maintenance became a bigger part of my job. Writing new code is now far less important to me than looking at a small part of a large system and trying to understand what is and is a not possible at that point. Static typing does not make this easy, but dynamic typing makes it far more difficult.
      • rbehrends 9y ago
        > But this is not the only cost that matters, indeed might not even be a cost. I'm not saying otherwise. My point is that there's no objective way to proclaim one better than the other. This depends on application domain, economic constraints, engineering constraints, what you're doing, and so forth. Writing Ada software that controls a pacemaker has totally different requirements than exploratory programming in Jupyter that mostly deals with integers, floats, and arrays and matrices thereof, for example.
  • barrkel 9y ago
    Writing well-typed code means writing a proof of some set of properties over the code. There are three assumptions here: (1) creating abstractions that are typed correctly is easy (2) the existing abstractions you're building from are correctly typed (3) the properties that the type system proves are valuable enough to reward the effort Whether (1) is true depends on your type system. If it's very simple (e.g. dynamically typed), it's trivially true. If it's rich and expressive, it can sometimes be impossible to express your intent without obfuscating your types (e.g. using pointers and typecasts or polymorphism or some other loophole); and with some type systems, it's plain impossible to express some valid programs. Whether (2) is true is a social problem. You need to have enough sensible people in your community such that you get to use List<T> rather than ObjectList with typecasts, or what have you. What's available in the runtime libraries often translates into what's commonly used for APIs in third party modules, and if the library of types isn't rich enough, APIs will use loopholes or typecasts or other mechanisms that obfuscate types. Third party code turns into a kind of firewall that stops your types (and the information, proofs, they convey) from flowing from one module to another in your program. Whether (3) is true also depends on your type system, but also on your application domain. It's in direct opposition to (1); the more you can prove with your type system, the harder it normally is to write code that proves exactly the right things, and neither more nor less (the risk is usually too little type information flowing through). If the properties being proved are important to your application domain, then that gives a big boost to type systems that can prove those properties. If it's just because it gives you warm fuzzies, and testing is what proves interesting things because interesting properties (in your domain) are harder to prove with a type system, then rich type systems are less useful. Personally, I was once a strong proponent of rich expressive type systems. But I eventually learned that they can become a kind of intellectual trap; programmers can spend too much time writing cleverly typed confections and less time actually solving problems. In extremis, layers of abstraction are created to massage the type system, often in such an indirect way that the value of the properties being proven are lost owing to the extra obfuscation. Now, I see much more value in a strong type system for languages like Rust, but much less value at higher levels of abstraction. That's because many of the properties being proven by Rust (like memory safety) are already proven in high-level dynamic languages through GC and lack of pointers and unsafe typecasts. Whereas application-level properties being proven through type systems are seldom valuable. Documentation and tooling are much stronger arguments for types in high-level languages than proofs; ironically, this means that the type systems don't need to be sound, as long as they're usually OK in practice!
  • throwaway91111 9y ago
    As a whole, you are correct. Pragmatically it allows defining the boundaries of soundness.