5 ms·

"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 we

by 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.
  - wwright 7y ago

by jerf 7y ago

_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.
- wwright 7y ago