6 ms·

Rich Hickey once said something (with regards to TDD) like, "We have guard rails on highways, but that doesn't mean we just take our hands off the wheel because

by _bxg1 7y ago

Rich Hickey once said something (with regards to TDD) like, "We have guard rails on highways, but that doesn't mean we just take our hands off the wheel because the rails will keep us on the road. Guard rails don't know where we actually want to go. We drive the car where we're trying to go, and the rails are only there for when things go wrong." I think a version of this applies to static types as well. Even under normal circumstances, I've noticed at times my own thoughts getting lazy when refactoring statically-typed code. I don't "load" as much of the program into my brain as I would otherwise; I just change the part I want to change and then fairly thoughtlessly fix all the type errors. I don't think this is a good thing. The OP takes this to an absolute extreme. Static types are there to document and to catch bugs early; they cannot be used as a complete verification that your code is correct, much less a generative tool for writing logic where "you're not entirely sure how" it works.

jerf 7y ago
"I don't think this is a good thing." How good a thing it is depends on how right you are when you do it. If your language is statically typed, but not very well, then it's a bad thing. But it's not just abstractly a bad thing because you are a lazy person who didn't choose to do useless cognitive work, it's a bad thing because you may be wrong. To give a specific example, if your type system forcibly adjoins NULL to all pointer types, you can't afford to take your hands off the wheel when dealing with pointer types and neglect that case. You must think about it when using pointer types. On the other hand, if you take your hands off the wheel for a moment, but you perform only type system manipulations that you have good and correct reasons to believe won't affect the behavior of the underlying code... then what's wrong with that? I'm guessing you've used the former type of language more than the latter? Me too. I think you've turned the justifiable fear you feel in that sort of language into a heuristic, which makes it easy to then forget the underlying problems. But there's no particular virtue to having to understand more of the program to do a manipulation than having to understand less. Proof: If that was always true, then that recurses on itself until you shouldn't ever make a change until you understand the whole program completely in your head at once (if not the whole system it is running on). Even if that's true, it doesn't matter; we humans don't have the cognitive capacity for that, we must window our understandings. It isn't just the micro task of refactoring one particular function; it's completely common for me to undertake a type-driven refactoring of code where just the type-driven aspects are plenty to fill my cognitive window. Especially since I'm usually in a looser language and I really have to watch those darned forcibly-adjoined NULLs. If I'm somehow "obligated" to understand more, the result isn't that I'm going to have that understanding, the result is that my hand will be tied and I won't be able to do that refactoring because it'll blow out my cognitive budget.
- _bxg1 7y ago
  > we must window our understandings I'm not arguing with that. I'm only saying that we shouldn't assume "the types are enough", so long as we have more "cognitive window" available. Here's why: add :: Integer -> Integer -> Integer add x y = x + y add :: Integer -> Integer -> Integer add x y = x - y The type system doesn't have any idea which of these is correct. So if the programmer is "asleep at the wheel", it's still entirely possible for their logic to come out wrong. All I'm saying is we shouldn't needlessly ignore the actual logic in favor of "letting the compiler write it for us". That's what the OP is expressly advocating for.
  - xfer 7y ago
    That's not what OP is arguing for. Here is the relevant portion that might clear your misconception about this article. > I’m not going to say that blindly filling in type holes always works, but I’d say maybe 95% of the time? It’s truly amazing just how far you can get by writing down the right type and making sure you use every variable. The reason why this works is known as theorems for free, which roughly states that we can infer lots of facts about a type signature (assuming it’s correct.) One of those facts we can infer is often the the only possible implementation. It’s cool as fuck, but you don’t need to understand the paper to use this idea in practice. One question you might have is “what the heck does it mean for a type to be correct?” Good question! It means your type should be as polymorphic as possible.
  - petschge 7y ago
    I am really torn on the subject. I write physics simulations for research use and will therefore assume a FDTD code that simulates Maxwells equations as an example. On one hand there is a bunch of minus signs in Maxwells equations and there is nothing except historical nomenclature and experiments that can tell you where they go. Nothing in the type system can know if dB/dt is curl(E) or -curl(E). (Note that dE/dt has the opposite sign.) And if you implement say a finite difference stencil you have a bunch of numerical coefficients like (1/24, -27/24, 27/24, -1/24) that are not straightforward to derive. If you go to NSFD these coefficients will actually come out of the numerical optimization run by another code. The compiler will never be able to type check that. On the other hand it can be quite useful to have the compiler type check variable for correct SI units, so you don't accidentally add curl(E) to B without multiplying by the time step dt. But that is already quite possible with the type system in C++ that is derived by purists as bad and weak. Maybe it could even add checks that stuff in the new time step has to have a change proportional to dt added to it and prevent me from accessing stuff that is not properly time centered. But then again I have not seen anybody write code like that in Haskell that did anything useful. Having guardrails is nice, but you can not write the entire program in types. And if you try all you get is the same complexity in a unreadable syntax.
