Re: [Haskell-cafe] Lazy series [was : Preventing sharing]
Sharing a private conversation, with the permission of Jerzy. On Sat, Jan 09, 2016 at 11:45:00AM +0100, Jerzy Karczmarczuk wrote:
Again: *exps = 1 + integral exps*
I said that if RHS exps is evaluated, it cannot work.
But if it evaluates to a thunk ... Then, on which premises you call the language "strict"?
Why not?
A thunk could either be a delayed function call, or it could be a memoised thunk, such as OCaml (a strict language) provides
http://caml.inria.fr/pub/docs/manual-ocaml/libref/Lazy.html [...] But in the original expression with exps, you don't delay anything. You don't construct *exps()*, or equivalent. This variable is just variable, lexical atom, and either you evaluate it or not. If not, don't call the language strict. If there is a delay form introduced by the compiler, the language is not strict.
If you don't agree, I suggest that instead of asking "why this doesn't work, it should!" , simply implement it.
Oleg has already provided most of the solution http://okmij.org/ftp/ML/powser.ml The aim is exps = 1 + integral exps In Oleg's framework the answer is let exps = I.fix (fun e -> int 1 +% integ e) In a hypothetical OCaml with typeclasses, this becomes let exps = I.fix (fun e -> 1 + integ e) The remaining objection is the presence of the fix. The solution here is to allow the language to support recursive bindings of lazy values[1], not just of function values. The we could write let rec exps = 1 + integ exps If you still do not agree I would appreciate it if you could explain why such a language a) could not exist, or b) would not be called "strict" If you're still not convinced, consider a lazy language, Haskell--, which doesn't allow recursive bindings of non-function types. In Haskell-- you *cannot* write exps = 1 + integral exps but you have to write exps = I.fix (\e -> 1 + integral e) So we see that the nice syntax "exps = 1 + integral exps" is not due to laziness (since Haskell-- is lazy, but you cannot write that). Instead the nice syntax is due to lazy recursive bindings, and this sugar can exist as well in a strict language as it can in a lazy one. Tom [1] Note that recursive bindings are anyway just syntactic sugar for a fixed point. The definition sum = \x -> case x of [] -> 0 (x:xs) = x + sum xs is (essentially) sugar for sum = fix (\sum' x -> case x of [] -> 0 (x:xs) = x + sum' xs) so adding additional sugar for binding lazy values can hardly spoil anything.
Tom Ellis wrote :
consider a lazy language, Haskell--,/which doesn't allow recursive bindings of non-function types./ In Haskell-- you *cannot* write
exps = 1 + integral exps
but you have to write
exps = I.fix (\e -> 1 + integral e)
So we see that the nice syntax "exps = 1 + integral exps" is not due to laziness (since Haskell-- is lazy, but you cannot write that). If you say so...
You may always say: "Consider the syntax XXXX. Now, consider a lazy language which doesn't allow XXXX. So, your nice syntax has nothing to do with laziness. QED". Tom, construct such a language, and I might believe you. Also, I recall your former objection, that *exps = 1 + integral exps* should work "for lazy lists" in a strict language. Please, implement it. Since you would need *letrec* anyway, I suggest Scheme (say, Racket). You will see what that implies. Compare the behaviour of strict and lazy Racket. Best regards Jerzy
On Sat, Jan 09, 2016 at 06:29:05PM +0100, Jerzy Karczmarczuk wrote:
Tom Ellis wrote :
consider a lazy language, Haskell--,/which doesn't allow recursive bindings of non-function types./ In Haskell-- you *cannot* write
exps = 1 + integral exps
but you have to write
exps = I.fix (\e -> 1 + integral e)
So we see that the nice syntax "exps = 1 + integral exps" is not due to laziness (since Haskell-- is lazy, but you cannot write that). If you say so...
You may always say:
"Consider the syntax XXXX. Now, consider a lazy language which doesn't allow XXXX. So, your nice syntax has nothing to do with laziness. QED".
Granted, but the more important point was the sketch of the strict language which *does* allow it. You have conveniently failed to challenge me on any of the aspects of the very simple design.
Tom, construct such a language, and I might believe you.
I remind you that Doug's original claim was "this won't work in a strict language", which he offered without proof, even a sketch of a proof. I still hold the onus is on you (or him) to demonstrate it!
Also, I recall your former objection, that
*exps = 1 + integral exps*
should work "for lazy lists" in a strict language. Please, implement it. Since you would need *letrec* anyway, I suggest Scheme (say, Racket). You will see what that implies. Compare the behaviour of strict and lazy Racket.
Maybe since Scheme and Racket are not typed things will go through there. I shall have to look into it. I don't know the languages. Tom
Sorry, forgot to reply to the list. On 01/09/2016 06:36 PM, Tom Ellis wrote:
On Sat, Jan 09, 2016 at 06:29:05PM +0100, Jerzy Karczmarczuk wrote:
Tom Ellis wrote :
consider a lazy language, Haskell--,/which doesn't allow recursive bindings of non-function types./ In Haskell-- you *cannot* write
exps = 1 + integral exps
but you have to write
exps = I.fix (\e -> 1 + integral e)
So we see that the nice syntax "exps = 1 + integral exps" is not due to laziness (since Haskell-- is lazy, but you cannot write that). If you say so...
You may always say:
"Consider the syntax XXXX. Now, consider a lazy language which doesn't allow XXXX. So, your nice syntax has nothing to do with laziness. QED".
Granted, but the more important point was the sketch of the strict language which *does* allow it. You have conveniently failed to challenge me on any of the aspects of the very simple design.
Tom, construct such a language, and I might believe you.
I remind you that Doug's original claim was "this won't work in a strict language", which he offered without proof, even a sketch of a proof. I still hold the onus is on you (or him) to demonstrate it!
If I'm not mistaken, a strict language implies that arguments are evaluated before function calls. To calculate exps, you need to add 1 to the result of the function call integral on argument exps. To evaluate that call, it first evaluates the arguments: exps. And so on... This causes a non-terminating calculation, I would expect. IMHO, unless you add explicit laziness to a strict language, which some do but it requires some extra syntax, this cannot be done. I do believe Scheme or ML does have laziness annotations, and they show in the data types and function call syntax.
Also, I recall your former objection, that
*exps = 1 + integral exps*
should work "for lazy lists" in a strict language. Please, implement it. Since you would need *letrec* anyway, I suggest Scheme (say, Racket). You will see what that implies. Compare the behaviour of strict and lazy Racket.
Maybe since Scheme and Racket are not typed things will go through there. I shall have to look into it. I don't know the languages.
Tom
If you propose that a function (or anything with a function type) is implicitly lazy, then I think that you are describing a lazy/non-strict language. kind regards, Arjen
On Sat, Jan 09, 2016 at 07:04:17PM +0100, Arjen wrote:
If I'm not mistaken, a strict language implies that arguments are evaluated before function calls. To calculate exps, you need to add 1 to the result of the function call integral on argument exps.
Sure, but why should evaluating exps actually do anything? If exps is of function type then evaluating it need not do anything at all!
To evaluate that call, it first evaluates the arguments: exps. And so on... This causes a non-terminating calculation, I would expect.
I disagree, for the reason above.
IMHO, unless you add explicit laziness to a strict language, which some do but it requires some extra syntax, this cannot be done.
You don't even need explicit laziness. Having exps be of function type will do. That means evaluating it will terminate early.
If you propose that a function (or anything with a function type) is implicitly lazy, then I think that you are describing a lazy/non-strict language.
I'm not sure what you're getting at here. I'm not proposing that function application is evaluated lazily, I'm claiming that functions themselves are lazy datatypes since they contain computations that are only run when you applying them to arguments. Tom
On 01/09/2016 07:11 PM, Tom Ellis wrote:
On Sat, Jan 09, 2016 at 07:04:17PM +0100, Arjen wrote:
If I'm not mistaken, a strict language implies that arguments are evaluated before function calls. To calculate exps, you need to add 1 to the result of the function call integral on argument exps.
Sure, but why should evaluating exps actually do anything? If exps is of function type then evaluating it need not do anything at all!
To evaluate that call, it first evaluates the arguments: exps. And so on... This causes a non-terminating calculation, I would expect.
I disagree, for the reason above.
IMHO, unless you add explicit laziness to a strict language, which some do but it requires some extra syntax, this cannot be done.
You don't even need explicit laziness. Having exps be of function type will do. That means evaluating it will terminate early.
If you propose that a function (or anything with a function type) is implicitly lazy, then I think that you are describing a lazy/non-strict language.
I'm not sure what you're getting at here. I'm not proposing that function application is evaluated lazily, I'm claiming that functions themselves are lazy datatypes since they contain computations that are only run when you applying them to arguments.
Tom
I was thinking of exps as a value (having a non-function type). Maybe I'm wrong or just not understanding the issue fully. How do you differentiate between expression that are values and those that are function applications on arguments? If I were to print the value of exps, like main = print exps. How would I express this? Or is it print's responsibility to evaluate the argument? Say, exps has type Integer. How does print differentiate between a actual value (print 42) and unevaluated expressions (print exps)? kind regards, Arjen
On Sat, Jan 09, 2016 at 07:22:48PM +0100, Arjen wrote:
I was thinking of exps as a value (having a non-function type). Maybe I'm wrong or just not understanding the issue fully. How do you differentiate between expression that are values and those that are function applications on arguments?
I'm not sure you really "differentiate" between them. The evaluation of function arguments just has different consequences when those argument values are integers than it does when those argument values are functions.
If I were to print the value of exps, like main = print exps. How would I express this? Or is it print's responsibility to evaluate the argument? Say, exps has type Integer. How does print differentiate between a actual value (print 42) and unevaluated expressions (print exps)?
I'm not quite sure what you're asking, but consider the difference between these two calls to the function id in OCaml. # let id x = x;; val id : 'a -> 'a = <fun> # id (Printf.printf "Hello");; Hello- : unit = () # id (fun () -> Printf.printf "Hello");; - : unit -> unit = <fun> The correspond to the following in an imaginary impure Haskell-like language: id (print "Hello") "Hello" id (\() -> print "Hello") <no output> Tom
On 01/09/2016 07:42 PM, Tom Ellis wrote:
On Sat, Jan 09, 2016 at 07:22:48PM +0100, Arjen wrote:
I was thinking of exps as a value (having a non-function type). Maybe I'm wrong or just not understanding the issue fully. How do you differentiate between expression that are values and those that are function applications on arguments?
I'm not sure you really "differentiate" between them. The evaluation of function arguments just has different consequences when those argument values are integers than it does when those argument values are functions.
If I were to print the value of exps, like main = print exps. How would I express this? Or is it print's responsibility to evaluate the argument? Say, exps has type Integer. How does print differentiate between a actual value (print 42) and unevaluated expressions (print exps)?
I'm not quite sure what you're asking, but consider the difference between these two calls to the function id in OCaml.
# let id x = x;; val id : 'a -> 'a = <fun>
# id (Printf.printf "Hello");; Hello- : unit = ()
# id (fun () -> Printf.printf "Hello");; - : unit -> unit = <fun>
The correspond to the following in an imaginary impure Haskell-like language:
id (print "Hello") "Hello"
id (\() -> print "Hello") <no output>
I think I see what you mean. Then in OCaml exps would have type unit->Int? And to get the value, you would use exps ()? kind regards, Arjen
On Sat, Jan 09, 2016 at 07:48:04PM +0100, Arjen wrote:
I'm not quite sure what you're asking, but consider the difference between these two calls to the function id in OCaml.
# let id x = x;; val id : 'a -> 'a = <fun>
# id (Printf.printf "Hello");; Hello- : unit = ()
# id (fun () -> Printf.printf "Hello");; - : unit -> unit = <fun>
The correspond to the following in an imaginary impure Haskell-like language:
id (print "Hello") "Hello"
id (\() -> print "Hello") <no output>
I think I see what you mean. Then in OCaml exps would have type unit->Int? And to get the value, you would use exps ()?
In OCaml exps could have type A, where A is isomorphic to () -> (Double, A) To get the first value you could (effectively) use 'exps ()'. You get a tail of type A along with it. I suggest you look through Oleg's code. It's quite illuminating. http://okmij.org/ftp/ML/powser.ml Tom
On Sat, Jan 09, 2016 at 06:29:05PM +0100, Jerzy Karczmarczuk wrote:
Tom Ellis wrote :
consider a lazy language, Haskell--,/which doesn't allow recursive bindings of non-function types./ In Haskell-- you *cannot* write
exps = 1 + integral exps
but you have to write
exps = I.fix (\e -> 1 + integral e)
So we see that the nice syntax "exps = 1 + integral exps" is not due to laziness (since Haskell-- is lazy, but you cannot write that).
Tom, construct such a language, and I might believe you.
By the way, for explicitness, here is my construction of such a language. Take any strict language and extend the rules for let rec such that let rec v = ... v ... means let v = fix (\v' -> ... v' ...) for any v that has lazy type (function types, explicit thunks etc.), where fix is its associated fixpoint operator. Then one can happily write let rec exps = 1 + integral exps because it means exactly Oleg's let exps = fix (\e -> 1 + integral e) Do you say (a) this language can't exist for some reason or (b) it is somehow "not strict"? Tom
participants (3)
-
Arjen -
Jerzy Karczmarczuk -
Tom Ellis