4 ms·
Rather than being specific to IO, I think you're missing an understanding of algebraic data types, and their use in strongly and statically typed languages. The
by scott_s 12y ago
Rather than being specific to IO, I think you're missing an understanding of algebraic data types, and their use in strongly and statically typed languages. The wikipedia entry is a decent place to start: http://en.wikipedia.org/wiki/Algebraic_data_type http://en.wikipedia.org/wiki/Algebraic_data_type
- taeric 12y agoActually, I think I'm just having more of this conversation in my head than I am in this forum. For better and worse. :) My point here was more that just because you have a file handle doesn't mean you have a valid place to write data. Making it optional would possibly prevent some bugs, true. However, it doesn't really help as soon as you have a filehandle to a full filesystem, for example. (Or, well, any other problem that usually happens to cause grief with the filesystems. You got a file, but by the time you went to use it the system was full and you couldn't, etc.) Regardless, I should have been clearer on many points (and I fully accept I was flat out wrong on at least a few :) ). I do think null pointers are bad. I also know with proper static analysis tools, you don't need a whole new type system to make things better. Unless you are considering tools such as Coverity and friends some form of type system.
- dllthomas 12y ago"Unless you are considering tools such as Coverity and friends some form of type system." I would, for the record. There was a thread some days ago (https://news.ycombinator.com/item?id=7916554 https://news.ycombinator.com/item?id=7916554) where I described some hackary I used to get particular guarantees out of C's type system. My response in https://news.ycombinator.com/item?id=7918423 https://news.ycombinator.com/item?id=7918423 seems tangentially relevant here. Type systems aren't (only/necessarily) features of a language.
- taeric 12y agoThat seems like an odd stance to take, to me. Am I the one that is actually on the "odd" end of this debate?
- dllthomas 12y agoI don't pretend my understanding is the most common understanding. I think it squares better with the state of research on these things than the most common understanding, though. I could absolutely be mistaken - I am more a practitioner than theoretician.
- taeric 12y agoIt makes sense that the theories behind them are the same. The distinction I make is whether or not the type is directly conveyed in the language. I don't know if that is a false distinction or not.
- dllthomas 12y agoI think that is mostly a false distinction. Types that are not directly conveyed in the language (and by that I assume you mean "that the compiler is aware of" and not "that are syntactically spelled out all over" - inference accounting for most of that difference) obviously cannot be used to specify semantics. I think the only other differences stem ultimately from standardization. Tooling could exploit any type system a program is known to follow. Likewise, compiler optimizations, &c, &c.
- taeric 12y agoTooling can also go beyond types, though. Interleaved calls to different types, for example, can be found through tooling. Types can't really do that. Well, I realize that is false. But the hoops all of the examples I have seen that types have to jump through to accomplish that aren't exactly pleasant. So, maybe my preference is just that tooling can give you many of the benefits of more advanced type systems, without having to have all of the boilerplate of it everywhere in the code. At any rate, I should say thank you very much for keeping this dialog going. Been a blast!
- dllthomas 12y ago"Tooling can also go beyond types, though." By "tooling" there, I wasn't referring to static analysis. I meant things like type-directed name resolution, type-directed completion, Agda's "holes", and so on. Strictly, these do not rely on the type system being "a part of" the language, but they do rely on some degree of standardization on a particular type system for the tool to work (or work well). "Interleaved calls to different types, for example, can be found through tooling." I actually don't understand exactly what you mean here. You might be surprised what even pretty rudimentary type systems can find if you leverage 'em right, though - as I mentioned in that other thread, I track which threads access what resources, and which functions live on which threads, with C's type system unadorned by additional checks (I do use additional static analysis, it just is entirely unnecessary to catch this one). "Well, I realize that is false. But the hoops all of the examples I have seen that types have to jump through to accomplish that aren't exactly pleasant. "So, maybe my preference is just that tooling can give you many of the benefits of more advanced type systems, without having to have all of the boilerplate of it everywhere in the code." Ironically, I think my C code has more annotations for my static analysis tool-of-choice than the C types. Certainly there are a lot of poor type systems, and a lot of languages that expose particular type systems poorly. Boilerplate type annotations are mostly unnecessary in languages with type inference. As I've said elsewhere, though, your tooling may be "more advanced type systems". Splint, for instance, can enforce linear typing - something that is not a part of the type system laid out in the C standard (or that enforced by typical C compilers, even with warnings). "At any rate, I should say thank you very much for keeping this dialog going. Been a blast!" Yes, it's turned out great :)