agentultra 7y ago
> Static types are there to document and to catch bugs early; they cannot be used as a complete verification that your code is correct, much less a generative tool for writing logic where "you're not entirely sure how" it works. You might be surprised to learn that this is not only possible but something research is definitely working towards. In a language like Agda, for example, when there is enough type information available the compiler can fill in the holes for you with the obviously correct implementation. The idea behind program synthesis drives this even further. Using type level specifications we can automatically derive the programs that meet those specifications. This is useful because the language of types is much more concise than the language of terms. For sufficiently difficult problems it's much easier for humans to reason about complexity in higher-level specifications. Let the computer generate the code! It's still early on for this kind of technology but projects like Synquid[0] are making good headway. Dependent-type theory also forms the basis of interactive theorem proving in Coq and Lean[1]. We use something like holes as the basis of proofs. Haskell's typed holes are quite a bit more loose but to me it feels very similar to working with such a system. I propose to Haskell there there exists an expression that satisfies a particular type and then I use the typed holes to fill in my obligations to provide a proof. The hole is my goal and the available objects in scope are my terms. It is a very effective tool for solving hard problems. [0] https://www.csail.mit.edu/research/synquid-synthesis-liquid-types https://www.csail.mit.edu/research/synquid-synthesis-liquid-... [1] https://leanprover.github.io/ https://leanprover.github.io/ update: Links
- _bxg1 7y ago
  > For sufficiently difficult problems it's much easier for humans to reason about complexity in higher-level specifications. Let the computer generate the code! Yet the humans must still fully consider the higher-level specification. I know that what you describe isn't a compiler per se, but from the perspective of programmer experience it seems analogous. You're not enabling the programmer to "not think", just to think on a more abstracted level. I think the gist of my point still stands; maybe not the final paragraph.
- simiones 7y ago
  I do wonder whether there is any reason to believe that generating code from types would ever be easier than writing the code directly. More specifically, I wonder if this: > This is useful because the language of types is much more concise than the language of terms. actually holds with sufficiently complex types. For example, would the fully-specified type for quicksort actually be shorter than quicksort? I don't know that there is any reason to believe so. The best we may be able to hope for is that we'll have less work to do for formal verification, since instead of writing both the proofs and the code, we may be able to only write the proofs and have the code for free. However, given that writing the proofs is, at least currently, much, much harder than writing just the code, I'm not sure this type of development would make more than a dent in the software engineering world.
ishjoh 7y ago
I'm happy that the static type guard rails exist. I mainly work on e-commerce codebases that have been operating for on average more than 5 years, have had a lot of different developers work on them, and are typically large enough (1 million lines of code or more), that I can't keep it all in my head. For this type of work, it's very nice to have static types, as some of the code has tests, some don't, and at least the static type is a sort of enforced guard rail. Ideally, everything would have tests, and most projects I work on we try to move in that direction with various amounts of success. For me, the most challenging changes can be Javascript changes where there are no tests and no types.
- _bxg1 7y ago
  Nobody is saying that guard-rails in the form of tests or static types aren't a good thing.
