5 ms·

The problem isn't the bottom type. The problem is that, in a lazy language, bottom is a value. And this is by no means practical. It's a pain.

wyager 10y ago
So you either have bottom as a value or you spin forever because your function that strictly produces a non-bottom value never terminates. Why is the latter preferable? Seems worse to me, since functions that are non-strict on the bottom value will still terminate.
- catnaroek 10y ago
  In a strict language, bottom isn't a part of the domain of any function to begin with, because bottom isn't a value. Functions map values to computations (in call-by-push-value), and then we classify computations by the type of their possible return value (in call-by-value). In any case, if you want to recover the benefits of laziness in a strict language, it's easy: just explicitly thunk computations. Here's how to do it in Standard ML: datatype 'a cell = Pure of 'a | Except of exn | Delay of unit -> 'a type 'a lazy = 'a cell ref fun pure x = ref (Pure x) fun delay f x = ref (Delay (fn _ => f x)) fun compute f = Pure (f ()) handle e => Except e fun force r = case !r of Pure x => x | Except e => raise e | Delay f => (r := compute f; force r) You can also provide a means to tie lazy (co)fixpoints: exception Diverge fun fix f = let val r = ref (Except Diverge) in r := compute (fn _ => f r); force r end The type checker will tell you in very clear terms the difference between `foo` (a value) and `foo lazy` (a thunked computation), in case you forget. On the other hand, recovering the benefits of strictness in a lazy language is much harder, less intuitive, and you don't get help from the type checker.
  - 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!).

wyager 10y ago

So you either have bottom as a value or you spin forever because your function that strictly produces a non-bottom value never terminates. Why is the latter preferable? Seems worse to me, since functions that are non-strict on the bottom value will still terminate.

catnaroek 10y ago
In a strict language, bottom isn't a part of the domain of any function to begin with, because bottom isn't a value. Functions map values to computations (in call-by-push-value), and then we classify computations by the type of their possible return value (in call-by-value). In any case, if you want to recover the benefits of laziness in a strict language, it's easy: just explicitly thunk computations. Here's how to do it in Standard ML: datatype 'a cell = Pure of 'a | Except of exn | Delay of unit -> 'a type 'a lazy = 'a cell ref fun pure x = ref (Pure x) fun delay f x = ref (Delay (fn _ => f x)) fun compute f = Pure (f ()) handle e => Except e fun force r = case !r of Pure x => x | Except e => raise e | Delay f => (r := compute f; force r) You can also provide a means to tie lazy (co)fixpoints: exception Diverge fun fix f = let val r = ref (Except Diverge) in r := compute (fn _ => f r); force r end The type checker will tell you in very clear terms the difference between `foo` (a value) and `foo lazy` (a thunked computation), in case you forget. On the other hand, recovering the benefits of strictness in a lazy language is much harder, less intuitive, and you don't get help from the type checker.
- 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!).