[Haskell-cafe] Linking and unsafePerformIO

[Jonathan Cast]

On Tue, 2008-10-14 at 12:31 -0400, David Roundy wrote:
> On Tue, Oct 14, 2008 at 05:20:35PM +0100, Jules Bean wrote:
> > David Roundy wrote:
> >> On Tue, Oct 14, 2008 at 04:05:23PM +0100, Jules Bean wrote:
> >>> Constants are mathematical and universal, like pi. That is what the
> >>> semantics of haskell say.
> >>
> >> Where do the semantics of haskell say this? 
> >
> > You should better ask 'which semantics?'.
> >
> > The semantics in which a value of type "Int -> Int" is denoted by a
> > mathematical function from Int to Int. In that semantics a value of
> > type "Int" denotes a specific Int.  And that denotation is, of
> > course, entirely independent of compiler or OS or package or dynamic
> > loading or any concern like that.
> >
> > This is, to my mind the "often assumed but never written down"
> > semantics of haskell. It's certainly the semantics *I* want haskell
> > to have.
> >
> > > How does it interact with fixing bugs (which means changing
> > > mathematical and universal constant functions--since all functions
> > > are constants)?
> >
> > That's fine. Changing a program changes it denotation.
> >
> > Running a program on a different interpreter or compiler had better
> > not change its denotation, otherwise it [the denotation] is not much
> > use as a basis for reasoning.
> 
> But you're saying above that we can't change programs, right? You
> probably won't be surprised to hear that different compilers are
> different programs.

This `problem' is already solved by the theory of logical relations.

jcc