[Haskell-cafe] semantics

[Alexander Solla]

On Tue, Feb 8, 2011 at 7:04 AM, Patrick Browne <patrick.browne at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110208/ce03677b/attachment.htm>