Hi All, In section 4.4.3 "Function and Pattern Bindings" of the Haskell 98 Report, it gives the following translation: ---- (The general binding form of a function is): x p_11 ... p_1k match_1 ... x p_n1 ... p_nk match_n Translation: The general binding form for functions is semantically equivalent to the equation (ie simple pattern binding): x = \x_1 ... x_k -> case (x_1, ..., x_k) of (p_11, ..., p_1k) match_1 ... (p_n1, ..., p_nk) match_n where x_i are new identifiers ---- What does it mean by "semantically equivalent". A rough approximation is "has the same meaning", but that depends on how you define the "meaning". For example: foo x = show x versus foo = \x -> show x I think the answer to the question is something like: this rule is intended to translate Haskell into the kernel, but it is not an equivalence that the programmer may (always) use in their own program (ie it is applicable only after type checking). I'm not sure where this rule fits into the definition of the language. Cheers, Bernie.
Bernard James wrote:
In section 4.4.3 "Function and Pattern Bindings" of the Haskell 98 Report, it gives the following translation:
[ the pattern lambda construction to case expression conversion from the Report]
What does it mean by "semantically equivalent". A rough approximation is "has the same meaning", but that depends on how you define the "meaning".
In the context of code execution, it all boils down to one unique meaning: the result of the execution, i.e., two code fragments inflicting the same environmental (informally "identifier -> variable -> value" mapping and I/O) change are considered semantically equivalent. This is called "operational semantics". One of the (many) advantages of Haskell, being a purely declarative language, is that one can use a more tractable approach: constructs are operationally equivalent if and only if they are substitutable (after proper renaming of variables to avoid incidental name clashes), and can even use a simple calculus in the kernel language (after the compilation you mentioned).
For example:
foo x = show x versus foo = \x -> show x
And, why not the simplest version: "foo = show"... If we call these three versions "foo1", "foo2" and "foo3", then they are semantically equivalent because, besides having the same type, one can substitute one with anyone of the others; if we have the definition g = foo1 "Hello" we can replace "foo1" with either "foo2" or "foo3" and get the exact same behavior (or operational semantics, if you prefer): g = foo2 "Hello"
I think the answer to the question is something like: this rule is intended to translate Haskell into the kernel, but it is not an equivalence that the programmer may (always) use in their own program (ie it is applicable only after type checking).
Semantic equivalence does not necessitate syntactical equivalence (although the opposite implication trivially holds...), if that was your worry. And, no, the programmers need not to worry about this equivalence in most cases, since the transformation is done for us by our friendly Haskell compiler/interpreter. Actually, the Haskell compiler/interpreter does not need to do the conversion at all, as long as the behavior is AS IF the conversion has been done. There are often more efficient ways to do things than to translate into the Haskell kernel language. Semantics (almost) always ignore efficiency issues :-)
I'm not sure where this rule fits into the definition of the language.
And I am not sure I understood your worries, so forgive me if my explanation was out-of-bounds, or trivial. Regards, David
For example:
foo x = show x versus foo = \x -> show x
And, why not the simplest version: "foo = show"...
If we call these three versions "foo1", "foo2" and "foo3", then they are semantically equivalent because, besides having the same type, one can substitute one with anyone of the others; if we have the definition
g = foo1 "Hello"
we can replace "foo1" with either "foo2" or "foo3" and get the exact same behavior (or operational semantics, if you prefer):
g = foo2 "Hello"
Thanks for your helpful comments David, I should have mentioned why I picked this example. In the absence of a suitable type signature, foo2 and foo3 won't pass the monomorphism restriction. So I can't freely apply the rule to my program as a transformation from Haskell to Haskell and always preserve the static properties of my program. However, you have answered my question, in that the semantics that the rule is talking about is the operational semantics. Cheers, Bernie.
participants (2)
-
Bernard James POPE -
David Bergman