On Tue, Feb 8, 2011 at 7:04 AM, Patrick Browne <patrick.browne@dit.ie> wrote:

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.