Specific denotations for pure types
conal at conal.net
Sat Mar 21 15:31:02 EDT 2009
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
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.)
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-prime