brainzap 7y ago
he never played need for speed
nikofeyn 7y ago
your paraphrasing of rich's thoughts seems like he is missing what type driven development is really about, and that is domain driven development. the idea behind letting types lead the way is not to just blindly rely on static types. it's old news that that is only a first approximation to writing good code. what types in sane languages (like f#'s records, discriminated unions, units of measure, classes, functions, etc.) allow is for you to model your domain in a clear way in code such that your programming becomes much more concise and clear as to what it is doing. the fact that static types try to link up everything is a side effect of that process.

by _bxg1 7y ago

jerf 7y ago

"I don't think this is a good thing." How good a thing it is depends on how right you are when you do it. If your language is statically typed, but not very well, then it's a bad thing. But it's not just abstractly a bad thing because you are a lazy person who didn't choose to do useless cognitive work, it's a bad thing because you may be wrong. To give a specific example, if your type system forcibly adjoins NULL to all pointer types, you can't afford to take your hands off the wheel when dealing with pointer types and neglect that case. You must think about it when using pointer types. On the other hand, if you take your hands off the wheel for a moment, but you perform only type system manipulations that you have good and correct reasons to believe won't affect the behavior of the underlying code... then what's wrong with that? I'm guessing you've used the former type of language more than the latter? Me too. I think you've turned the justifiable fear you feel in that sort of language into a heuristic, which makes it easy to then forget the underlying problems. But there's no particular virtue to having to understand more of the program to do a manipulation than having to understand less. Proof: If that was always true, then that recurses on itself until you shouldn't ever make a change until you understand the whole program completely in your head at once (if not the whole system it is running on). Even if that's true, it doesn't matter; we humans don't have the cognitive capacity for that, we must window our understandings. It isn't just the micro task of refactoring one particular function; it's completely common for me to undertake a type-driven refactoring of code where just the type-driven aspects are plenty to fill my cognitive window. Especially since I'm usually in a looser language and I really have to watch those darned forcibly-adjoined NULLs. If I'm somehow "obligated" to understand more, the result isn't that I'm going to have that understanding, the result is that my hand will be tied and I won't be able to do that refactoring because it'll blow out my cognitive budget.

_bxg1 7y ago
> we must window our understandings I'm not arguing with that. I'm only saying that we shouldn't assume "the types are enough", so long as we have more "cognitive window" available. Here's why: add :: Integer -> Integer -> Integer add x y = x + y add :: Integer -> Integer -> Integer add x y = x - y The type system doesn't have any idea which of these is correct. So if the programmer is "asleep at the wheel", it's still entirely possible for their logic to come out wrong. All I'm saying is we shouldn't needlessly ignore the actual logic in favor of "letting the compiler write it for us". That's what the OP is expressly advocating for.
- xfer 7y ago
  That's not what OP is arguing for. Here is the relevant portion that might clear your misconception about this article. > I’m not going to say that blindly filling in type holes always works, but I’d say maybe 95% of the time? It’s truly amazing just how far you can get by writing down the right type and making sure you use every variable. The reason why this works is known as theorems for free, which roughly states that we can infer lots of facts about a type signature (assuming it’s correct.) One of those facts we can infer is often the the only possible implementation. It’s cool as fuck, but you don’t need to understand the paper to use this idea in practice. One question you might have is “what the heck does it mean for a type to be correct?” Good question! It means your type should be as polymorphic as possible.
- petschge 7y ago
  I am really torn on the subject. I write physics simulations for research use and will therefore assume a FDTD code that simulates Maxwells equations as an example. On one hand there is a bunch of minus signs in Maxwells equations and there is nothing except historical nomenclature and experiments that can tell you where they go. Nothing in the type system can know if dB/dt is curl(E) or -curl(E). (Note that dE/dt has the opposite sign.) And if you implement say a finite difference stencil you have a bunch of numerical coefficients like (1/24, -27/24, 27/24, -1/24) that are not straightforward to derive. If you go to NSFD these coefficients will actually come out of the numerical optimization run by another code. The compiler will never be able to type check that. On the other hand it can be quite useful to have the compiler type check variable for correct SI units, so you don't accidentally add curl(E) to B without multiplying by the time step dt. But that is already quite possible with the type system in C++ that is derived by purists as bad and weak. Maybe it could even add checks that stuff in the new time step has to have a change proportional to dt added to it and prevent me from accessing stuff that is not properly time centered. But then again I have not seen anybody write code like that in Haskell that did anything useful. Having guardrails is nice, but you can not write the entire program in types. And if you try all you get is the same complexity in a unreadable syntax.

agentultra 7y ago

> Static types are there to document and to catch bugs early; they cannot be used as a complete verification that your code is correct, much less a generative tool for writing logic where "you're not entirely sure how" it works. You might be surprised to learn that this is not only possible but something research is definitely working towards. In a language like Agda, for example, when there is enough type information available the compiler can fill in the holes for you with the obviously correct implementation. The idea behind program synthesis drives this even further. Using type level specifications we can automatically derive the programs that meet those specifications. This is useful because the language of types is much more concise than the language of terms. For sufficiently difficult problems it's much easier for humans to reason about complexity in higher-level specifications. Let the computer generate the code! It's still early on for this kind of technology but projects like Synquid[0] are making good headway. Dependent-type theory also forms the basis of interactive theorem proving in Coq and Lean[1]. We use something like holes as the basis of proofs. Haskell's typed holes are quite a bit more loose but to me it feels very similar to working with such a system. I propose to Haskell there there exists an expression that satisfies a particular type and then I use the typed holes to fill in my obligations to provide a proof. The hole is my goal and the available objects in scope are my terms. It is a very effective tool for solving hard problems. [0] https://www.csail.mit.edu/research/synquid-synthesis-liquid-types https://www.csail.mit.edu/research/synquid-synthesis-liquid-... [1] https://leanprover.github.io/ https://leanprover.github.io/ update: Links

_bxg1 7y ago
> For sufficiently difficult problems it's much easier for humans to reason about complexity in higher-level specifications. Let the computer generate the code! Yet the humans must still fully consider the higher-level specification. I know that what you describe isn't a compiler per se, but from the perspective of programmer experience it seems analogous. You're not enabling the programmer to "not think", just to think on a more abstracted level. I think the gist of my point still stands; maybe not the final paragraph.
simiones 7y ago
I do wonder whether there is any reason to believe that generating code from types would ever be easier than writing the code directly. More specifically, I wonder if this: > This is useful because the language of types is much more concise than the language of terms. actually holds with sufficiently complex types. For example, would the fully-specified type for quicksort actually be shorter than quicksort? I don't know that there is any reason to believe so. The best we may be able to hope for is that we'll have less work to do for formal verification, since instead of writing both the proofs and the code, we may be able to only write the proofs and have the code for free. However, given that writing the proofs is, at least currently, much, much harder than writing just the code, I'm not sure this type of development would make more than a dent in the software engineering world.

ishjoh 7y ago

I'm happy that the static type guard rails exist. I mainly work on e-commerce codebases that have been operating for on average more than 5 years, have had a lot of different developers work on them, and are typically large enough (1 million lines of code or more), that I can't keep it all in my head. For this type of work, it's very nice to have static types, as some of the code has tests, some don't, and at least the static type is a sort of enforced guard rail. Ideally, everything would have tests, and most projects I work on we try to move in that direction with various amounts of success. For me, the most challenging changes can be Javascript changes where there are no tests and no types.

_bxg1 7y ago
Nobody is saying that guard-rails in the form of tests or static types aren't a good thing.

brainzap 7y ago

he never played need for speed

nikofeyn 7y ago

your paraphrasing of rich's thoughts seems like he is missing what type driven development is really about, and that is domain driven development. the idea behind letting types lead the way is not to just blindly rely on static types. it's old news that that is only a first approximation to writing good code. what types in sane languages (like f#'s records, discriminated unions, units of measure, classes, functions, etc.) allow is for you to model your domain in a clear way in code such that your programming becomes much more concise and clear as to what it is doing. the fact that static types try to link up everything is a side effect of that process.