8 ms·

The problem is that fundamentally we always have types. We must define different types of bytes and the different things we can do with those bytes. If you can

The problem is that fundamentally we always have types. We must define different types of bytes and the different things we can do with those bytes. If you can generate a binary from your programming language, it must use a form of static or inferred typing to know what assembly code to generate. A dynamic language just checks at runtime, and adds a bunch of overhead, which isn't always necessary, and is more likely to result in weird "defined" behavior like we get from javascript and php. Typescript is very popular because you can make certain guarantees at compile time, instead of a vague hand-wave of "the code looks good". As an example of the benefits of type-checking, in the Vulkan api, there are a lot of handles. VkRenderPass, VkPipeline, VkSwapchain, VkDevice, etc. All of these are just pointers. If we take a function like: void vkDestroyCommandPool(VkDevice,VkCommandPool,const VkAllocationCallbacks*);` And remove the type checking: void vkDestroyCommandPool(void*,void*,const void*); It is the same API, but without type-checking. Even if the parameters are labelled, with this new API I could mess up and pass the wrong thing.

wool_gather 6y ago
The article is not even remotely suggesting removing type information. On the contrary, it's talking about some ways to augment a type checker with different grammar or ways of constructing APIs.
- MetaDark 6y ago
  No, but you can always encode this augmented information in types to make it explicit, and possibly help the compiler make optimizations. Using a weaker type when you can use a stronger type is just as bad as removing type information.
  - masklinn 6y ago
    > No, but you can always encode this augmented information in types to make it explicit Technically yes, but not all type systems make it practical, or really relevant e.g. you can encode nullability in a type in java… but your reference to your Optional is still itself nullable.
inetknght 6y ago
In C perhaps that's unfortunate. I'm sure glad we have more modern C++ that would enforce pointer types. ... as long as the functions aren't declared in `extern "C" { ... }` which many libraries are. That's for many reasons, some of which include the very type system itself being an inhibitor of easy integration across languages.
- moonchild 6y ago
  I don't quite follow. C will also prevent you from mixing up disparate pointer types; and c++ has no protection against void pointers.
  - inetknght 6y ago
    > C will also prevent you from mixing up disparate pointer types No it won't. In C++ it's a compile error [0]. In C it's just a warning [1]. > c++ has no protection against void pointers You're somewhat correct but the answer is a lot more nuanced (because void* is very nuanced). Again, C++ will complain unless you do it "right" [2] while C is ... willing to let you blow your leg off [3]. However the definition of "right" is still just as dangerous as C's because all type information was lost in the void and it's up to the programmer to get it right -- and programmers are notoriously buggy. [0] https://gcc.godbolt.org/z/166ns8 https://gcc.godbolt.org/z/166ns8 [1] https://gcc.godbolt.org/z/vEnajj https://gcc.godbolt.org/z/vEnajj [2] https://gcc.godbolt.org/z/cGe39z https://gcc.godbolt.org/z/cGe39z [3] https://gcc.godbolt.org/z/orb1s8 https://gcc.godbolt.org/z/orb1s8
    - int_19h 6y ago
      Using extern "C" doesn't change the C++ rules for implicit pointer conversions, though.
