3 ms·

I am unsure where the proof, or even supporting argument, would come from for such a statement. The literature is lengthy and deep, but I would sum up the curre

I am unsure where the proof, or even supporting argument, would come from for such a statement. The literature is lengthy and deep, but I would sum up the current understanding and most popular argument against your stated position by citing Robert Harper (who I admit is notoriously anti-Laziness by default) in his commentary to the 2nd Edition to Practical Foundations of Programming Languages: "The problem is the very idea of a lazy language, which imposes a ruinous semantics on types. An eager semantics supports the expected semantics of types (for example, the natural numbers are the natural numbers) and, moreover, admits definition of the lazy forms of these types using suspension types (Chapter 36). A value of a suspension type is either a value of the underlying type, or a computation of such a value that may diverge. There being no representation of the eager types in a lazy language, it follows that, eager languages are strictly more expressive than lazy languages." [1] This paragraph is then followed by a link to Harper's "PCF by Value" supplement/errata to the above referenced PFPL, where such a statement is reinforced. [2] [1] - https://www.cs.cmu.edu/~rwh/pfpl/supplements/commentary.pdf https://www.cs.cmu.edu/~rwh/pfpl/supplements/commentary.pdf [2] - https://www.cs.cmu.edu/~rwh/pfpl/supplements/pcfv.pdf https://www.cs.cmu.edu/~rwh/pfpl/supplements/pcfv.pdf

mrkeen 2y ago
> I am unsure where the proof, or even supporting argument You make a lazy function strict by asking for its output now rather than later. > An eager semantics supports the expected semantics of types (for example, the natural numbers are the natural numbers). What a (counter)example! In lazy semantics the natural numbers are the natural numbers. In eager semantics the natural numbers are stack overflow. > moreover, admits definition of the lazy forms of these types using suspension types This is the required modification that your library maintainer would need to make if he had produced a strict library that you wanted to use lazily. Hence "You cannot ask a strict function to behave lazily." > There being no representation of the eager types in a lazy language Because the lazy representation is the same as the eager representation in the source code. It's up to the caller to demand values now, or later, hence "But you can ask a lazy function to behave strictly."
- eru 2y ago
  > You make a lazy function strict by asking for its output now rather than later. That doesn't mean you can evaluate the function strictly. Have a look at this example: f = head . map (2+) x = f [5, undefined] You can ask for x right away (it's 7), but if you evaluate f strictly, it still diverges. In any case, my suggestion is not to deal with arbitrary functions; but to restrict the set of untagged functions to those where any evaluation order works. 'Works' in the sense that any evaluation order takes a finite amount of time.

mrkeen 2y ago

> I am unsure where the proof, or even supporting argument You make a lazy function strict by asking for its output now rather than later. > An eager semantics supports the expected semantics of types (for example, the natural numbers are the natural numbers). What a (counter)example! In lazy semantics the natural numbers are the natural numbers. In eager semantics the natural numbers are stack overflow. > moreover, admits definition of the lazy forms of these types using suspension types This is the required modification that your library maintainer would need to make if he had produced a strict library that you wanted to use lazily. Hence "You cannot ask a strict function to behave lazily." > There being no representation of the eager types in a lazy language Because the lazy representation is the same as the eager representation in the source code. It's up to the caller to demand values now, or later, hence "But you can ask a lazy function to behave strictly."

eru 2y ago
> You make a lazy function strict by asking for its output now rather than later. That doesn't mean you can evaluate the function strictly. Have a look at this example: f = head . map (2+) x = f [5, undefined] You can ask for x right away (it's 7), but if you evaluate f strictly, it still diverges. In any case, my suggestion is not to deal with arbitrary functions; but to restrict the set of untagged functions to those where any evaluation order works. 'Works' in the sense that any evaluation order takes a finite amount of time.