5 ms·
The point of the type system is that you can express your intent through an invariant or property at one place (i.e. the "head" function can specify that it sho
by Felz 7y ago
The point of the type system is that you can express your intent through an invariant or property at one place (i.e. the "head" function can specify that it should never be used on an empty list) and propagate that outwards so that it's enforced at all times.
This is more effective than trying to remember to always check the head function in every single place you ever try to get the first element of a list.
Yes, you can still write a compiling but wrong program. But it will likely be pretty close to what you actually want it to do, and it's easier to notice the behavior is not what you expected in one place, enforce that behavior via types, and see where you went wrong through compiler errors.
- yakshaving_jgt 7y agoThe craziest thing about this is that programmers will often think "well, this tech can't prevent every possible kind of bug, therefore it's useless and we may as well use Python/Ruby/JS/whatever". Programming usually happens in the context of a business, and the technology used has implications in a cost/benefit analysis. Being able to express invariants at the type level is cheaper for a business at scale.
- jstimpfle 7y agoProgrammers who think types let them express their invariants are often ignorant about the fact that expressing those invariants makes their program a mess, so much that they have to consider possibly mutually incompatible language extensions, or reduce modularity of their program to the point where it becomes a pain to compile and becomes hard to maintain, and might require a complete redesign at some point when a minor functional requirement is added... If you consider this huge overhead in development cost, maybe time is better spent in less intrusive ways of improving software reliability.
- marceloabsousa 7y agoSure, but it's about striking a balance between the type (specification) and the program (implementation). The myth mentioned is just something people say to beginners in Haskell but no experienced programmer truly believes - reason being again this balance. When you can express so much in your type system that the implementation can be mostly automated, you have shifted the semantic mess to a level above but have not really made any substantial progress. Still, it's undeniable that type systems are perhaps the only kind of formal methods who really made it to the mainstream software developer because they can be useful. What I find frustrating is that no one is really guiding the programmers in finding good patterns for achieving a healthy balance specially for code that needs to be maintained and adjusted to new use cases.
- jstimpfle 7y agoI'm not sure they have become mainstream. Java and the like have Generics, but I think that's about where "mainstream" ends. (And even Generics can be problematic).
- deschutes 7y agoI think many programmers are skeptical of advanced type systems because the OPs straw man is what gets advertised at the water cooler. I've seen it myself in professional settings. My impression is that advanced type systems interest people because they're cool moreso than because they're practical tools for reducing errors. The kind of discussion I see on this post generally reinforces my impression.
- yakshaving_jgt 7y agoThat hasn't been my experience so far, but I'd be interested to read in more concrete terms exactly what level of type-level invariant expression begins to create overly-rigid software. FWIW, I'm not suggesting moving everything possible into types. I'm suggesting types are better than not having them, just like tests are better than not having them.
- jstimpfle 7y agoA software artifact that has a very specific type usually also needs to be very specific in terms of its required preconditions. Which puts a significant burden on the user of that artifact. And now that user probably requires its own additional preconditions to be able to conform. And so on. I don't know, maybe there is a good way of structuring the software to avoid this effect (I'm not extremely invested in type systems), but maybe it's just a lot of additional pain on top -- too much perceived pain for people who can barely make their software "seems to work".
- beders 7y agoI can confirm this 100%. Having worked at an old (19 years) Java code-base full of unnecessary patterns & abstractions. Even with really great refactoring help from the IDEA, making meaningful changes is very very time consuming. I've spent weeks on it. The complexity was creeping in over the years and is almost impossible to get out again. But it has types!!!11! And if I then look at the actual data transformations behind all this code: It would be a 2 day exercise in Clojure to re-build this from scratch.
- lmm 7y agoJava has probably the most notoriously limited typesystem in actual use. Judging type systems by Java is like judging electric cars by the Sinclair C5. Try an ML-family language sometime.
- ferzul 7y agobut that is not the point of Haskell's type system, since it doesn't even begin to try to reach that goal. firstly, the most available `head` function crashes on half the constructors. more fundamentally, just try using any file or network io method. you just won't have a clue how it can fail, because it isn't even documented. there's many methods where the best you can do is work out what exception is being used to wrap a C errno and read the appropriate Linux man page. at least C documents it's functions that can return errors, and usually encodes them in the type. in Haskell, it's just, "if you're dumb enough to use IO (and what alternative have you got), anything can crash all the time. deal with it". Haskell is great right up to that point, but that's a critical point. (I've tried to find ways to deal with this, but the most people seen to refer too something else when discussing how horrible exceptions are, so I wonder if I'm insane)
- mbrock 7y agoYou might like the paper “Ghosts of Departed Proofs” which shows a great technique for dealing with preconditions in Haskell.
- ferzul 7y agoI'll surely read it, but based on the abstract, it's a design pattern for library writers, not a sanity pattern for library users. it won't let me know how or if the function you wrote will throw an exception, or what kind of exception it will throw, unless it's documented in the type. but my objection is that many times, the possibly of failure is only present in my generic, language/api agnostic knowledge that a file might not be readable or a ship might drop an anchor on a cable. having thought about it, I then have to read the source code to understand what exception might get thrown, so I can prevent my program from crashing. (i would prefer it to continue as best as it can in the case that some api is unavailable, which is obviously a usecase dependent decision)
- mbrock 7y agoMy general approach to programming is that every language at the moment is bad in serious, fatal ways, and that we are all just experimenting and practicing so that 50 years from now we might have a decent approach. Haskell is horrible in some ways, excellent in others, and this paper seems to offer a promising technique.