<br><br><div class="gmail_quote">On Tue, Feb 8, 2011 at 7:04 AM, Patrick Browne <span dir="ltr"><<a href="mailto:patrick.browne@dit.ie">patrick.browne@dit.ie</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Consider the following definitions:<br>
1. Denotational semantics can be considered as relation between syntax<br>
and mathematical objects (the meaning of the syntax).<br>
2. Operational semantics can be considered as set of rules for<br>
performing computation.<br>
<br>
Question 1<br>
Applying these definitions in a Haskell context can I say that the<br>
lambda calculus provides both the operational and denotational<br>
semantics for Haskell programs at value level for definition and<br>
evaluations.<br>
<br></blockquote><div><br></div><div>Sure. There are other, more-or-less equally applicable semantic frameworks. My preferred framework is:</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Question 2<br>
Does it make sense to use these definitions at type level? If so, what<br>
exactly do they represent?<br>
<br>
<br></blockquote><div><br></div><div>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. </div>
<div><br></div><div>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.</div>
</div><br>