3 ms·

> 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 versio

> 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?
- tome 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! What makes you think that? Thunking would be monadic (and comonadic) and so there's great hope that it could be syntactically very convenient. We don't complain that typed IO adds hundreds of lexemes to our average Haskell file. > > the type checker still won't distinguish lazy from strict data. > [...] I could do what you're doing in Haskell by compiling every module with STRICT and having manual thunks. You'd still have to read other people's Haskell code where the types don't distinguish between strict and lazy. > > 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. I've never heard of that. How do you get this functionality? > > I've said that, twice: > You didn't actually say that in either of those comments. Yes, that's what CBPV provides.

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?

tome 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! What makes you think that? Thunking would be monadic (and comonadic) and so there's great hope that it could be syntactically very convenient. We don't complain that typed IO adds hundreds of lexemes to our average Haskell file. > > the type checker still won't distinguish lazy from strict data. > [...] I could do what you're doing in Haskell by compiling every module with STRICT and having manual thunks. You'd still have to read other people's Haskell code where the types don't distinguish between strict and lazy. > > 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. I've never heard of that. How do you get this functionality? > > I've said that, twice: > You didn't actually say that in either of those comments. Yes, that's what CBPV provides.