On Tue, Feb 8, 2011 at 7:04 AM, Patrick Browne
Consider the following definitions: 1. Denotational semantics can be considered as relation between syntax and mathematical objects (the meaning of the syntax). 2. Operational semantics can be considered as set of rules for performing computation.
Question 1 Applying these definitions in a Haskell context can I say that the lambda calculus provides both the operational and denotational semantics for Haskell programs at value level for definition and evaluations.
Sure. There are other, more-or-less equally applicable semantic frameworks. My preferred framework is:
Question 2 Does it make sense to use these definitions at type level? If so, what exactly do they represent?
Under the Howard-Curry Isomorphism, the type level definitions correspond to theorems in a typed logic, and the implementations (the value terms) correspond to proofs of the theorems. I suppose this is more of a "denotational" interpretation. The language of values and terms is more operational. If we really want to try to come up with an operational semantic for types, I suppose we should start with something along the lines of "a type represents an 'abstract set' or a 'category' of values. I suppose some of these are indexed -- like the functorial types [a], Maybe a, etc. It is hard to come up with a single operational semantic for types, because they do so many different things, and there is a semantic for each interpretation.