7 ms·

Your "easy" thunked laziness is horrendous. Not only is it unusably verbose, but it relies on mutable reference updates. Doing this properly is a non-trivial pr

by wyager 10y ago

Your "easy" thunked laziness is horrendous. Not only is it unusably verbose, but it relies on mutable reference updates. Doing this properly is a non-trivial problem that really requires language support. GHC has a whole infrastructure around thunks, sparks, blackholing, etc. It's also much easier to make a strict Haskell data type than it is to do this ML hack you've proposed. You either annotate the module as STRICT or you add a few exclamation marks in the data definition. And again, strict languages don't actually solve the totality problem: def foo(x): y = collatz(x) return y y is not bottom. Great, but you've gained nothing. This computation might still diverge. All you've done is kicked the can a foot to the left. To actually get any interesting benefits of bottom not being a value, you need a totality checker, and at that point you might as well use a lazy language with a totality checker. An actually interesting solution would be to distinguish between data and codata at the type level, which would provide the same compile-time guarantees as explicitly deferring computation without the awful syntactic overhead. It still wouldn't solve atotality, but it would address all your concerns.

catnaroek 10y ago
> Not only is it unusably verbose, It's an (admittedly not thread-safe) implementation in under 30 lines! (I would have bothered providing a thread-safe version if Standard ML had a thread-safe reference cell type. Alas...) In any case, clients don't have to see any of this. All clients have to do is use the functions `pure`, `delay`, `force` and `fix`. > but it relies on mutable reference updates. Well, laziness is mutation. My implementation just exposes that fact. A better criticism is “your implementation doesn't give you polymorphic lazy values, because of ML's value restriction”. > Doing this properly is a non-trivial problem that really requires language support. I don't disagree. I want both strictness and laziness, naturally. But if I'm forced to have only one, it's easier to get the benefits of laziness in a strict language than the other way around. > It's also much easier to make a strict Haskell data type than it is to do this ML hack you've proposed. Even if you use the STRICT pragma, the type checker still won't distinguish lazy from strict data. What happened to “the type checker is your ally”? > And again, strict languages don't actually solve the totality problem: I never said they do. What strictness does is “cordon off” the misbehavior of computations (diverging, raising exceptions, you name it) so that it doesn't infect values. > To actually get any interesting benefits of bottom not being a value, you need a totality checker No, that's unnecessary. One benefit of bottom not being a value is that, for instance, you can prove type class laws by induction on the datatype for which you're providing an instance. (You can do that in Haskell too, if you don't mind being wrong.) Of course, bottom is always a computation, but that's a fact of life in languages with general recursion. > An actually interesting solution would be to distinguish between data and codata at the type level I've said that, twice: https://news.ycombinator.com/item?id=12240669 https://news.ycombinator.com/item?id=12240669, https://news.ycombinator.com/item?id=12240622 https://news.ycombinator.com/item?id=12240622 > It still wouldn't solve atotality, I don't see how the lack of totality is something that needs to be “solved”. General recursion is a good thing a general-purpose language.
- tome 10y ago
  Just so you don't think that the entire Haskell community disapproves of your ideas, let me say that I very much appreciate this kind of programme (as long as you preserve purity!).
  - catnaroek 10y ago
    Oh, sure, effect segregation is a truly great idea, and I want to see more of it, no less.
- wyager 10y ago
  > All clients have to do is use the functions `pure`, `delay`, `force` and `fix`. Oh great, this would only add hundreds of lexemes to your average Haskell file! > Well, laziness is mutation. Reference mutation is a single implementation of lazy semantics. The trick is doing it correctly and efficiently (syntactically and computationally). > My implementation just exposes that fact You say that as if it's a good thing. If I wanted to deal with every detail of the evaluation model, I'd program in assembly. > the type checker still won't distinguish lazy from strict data. Nor does it in your example. In your example, there's only strict data, and you can simulate lazy data with a hack. I agree that the type checker should distinguish between data and codata, but let's not pretend that your example demonstrates that. I could do what you're doing in Haskell by compiling every module with STRICT and having manual thunks. (Note that I don't want to do that.) > What strictness does is “cordon off” the misbehavior of computations That is a fair point. However, this is not really relevant except in debugging, at which point the runtime will tell us which lazy value is diverging anyway. In production, your program is going to spin (or crash) with strict or lazy semantics. > You can do that in Haskell too, if you don't mind being wrong. Or if you don't mind excluding bottom from consideration, which is quite reasonable. That's morally more defensible than pretending you don't have unsafe stateful mutation in languages like ML. > I've said that, twice: You didn't actually say that in either of those comments. > I don't see how the lack of totality is something that needs to be “solved”. You're the one advocating for the compiler telling you when your program is divergent. What better way to do it than proving totality?
  - 10y ago
nickpsecurity 10y ago
"To actually get any interesting benefits of bottom not being a value, you need a totality checker, and at that point you might as well use a lazy language with a totality checker. An actually interesting solution would be to distinguish between data and codata at the type level," I'm as far from specialist and educated on the topic of FP as I could be but still collect info on it for later on (or interested people). This statement jumped out at me as I was trying to find non-Turing complete languages for LANGSEC with one sounding very similar. I'm just curious if your statement applies to it or if my guess was way off for whatever reason. http://pll.cpsc.ucalgary.ca/charity1/www/home.html http://pll.cpsc.ucalgary.ca/charity1/www/home.html https://en.wikipedia.org/wiki/Charity_(programming_language) https://en.wikipedia.org/wiki/Charity_(programming_language) Regardless, this one seemed special versus most projects I've seen. Not like the others. Also uses category theory as OP topic is about. So, I'm keeping it & running it by people just in case there's lasting value worth further investment/exploration.
- catnaroek 10y ago
  Practical programming is all about the effects. Without effects, maybe you can do very good mathematics, but write software you cannot. Unfortunately, effects are quite unwieldy. The difficulty of reasoning about effectful programs grows faster than linearly on the number of effects that can happen in them, because effects interact with each other in all sorts of tricky ways. In the limit, reasoning rigorously about a program in which “anything can happen” is practically impossible. The great insight of functional programming researchers and Haskell programmers is that you can use types to classify programs according to their possible effects, from which it follows that you don't need to worry about any other effects other than those sanctioned by the type. This is the essence of the whole monad business. At this point, I need to introduce a little bit of terminology: (0) A value is something you can bind to a variable. At this point, it doesn't matter whether “bind” means “let binding as in functional languages” or “imperative assignment”. Either works equally well. (1) A computation is what happens when you evaluate an expression or execute a statement. Again, the difference between the functional and imperative versions doesn't really matter. The difference between strict and lazy languages lies in what is considered a value: (0) In strict languages (ML, Lisp, Java, Python, etc.), a value is the result of a finished computation. For instance, in Java, `x = 2 + 2;` means “bind the result of evaluating `2 + 2` to the variable `x`”. (In case pron ever reads this, I'm openly admitting he was right and I was wrong about this, when, in a previous flame war between us, he pointed out that `2 + 2` isn't `4`, but rather the former evaluates to the latter.) As a result, values form a pure sublanguage of any strict language: Since no computation can happen and everything is already its own final result, the statement “all computations are free of side effects, and successfully terminate with a result” is vacuously true. (1) In lazy languages, however, unfinished computations are values in their own right. Compound with the inability of Haskell's type system to distinguish between terminating and non-terminating computations, this means any variable could be bound to a non-terminating computation. Non-termination is an effect (unlike most other effects, often an unwanted one), and this causes technical difficulties, on which I shall not elaborate further, other than to note that these difficulties can be sorted out with a “denotational semantics”, which relies on powerful mathematical tool called “domain theory”. However, instead of learning and using these tools, most Haskellers just pretend the technical difficulties didn't exist in the first place.
dllthomas 10y ago
> Great, but you've gained nothing. This computation might still diverge. All you've done is kicked the can a foot to the left. A foot closer to where the error occurred.

by wyager 10y ago

catnaroek 10y ago

> Not only is it unusably verbose, It's an (admittedly not thread-safe) implementation in under 30 lines! (I would have bothered providing a thread-safe version if Standard ML had a thread-safe reference cell type. Alas...) In any case, clients don't have to see any of this. All clients have to do is use the functions `pure`, `delay`, `force` and `fix`. > but it relies on mutable reference updates. Well, laziness is mutation. My implementation just exposes that fact. A better criticism is “your implementation doesn't give you polymorphic lazy values, because of ML's value restriction”. > Doing this properly is a non-trivial problem that really requires language support. I don't disagree. I want both strictness and laziness, naturally. But if I'm forced to have only one, it's easier to get the benefits of laziness in a strict language than the other way around. > It's also much easier to make a strict Haskell data type than it is to do this ML hack you've proposed. Even if you use the STRICT pragma, the type checker still won't distinguish lazy from strict data. What happened to “the type checker is your ally”? > And again, strict languages don't actually solve the totality problem: I never said they do. What strictness does is “cordon off” the misbehavior of computations (diverging, raising exceptions, you name it) so that it doesn't infect values. > To actually get any interesting benefits of bottom not being a value, you need a totality checker No, that's unnecessary. One benefit of bottom not being a value is that, for instance, you can prove type class laws by induction on the datatype for which you're providing an instance. (You can do that in Haskell too, if you don't mind being wrong.) Of course, bottom is always a computation, but that's a fact of life in languages with general recursion. > An actually interesting solution would be to distinguish between data and codata at the type level I've said that, twice: https://news.ycombinator.com/item?id=12240669 https://news.ycombinator.com/item?id=12240669, https://news.ycombinator.com/item?id=12240622 https://news.ycombinator.com/item?id=12240622 > It still wouldn't solve atotality, I don't see how the lack of totality is something that needs to be “solved”. General recursion is a good thing a general-purpose language.

tome 10y ago
Just so you don't think that the entire Haskell community disapproves of your ideas, let me say that I very much appreciate this kind of programme (as long as you preserve purity!).
- catnaroek 10y ago
  Oh, sure, effect segregation is a truly great idea, and I want to see more of it, no less.
wyager 10y ago
> All clients have to do is use the functions `pure`, `delay`, `force` and `fix`. Oh great, this would only add hundreds of lexemes to your average Haskell file! > Well, laziness is mutation. Reference mutation is a single implementation of lazy semantics. The trick is doing it correctly and efficiently (syntactically and computationally). > My implementation just exposes that fact You say that as if it's a good thing. If I wanted to deal with every detail of the evaluation model, I'd program in assembly. > the type checker still won't distinguish lazy from strict data. Nor does it in your example. In your example, there's only strict data, and you can simulate lazy data with a hack. I agree that the type checker should distinguish between data and codata, but let's not pretend that your example demonstrates that. I could do what you're doing in Haskell by compiling every module with STRICT and having manual thunks. (Note that I don't want to do that.) > What strictness does is “cordon off” the misbehavior of computations That is a fair point. However, this is not really relevant except in debugging, at which point the runtime will tell us which lazy value is diverging anyway. In production, your program is going to spin (or crash) with strict or lazy semantics. > You can do that in Haskell too, if you don't mind being wrong. Or if you don't mind excluding bottom from consideration, which is quite reasonable. That's morally more defensible than pretending you don't have unsafe stateful mutation in languages like ML. > I've said that, twice: You didn't actually say that in either of those comments. > I don't see how the lack of totality is something that needs to be “solved”. You're the one advocating for the compiler telling you when your program is divergent. What better way to do it than proving totality?
- 10y ago

nickpsecurity 10y ago

"To actually get any interesting benefits of bottom not being a value, you need a totality checker, and at that point you might as well use a lazy language with a totality checker. An actually interesting solution would be to distinguish between data and codata at the type level," I'm as far from specialist and educated on the topic of FP as I could be but still collect info on it for later on (or interested people). This statement jumped out at me as I was trying to find non-Turing complete languages for LANGSEC with one sounding very similar. I'm just curious if your statement applies to it or if my guess was way off for whatever reason. http://pll.cpsc.ucalgary.ca/charity1/www/home.html http://pll.cpsc.ucalgary.ca/charity1/www/home.html https://en.wikipedia.org/wiki/Charity_(programming_language) https://en.wikipedia.org/wiki/Charity_(programming_language) Regardless, this one seemed special versus most projects I've seen. Not like the others. Also uses category theory as OP topic is about. So, I'm keeping it & running it by people just in case there's lasting value worth further investment/exploration.

catnaroek 10y ago
Practical programming is all about the effects. Without effects, maybe you can do very good mathematics, but write software you cannot. Unfortunately, effects are quite unwieldy. The difficulty of reasoning about effectful programs grows faster than linearly on the number of effects that can happen in them, because effects interact with each other in all sorts of tricky ways. In the limit, reasoning rigorously about a program in which “anything can happen” is practically impossible. The great insight of functional programming researchers and Haskell programmers is that you can use types to classify programs according to their possible effects, from which it follows that you don't need to worry about any other effects other than those sanctioned by the type. This is the essence of the whole monad business. At this point, I need to introduce a little bit of terminology: (0) A value is something you can bind to a variable. At this point, it doesn't matter whether “bind” means “let binding as in functional languages” or “imperative assignment”. Either works equally well. (1) A computation is what happens when you evaluate an expression or execute a statement. Again, the difference between the functional and imperative versions doesn't really matter. The difference between strict and lazy languages lies in what is considered a value: (0) In strict languages (ML, Lisp, Java, Python, etc.), a value is the result of a finished computation. For instance, in Java, `x = 2 + 2;` means “bind the result of evaluating `2 + 2` to the variable `x`”. (In case pron ever reads this, I'm openly admitting he was right and I was wrong about this, when, in a previous flame war between us, he pointed out that `2 + 2` isn't `4`, but rather the former evaluates to the latter.) As a result, values form a pure sublanguage of any strict language: Since no computation can happen and everything is already its own final result, the statement “all computations are free of side effects, and successfully terminate with a result” is vacuously true. (1) In lazy languages, however, unfinished computations are values in their own right. Compound with the inability of Haskell's type system to distinguish between terminating and non-terminating computations, this means any variable could be bound to a non-terminating computation. Non-termination is an effect (unlike most other effects, often an unwanted one), and this causes technical difficulties, on which I shall not elaborate further, other than to note that these difficulties can be sorted out with a “denotational semantics”, which relies on powerful mathematical tool called “domain theory”. However, instead of learning and using these tools, most Haskellers just pretend the technical difficulties didn't exist in the first place.

dllthomas 10y ago

> Great, but you've gained nothing. This computation might still diverge. All you've done is kicked the can a foot to the left. A foot closer to where the error occurred.