Why is getArgs in the IO monad?
See subject. It seems that it would be constant through execution, and so could be just [String]. Jim
It's not a constant; see, for example, System.Environment.withArgs (http://www.haskell.org/ghc/docs/latest/html/libraries/base/System.Environmen...). Abe On Mon, 17 Jan 2005 16:23:17 -0500, Jim Apple <japple@freeshell.org> wrote:
See subject. It seems that it would be constant through execution, and so could be just [String].
Jim
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
How about a semantic answer instead of an operational one? If getArgs had type [String], then its denotation must be a (lazy) list of (lazy) sequences of characters (extended by bottom). For instance, the expression (words "hello world") denotes the list ["hello","world"]. What list would "getArgs" denote? - Conal -----Original Message----- From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Abraham Egnor Sent: Monday, January 17, 2005 1:31 PM To: Jim Apple Cc: haskell@haskell.org Subject: Re: [Haskell] Why is getArgs in the IO monad? It's not a constant; see, for example, System.Environment.withArgs (http://www.haskell.org/ghc/docs/latest/html/libraries/base/System.Envir onment.html#v%3AwithArgs). Abe On Mon, 17 Jan 2005 16:23:17 -0500, Jim Apple <japple@freeshell.org> wrote:
See subject. It seems that it would be constant through execution, and so could be just [String].
Jim
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Conal Elliott wrote:
If getArgs had type [String], then its denotation must be a (lazy) list of (lazy) sequences of characters (extended by bottom). For instance, the expression (words "hello world") denotes the list ["hello","world"]. What list would "getArgs" denote?
I don't think I understand your (rhetorical) question. It seems that, looking out at the world from main, the args passed to main and the compilation happen at the same time (before, long long ago). What motivation would we have for treating them differently? Jim
Hi Jim. If I understand you, you're asking for an operational answer to your original "why" -- this time bringing in the operational issues of compile and run times. I'm suggesting you might better understand the why of Haskell if you think denotationally (here about the meaning of the [String] type), rather than operationally. As a simpler example (type-wise), if "getArgs" were to have type [String], then "length getArgs" would have type Int. The meaning of "length getArgs" would then have to be a value whose type is the meaning of Haskell's "Int", i.e. either bottom or a 32-bit integer. I'm guessing that none of those 2^32+1 values is what you'd mean by "length getArgs". On the other hand, the IO monad is a much roomier type. HTH, - Conal -----Original Message----- From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Jim Apple Sent: Monday, January 17, 2005 10:28 PM To: haskell@haskell.org Subject: [Haskell] Re: Why is getArgs in the IO monad? Conal Elliott wrote:
If getArgs had type [String], then its denotation must be a (lazy) list of (lazy) sequences of characters (extended by bottom). For instance, the expression (words "hello world") denotes the list ["hello","world"]. What list would "getArgs" denote?
I don't think I understand your (rhetorical) question. It seems that, looking out at the world from main, the args passed to main and the compilation happen at the same time (before, long long ago). What motivation would we have for treating them differently? Jim _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
I still think I'm missing your point, but let me take a stab at it. Conal Elliott wrote:
I'm suggesting you might better understand the why of Haskell if you think denotationally (here about the meaning of the [String] type), rather than operationally.
The meaning of a type seems to be about what happens operationally. ":: [String]" is an operational guarantee, so if we let "getArgs :: [String]" that is a promise that there is some list of Strings at runtime.
I'm guessing that none of those 2^32+1 values is what you'd mean by "length getArgs".
Well, I suppose I mean something like an existential type: there is some Int that is length getArgs. Even if this is denotationally different from a value like zero :: Int, I think it is also different from getLine :: IO String. It seems to mean something between these. I suppose my intuition is that it is closer to :: Int Jim
Jim Apple wrote:
Even if this is denotationally different from a value like zero :: Int, I think it is also different from getLine :: IO String. It seems to mean something between these.
I think I understand your point better now: Do you want another denotational distinction, somewhere between the semantic simplicity of Int or [String] and the semantically intractable kitchen-sink IO? I'd like to see more exploration in that in-between space. Cheers, - Conal -----Original Message----- From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Jim Apple Sent: Tuesday, January 18, 2005 12:15 AM To: haskell@haskell.org Subject: [Haskell] Re: Why is getArgs in the IO monad? I still think I'm missing your point, but let me take a stab at it. Conal Elliott wrote:
I'm suggesting you might better understand the why of Haskell if you think denotationally (here about the meaning of the [String] type), rather than operationally.
The meaning of a type seems to be about what happens operationally. ":: [String]" is an operational guarantee, so if we let "getArgs :: [String]" that is a promise that there is some list of Strings at runtime.
I'm guessing that none of those 2^32+1 values is what you'd mean by "length getArgs".
Well, I suppose I mean something like an existential type: there is some Int that is length getArgs. Even if this is denotationally different from a value like zero :: Int, I think it is also different from getLine :: IO String. It seems to mean something between these. I suppose my intuition is that it is closer to :: Int Jim _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Conal Elliott wrote:
The meaning of "length getArgs" would then have to be a value whose type is the meaning of Haskell's "Int", i.e. either bottom or a 32-bit integer. I'm guessing that none of those 2^32+1 values is what you'd mean by "length getArgs". On the other hand, the IO monad is a much roomier type.
I'm not strongly convinced by this argument. I don't think you can tell me which particular Char value you mean by the expression (maxBound :: Char) either, yet you probably wouldn't argue for changing maxBound's type. I think Jim's claim is that there's no clear dividing line between these cases, and I tend to agree. Even if you want to disallow explicit recompilation (and how do you define "compilation" denotationally?), an automatic rollout of a new version of Hugs could lead to successive invocations of a script using different values of (maxBound :: Char) (or, more plausibly, some constant defined in the library) without user intervention. How is this different from any other environmental change, such as a change in the program arguments? I think this is what Jim meant when he wrote
It seems that, looking out at the world from main, the args passed to main and the compilation happen at the same time (before, long long ago). What motivation would we have for treating them differently?
-- Ben
On Tue, Jan 18, 2005 at 08:12:42AM -0800, Ben Rudiak-Gould wrote:
Even if you want to disallow explicit recompilation (and how do you define "compilation" denotationally?), an automatic rollout of a new version of Hugs could lead to successive invocations of a script using different values of (maxBound :: Char) (or, more plausibly, some constant defined in the library) without user intervention. How is this different from any other environmental change, such as a change in the program arguments?
Big difference. The change in program arguments is inevitable, or at least expected. The change in Haskell implementation can be avoided, by compiling the program or simply by not switching to a newer version. The more there are pure values that change from execution to execution, the more often will smart libraries like WASH/CGI break in mysterious ways. Please, no! Best regards, Tomasz
Surely both requirements can be satisfied if the programs arguments are made parameters of main: main :: [String] -> IO () Keean. Ben Rudiak-Gould wrote:
Conal Elliott wrote:
The meaning of "length getArgs" would then have to be a value whose type is the meaning of Haskell's "Int", i.e. either bottom or a 32-bit integer. I'm guessing that none of those 2^32+1 values is what you'd mean by "length getArgs". On the other hand, the IO monad is a much roomier type.
Ben Rudiak-Gould <Benjamin.Rudiak-Gould@cl.cam.ac.uk> writes:
How is this different from any other environmental change, such as a change in the program arguments?
Isn't this really the old (or fairly recent) discussion of "top level things with identity"? Should one be able to do something like args :: [String] args <- getArgs at the top level? -kzm -- If I haven't seen further, it is by standing in the footprints of giants
On 18 Jan 2005, at 16:12, Ben Rudiak-Gould wrote:
I'm not strongly convinced by this argument. I don't think you can tell me which particular Char value you mean by the expression (maxBound :: Char) either, yet you probably wouldn't argue for changing maxBound's type. I think Jim's claim is that there's no clear dividing line between these cases, and I tend to agree. Even if you want to disallow explicit recompilation (and how do you define "compilation" denotationally?), an automatic rollout of a new version of Hugs could lead to successive invocations of a script using different values of (maxBound :: Char) (or, more plausibly, some constant defined in the library) without user intervention. How is this different from any other environmental change, such as a change in the program arguments? I think this is what Jim meant when he wrote
Library constants which change between runs are evil. As a comparison note that the common Java and C and C++ compilers will all happily inline library constants at compile time, so they also would suffer brokenness if a library constant wasn't constant between runs. Jules
Oh! I hope that Haskell language and library semantics are defined independently from any particular Haskell implementation. - Conal -----Original Message----- From: br276@hermes.cam.ac.uk [mailto:br276@hermes.cam.ac.uk] On Behalf Of Ben Rudiak-Gould Sent: Tuesday, January 18, 2005 8:13 AM To: Conal Elliott Cc: 'Jim Apple'; haskell@haskell.org Subject: Re: [Haskell] Re: Why is getArgs in the IO monad? Conal Elliott wrote:
The meaning of "length getArgs" would then have to be a value whose type is the meaning of Haskell's "Int", i.e. either bottom or a 32-bit integer. I'm guessing that none of those 2^32+1 values is what you'd mean by "length getArgs". On the other hand, the IO monad is a much roomier type.
I'm not strongly convinced by this argument. I don't think you can tell me which particular Char value you mean by the expression (maxBound :: Char) either, yet you probably wouldn't argue for changing maxBound's type. I think Jim's claim is that there's no clear dividing line between these cases, and I tend to agree. Even if you want to disallow explicit recompilation (and how do you define "compilation" denotationally?), an automatic rollout of a new version of Hugs could lead to successive invocations of a script using different values of (maxBound :: Char) (or, more plausibly, some constant defined in the library) without user intervention. How is this different from any other environmental change, such as a change in the program arguments? I think this is what Jim meant when he wrote
It seems that, looking out at the world from main, the args passed to main and the compilation happen at the same time (before, long long ago). What motivation would we have for treating them differently?
-- Ben
On Mon, Jan 17, 2005 at 04:23:17PM -0500, Jim Apple wrote:
See subject. It seems that it would be constant through execution, and so could be just [String].
I like to think that pure functions don't change between executions. getArgs :: [String] would certainly break that. Best regards, Tomasz
On Tue, Jan 18, 2005 at 01:31:19AM -0500, Jim Apple wrote:
Tomasz Zielonka wrote:
I like to think that pure functions don't change between executions.
I'd like to think they wouldn't change within executions. Is there a pure haskell way to check the value of a function between exections?
Perhaps I was unclear. I want pure functions to give the same results every time they are run for the same arguments, as long as the have the same definition. This makes like easier. Also, some haskell libraries rely on that - take WASH/CGI for example. Best regards, Tomasz
On 18 Jan 2005, at 06:31, Jim Apple wrote:
Tomasz Zielonka wrote:
I like to think that pure functions don't change between executions.
I'd like to think they wouldn't change within executions. Is there a pure haskell way to check the value of a function between exections?
In principle, a haskell compiler might notice that a function is always called with a particular argument, and inline the result of the function at compile-time. For example, you might well expect a program containing the subterm "3+4" to be compiled into machine code which directly uses the constant value 7. Certainly most decent C compilers will perform this optimisation. Such an optimisation, depends on the knowledge that "3+4" is always the same value: i.e. that a pure function, given the same arguments, always returns the same value (even between executions). More sophisticated optimisation transforms might also depend on the same property. Whether GHC actually performs an optimisation along these lines I have no idea. Jules
participants (8)
-
Abraham Egnor -
Ben Rudiak-Gould -
Conal Elliott -
Jim Apple -
Jules Bean -
Keean Schupke -
Ketil Malde -
Tomasz Zielonka