cle 6y ago
I think it’s important to be more specific here. You can always mess up and pass the wrong thing, the type system can never know what is semantically correct, no matter how strict your types are. They’re about ergonomically reducing the space of valid programs. There are a lot of interesting tradeoffs to be made there. Over strict specification (whether parsing or type checking), specifically checking for invariants that aren’t actually useful, can make code and systems brittle and hard to change, just like under specifying them. The specifications can also be different depending on what you’re doing with the data. Also as the expressiveness of types increases, the space of possible ways to constrain your program space goes up, along with the complexity of the transformations of that space, making it difficult to understand what the valid program space actually is, hard to understand when you’ve accidentally excluded perfectly valid programs, etc. So yes, fundamentally there are always types and underlying structure to useful data, but saying that it has “a” type is dramatically over-simplifying things.
- choeger 6y ago
  >I think it’s important to be more specific here. You can always mess up and pass the wrong thing, the type system can never know what is semantically correct This is not true. Consider the map function of a typical functional language with parametric polymorphism: map : (a -> b) -> [a] -> [b] That signature is complete, it covers everything there is to know about the function. And, except for trivial implementations, there is no way to implement it wrongly. In some cases, one can even rule out trivial implementations and infer the correct implementations from the type signature alone. In any case, there is no "semantically wrong" input to such a function. It is just a function and totally agnostic regarding your use case.
  - tsimionescu 6y ago
    Of course that type doesn't encode everything there is to know about that function, even assuming purity. Here are some functions that match that type signature: map1 foo x:xs = [foo x] mapR foo x:xs = append (mapR foo xs) foo x mapI foo x:xs = foo x : mapI foo x:xs Of course, we can create many more functions that arrange the values in other creative ways, that add more or fewer values etc. If the function isn't pure, we can also imagine many more dimensions of functions that do arbitrarily different things from what you would expect. If you want complete signatures without dependent types, you need functions which take only single values of different unknown types, like apply: (a -> b) -> a -> b. If you have more than one parameter of the same unknown type, you'll have some ambiguity already. Non-dependent types can only be used to encode extremely simple properties of a program. They are certainly useful, but they are not in any way the be-all, end-all of static verification.
mumblemumble 6y ago
I don't see this as challenging anything that the article is ultimately proposing. See, for example, the last paragraph: > I thank the flying spaghetti monster almost every day for the type system in my day job (and that is only Java’s tepid concoction)... Isn't exactly a statement you'd expect to find in the concluding remarks an essay whose goal is to question the value of type systems or static types. It's presumably something more nuanced like that. Maybe something more like > we are in danger of thinking that type systems are the only way of achieving correctness in software construction. Which seems reasonable to me. Type systems are excellent for eliminating certain classes of errors. But we shouldn't let them become a golden hammer. Even if they can be used to eliminate other classes of errors, that doesn't necessarily mean they're the best tool for the job. Lately, for example, I've been seeing some disillusionment with dependent typing, and people saying, in effect, "Yeah, it's a really impressive technique, but try to find a simpler solution first." And some of those simpler solutions do come from the dynamic programming world. For example, "You can then go further and remove the more primitive operations, only allowing access to the higher level abstractions," is another excellent way to make illegal states unrepresentable. And you don't need shiny new programming languages or rocket powered type systems to do it. I was really rather disappointed that that section of the article gave a nod to Dijkstra, but completely failed to mention Alan Kay's The Early History of Smalltalk, which was, to an approximation, several thousand words' worth of grinding away on that point.
moonchild 6y ago
And indeed, in opengl, where all handles have the same type (GLuint), it's very easy to mix up handles of different types. It's quite easy to fix this without breaking ABI compatibility; but it hasn't been done in any implementation that I know of.

wool_gather 6y ago

The article is not even remotely suggesting removing type information. On the contrary, it's talking about some ways to augment a type checker with different grammar or ways of constructing APIs.

MetaDark 6y ago
No, but you can always encode this augmented information in types to make it explicit, and possibly help the compiler make optimizations. Using a weaker type when you can use a stronger type is just as bad as removing type information.
- masklinn 6y ago
  > No, but you can always encode this augmented information in types to make it explicit Technically yes, but not all type systems make it practical, or really relevant e.g. you can encode nullability in a type in java… but your reference to your Optional is still itself nullable.

inetknght 6y ago

In C perhaps that's unfortunate. I'm sure glad we have more modern C++ that would enforce pointer types. ... as long as the functions aren't declared in `extern "C" { ... }` which many libraries are. That's for many reasons, some of which include the very type system itself being an inhibitor of easy integration across languages.

moonchild 6y ago
I don't quite follow. C will also prevent you from mixing up disparate pointer types; and c++ has no protection against void pointers.
- inetknght 6y ago
  > C will also prevent you from mixing up disparate pointer types No it won't. In C++ it's a compile error [0]. In C it's just a warning [1]. > c++ has no protection against void pointers You're somewhat correct but the answer is a lot more nuanced (because void* is very nuanced). Again, C++ will complain unless you do it "right" [2] while C is ... willing to let you blow your leg off [3]. However the definition of "right" is still just as dangerous as C's because all type information was lost in the void and it's up to the programmer to get it right -- and programmers are notoriously buggy. [0] https://gcc.godbolt.org/z/166ns8 https://gcc.godbolt.org/z/166ns8 [1] https://gcc.godbolt.org/z/vEnajj https://gcc.godbolt.org/z/vEnajj [2] https://gcc.godbolt.org/z/cGe39z https://gcc.godbolt.org/z/cGe39z [3] https://gcc.godbolt.org/z/orb1s8 https://gcc.godbolt.org/z/orb1s8
  - int_19h 6y ago
    Using extern "C" doesn't change the C++ rules for implicit pointer conversions, though.

