3 ms·

Some of the type-machinery code (hint, it has words like "hoist" or "lift" that describe type operations, not data operations) is like that, and its really not

Some of the type-machinery code (hint, it has words like "hoist" or "lift" that describe type operations, not data operations) is like that, and its really not a problem because it does the only thing it can do given the types, and the things it does have nothing to do with your business domain or I/O so its never going to change unless a library you are using changes. When that happens its annoying but you just play type tetris again until the red squiggly lines go away and then you are fine for another few years. It isn't something I'd really brag about though as its really hard to explain the benefits of this stuff to non-Haskellers and you can end up wasting infinite amounts of time polishing these abstractions instead of getting work done.

jrochkind1 7y ago
> because it does the only thing it can do given the types Okay, this may be (probably is) a stupid question, because I know no Haskell whatsoever, but... if there's really only one thing it can do given the types, why does the code have to be there at all? Why can't you just write "Do the only thing you can do given these types"? If it's code humans aren't meant to read anyway, and it really is the only thing that could be done... why can't the compiler just do it without you having to put the non-human-intelligible code in your source files?
- syrak 7y ago
  This is an interesting question. Technically there is more than one possible implementation, but you would also have to go out of your way to get it wrong. Automatically determining what constitutes "going out of your way" so that the code can be generated automatically is an active area of research (program synthesis), but as this post already shows, for "simple" cases, we're getting pretty close. As the post mentions, there are certain dead giveaways of an incorrect implementation, such as unused variables. Conversely one may still have some rough idea of the desired code to guide the implementation. The point is not about entirely removing one's mind from the process, but to allow oneself to only think about the choices that matter, which are few. Alternatively, another way to look at the problem is that these types, while already being quite precise, are still not as precise as they could be, because the type system is not sufficiently expressive. And even with the ability to describe the desired properties to uniquely determine the implementation: - it may not be obvious that the implementation is in fact uniquely determined; - a solution, unique or not, may not be easy to find automatically. Program synthesis is essentially the same problem as proof search (c.f. Curry-Howard correspondence); knowing that there is a proof of Fermat's last theorem is not sufficient to construct an actual proof of it from scratch. For these reasons, it may still be desirable to nail down the implementation explicitly even if it is hard to read. It's also worth considering the fact that polysemy (the package that the controversial snippet at the beginning of the post comes from) is very much an implementation of a state-of-the-art effect system using state-of-the-art features of Haskell's type system, so it can be expected that the abstractions to make this code more digestible (for the right audience) are still missing, because no one has ever thought of how to express them yet.

jrochkind1 7y ago

> because it does the only thing it can do given the types Okay, this may be (probably is) a stupid question, because I know no Haskell whatsoever, but... if there's really only one thing it can do given the types, why does the code have to be there at all? Why can't you just write "Do the only thing you can do given these types"? If it's code humans aren't meant to read anyway, and it really is the only thing that could be done... why can't the compiler just do it without you having to put the non-human-intelligible code in your source files?

syrak 7y ago
This is an interesting question. Technically there is more than one possible implementation, but you would also have to go out of your way to get it wrong. Automatically determining what constitutes "going out of your way" so that the code can be generated automatically is an active area of research (program synthesis), but as this post already shows, for "simple" cases, we're getting pretty close. As the post mentions, there are certain dead giveaways of an incorrect implementation, such as unused variables. Conversely one may still have some rough idea of the desired code to guide the implementation. The point is not about entirely removing one's mind from the process, but to allow oneself to only think about the choices that matter, which are few. Alternatively, another way to look at the problem is that these types, while already being quite precise, are still not as precise as they could be, because the type system is not sufficiently expressive. And even with the ability to describe the desired properties to uniquely determine the implementation: - it may not be obvious that the implementation is in fact uniquely determined; - a solution, unique or not, may not be easy to find automatically. Program synthesis is essentially the same problem as proof search (c.f. Curry-Howard correspondence); knowing that there is a proof of Fermat's last theorem is not sufficient to construct an actual proof of it from scratch. For these reasons, it may still be desirable to nail down the implementation explicitly even if it is hard to read. It's also worth considering the fact that polysemy (the package that the controversial snippet at the beginning of the post comes from) is very much an implementation of a state-of-the-art effect system using state-of-the-art features of Haskell's type system, so it can be expected that the abstractions to make this code more digestible (for the right audience) are still missing, because no one has ever thought of how to express them yet.