> So the two conditions
> if a `eq` b then F(a) `eq` F(b)
> if a `req` b then G(a) `req` G(b)
> will only lead to different classes of functions (homomorphisms with
> respect to different properties). The latter will in math more correspond
> to consider all underlying set functions, whereas in the former case one
> restraints at preserving certain semantic structure.
>
> So I think one should not bother too much about breaking referential
> transparency when allowing access to the underlying runtime covers. On the
> contrary, it seems that this exactly what one should expect to happen.
I would not be so gung-ho about breaking referential transparency. While I
agree that it is convenient in specific cases to have a language that
doesn't obey referential transparency, and just use a different, more
specialized theory for reasoning about programs, it seems like that strategy
would force one to deal with either one complex, monolithic theory, or a
multiplicity of similar smaller theories.
The way Haskell employs monads, we can define what amounts to a
domain-specific sublanguage which maybe isn't referentially transparent, and
then translate propositions about programs in the sublanguage into more
familiar propositions about Haskell programs which are referentially
transparent. So Haskell functions as a universal language to express
domain-specific language denotations in. That was the whole point of
introducing monads in the first place, I think: compositional denotational
semantics.
So, why would you want to break referential transparency when you've gone to
all the above trouble to preserve it already?
--FC