cle 6y ago

I think it’s important to be more specific here. You can always mess up and pass the wrong thing, the type system can never know what is semantically correct, no matter how strict your types are. They’re about ergonomically reducing the space of valid programs. There are a lot of interesting tradeoffs to be made there. Over strict specification (whether parsing or type checking), specifically checking for invariants that aren’t actually useful, can make code and systems brittle and hard to change, just like under specifying them. The specifications can also be different depending on what you’re doing with the data. Also as the expressiveness of types increases, the space of possible ways to constrain your program space goes up, along with the complexity of the transformations of that space, making it difficult to understand what the valid program space actually is, hard to understand when you’ve accidentally excluded perfectly valid programs, etc. So yes, fundamentally there are always types and underlying structure to useful data, but saying that it has “a” type is dramatically over-simplifying things.

choeger 6y ago
>I think it’s important to be more specific here. You can always mess up and pass the wrong thing, the type system can never know what is semantically correct This is not true. Consider the map function of a typical functional language with parametric polymorphism: map : (a -> b) -> [a] -> [b] That signature is complete, it covers everything there is to know about the function. And, except for trivial implementations, there is no way to implement it wrongly. In some cases, one can even rule out trivial implementations and infer the correct implementations from the type signature alone. In any case, there is no "semantically wrong" input to such a function. It is just a function and totally agnostic regarding your use case.
- tsimionescu 6y ago
  Of course that type doesn't encode everything there is to know about that function, even assuming purity. Here are some functions that match that type signature: map1 foo x:xs = [foo x] mapR foo x:xs = append (mapR foo xs) foo x mapI foo x:xs = foo x : mapI foo x:xs Of course, we can create many more functions that arrange the values in other creative ways, that add more or fewer values etc. If the function isn't pure, we can also imagine many more dimensions of functions that do arbitrarily different things from what you would expect. If you want complete signatures without dependent types, you need functions which take only single values of different unknown types, like apply: (a -> b) -> a -> b. If you have more than one parameter of the same unknown type, you'll have some ambiguity already. Non-dependent types can only be used to encode extremely simple properties of a program. They are certainly useful, but they are not in any way the be-all, end-all of static verification.

mumblemumble 6y ago

I don't see this as challenging anything that the article is ultimately proposing. See, for example, the last paragraph: > I thank the flying spaghetti monster almost every day for the type system in my day job (and that is only Java’s tepid concoction)... Isn't exactly a statement you'd expect to find in the concluding remarks an essay whose goal is to question the value of type systems or static types. It's presumably something more nuanced like that. Maybe something more like > we are in danger of thinking that type systems are the only way of achieving correctness in software construction. Which seems reasonable to me. Type systems are excellent for eliminating certain classes of errors. But we shouldn't let them become a golden hammer. Even if they can be used to eliminate other classes of errors, that doesn't necessarily mean they're the best tool for the job. Lately, for example, I've been seeing some disillusionment with dependent typing, and people saying, in effect, "Yeah, it's a really impressive technique, but try to find a simpler solution first." And some of those simpler solutions do come from the dynamic programming world. For example, "You can then go further and remove the more primitive operations, only allowing access to the higher level abstractions," is another excellent way to make illegal states unrepresentable. And you don't need shiny new programming languages or rocket powered type systems to do it. I was really rather disappointed that that section of the article gave a nod to Dijkstra, but completely failed to mention Alan Kay's The Early History of Smalltalk, which was, to an approximation, several thousand words' worth of grinding away on that point.

moonchild 6y ago

And indeed, in opengl, where all handles have the same type (GLuint), it's very easy to mix up handles of different types. It's quite easy to fix this without breaking ABI compatibility; but it hasn't been done in any implementation that I know of.