On Sat, Mar 21, 2009 at 12:08 PM, Achim Schneider
<barsoap@web.de> 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.)