Specific denotations for pure types

[Conal Elliott]

On Sat, Mar 21, 2009 at 12:08 PM, Achim Schneider <barsoap at web.de> wrote:

> Conal Elliott <conal at conal.net> wrote:
>
> > >
> > > yes, but dodgy isn't Bool, it's _a_ Bool.
> >
> >
> > Right.  dodgy is _a_ Bool, and therefore its meaning is an element of
> > the meaning of Bool.  If _any_ element of Bool (e.g. dodgy) has a
> > machine-dependent meaning, then the meaning of Bool itself much have a
> > complex enough structure to contain such an element.
> >
> Then, yes, every Haskell type depends on whatever any type depends on,
> and the only way for the denotations not to explode into one's face is
> to abstract away the fact that an expression forces its context upon
> its continuation. "MachineInfo ->" can be added by the denotation of
> function application, there's no need to have it inside Bool's
> denotation.


Maybe what you're saying is that the meanings of the strictly boolean
building blocks (True, False, &&, ||, not) don't do anything interesting
with machine-info.  They just pass it along in a totally standard way that
can be abstracted out.  If so, I agree.

And still, dodgy does have type Bool, so the meaning of Bool (the
corresponding semantic domain) must have room in it for the meaning of
dodgy, i.e., for machine-dependence (and compiler-dependence).  The
principle I'm assuming is that the meaning of a well-typed expression
inhabits the meaning of the expression's type.  (BTW, this principle
explains what's unsafe about unsafePerformIO.)

  - Conal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-prime/attachments/20090321/a6e4197a/attachment.htm