3 ms·

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

by 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.
catnaroek 10y ago
> Oh great, this would only add hundreds of lexemes to your average Haskell file! I'd rather only use laziness when it's absolutely necessary. > Reference mutation is a single implementation of lazy semantics. The only way you can avoid mutation in an implementation of laziness is to use a key-value container that maps thunk IDs to their respective contents. This imposes an extra cost, logarithmic in the number of thunks in your computation. I don't think you'd like this implementation. I'm aware that my implementation has deficiencies, e.g., it isn't thread-safe, and it doesn't support polymorphic lazy values. And, of course, because the compiler isn't aware of what I'm doing, I don't get benefits that Haskellers take for granted, like stream fusion and whatnot. But my implementation does capture the essence of laziness: computing an expression when you first need its result, and memoizing this result to avoid recomputing it again. > 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. I don't think you can meaningfully abstract the evaluation strategy in a general-purpose programming language. Note that having the Church-Rosser property isn't enough: It says absolutely nothing about the impact of picking this or that reduction strategy on the cost of a computation. Programmers care about that too. > Nor does it in your example. (...) let's not pretend that your example demonstrates that. It does. The types `foo` and `foo lazy` are very different, and ML's type checker will let you know if you wrongly conflate them. > pretending you don't have unsafe stateful mutation in languages like ML. Using reference cells in ML is perfectly safe as long as your program is single-threaded. It's unsafe in a multi-threaded context, but the same is true of Haskell's `IORef`. And I don't pretend that there's no mutation in ML. I'm perfectly aware that ML isn't a pure language, and every expression is potentially effectful unless proven otherwise. Just like every Haskell expression is potentially nonproductive unless proven otherwise. > You didn't actually say that in either of those comments. I did. Call-by-push-value distinguishes between value types (sums, tensor products) and computation types (categorical products, functions), which live in two different categories, related by a pair of adjoint functors. The composition of these adjoint functors is precisely the usual monad for whatever kind of effects your computations might have. (Corollary: if your computations are pure, the adjunction is actually an equivalence of categories. It becomes patently clear that nontermination is an effect!) All of this is explained in the papers ( http://www.cs.bham.ac.uk/~pbl/papers/ http://www.cs.bham.ac.uk/~pbl/papers/ ), so I didn't feel a need to repeat it here. > You're the one advocating for the compiler telling you when your program is divergent. When did I say that? What I actually said is “using a strict language prevents computational effects from infecting values”. Laziness pushes nontermination far away from its source, just like dynamic typing pushes type errors far away from their source. Of course, both laziness and dynamic typing have their place - it just isn't “everywhere in the program”.

by wyager 10y ago

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.

catnaroek 10y ago

> Oh great, this would only add hundreds of lexemes to your average Haskell file! I'd rather only use laziness when it's absolutely necessary. > Reference mutation is a single implementation of lazy semantics. The only way you can avoid mutation in an implementation of laziness is to use a key-value container that maps thunk IDs to their respective contents. This imposes an extra cost, logarithmic in the number of thunks in your computation. I don't think you'd like this implementation. I'm aware that my implementation has deficiencies, e.g., it isn't thread-safe, and it doesn't support polymorphic lazy values. And, of course, because the compiler isn't aware of what I'm doing, I don't get benefits that Haskellers take for granted, like stream fusion and whatnot. But my implementation does capture the essence of laziness: computing an expression when you first need its result, and memoizing this result to avoid recomputing it again. > 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. I don't think you can meaningfully abstract the evaluation strategy in a general-purpose programming language. Note that having the Church-Rosser property isn't enough: It says absolutely nothing about the impact of picking this or that reduction strategy on the cost of a computation. Programmers care about that too. > Nor does it in your example. (...) let's not pretend that your example demonstrates that. It does. The types `foo` and `foo lazy` are very different, and ML's type checker will let you know if you wrongly conflate them. > pretending you don't have unsafe stateful mutation in languages like ML. Using reference cells in ML is perfectly safe as long as your program is single-threaded. It's unsafe in a multi-threaded context, but the same is true of Haskell's `IORef`. And I don't pretend that there's no mutation in ML. I'm perfectly aware that ML isn't a pure language, and every expression is potentially effectful unless proven otherwise. Just like every Haskell expression is potentially nonproductive unless proven otherwise. > You didn't actually say that in either of those comments. I did. Call-by-push-value distinguishes between value types (sums, tensor products) and computation types (categorical products, functions), which live in two different categories, related by a pair of adjoint functors. The composition of these adjoint functors is precisely the usual monad for whatever kind of effects your computations might have. (Corollary: if your computations are pure, the adjunction is actually an equivalence of categories. It becomes patently clear that nontermination is an effect!) All of this is explained in the papers ( http://www.cs.bham.ac.uk/~pbl/papers/ http://www.cs.bham.ac.uk/~pbl/papers/ ), so I didn't feel a need to repeat it here. > You're the one advocating for the compiler telling you when your program is divergent. When did I say that? What I actually said is “using a strict language prevents computational effects from infecting values”. Laziness pushes nontermination far away from its source, just like dynamic typing pushes type errors far away from their source. Of course, both laziness and dynamic typing have their place - it just isn't “everywhere in the program”.