On a totally non-theory side, Haskell isn't referentially transparent.
In particular, any code that calls unsafePerformIO or
unsafeInterleaveIO is not necessarily RT. Given that getContents and
interact use unsafeInterleaveIO, this includes most toy programs as
well as almost every non-toy program; almost all use unsafePerformIO
intentionally.
That said, the situations in which these functions are RT are not that
hard to meet, but they would muddy up any formal proof significantly.
Personally, I'm happy with the hand-wavy proof that goes like this:
1) "pure" functions don't have side effects.
2) side-effect free functions can be duplicated or shared without
affecting the results of the program that uses them (in the absence of
considerations of resource limitation like running out of memory)
3) any function that only uses other pure functions is pure
4) all Haskell98 functions that don't use unsafe* are pure
5) therefore Haskell98 minus unsafe functions is referentially transparent.
Note that I am including I/O actions as "pure" when observed as the
GHC implementation of IO a ~~ World -> (World, a); the function result
that is the value of "main" is pure. It is only the observation of
that function by the runtime that causes side effects.
-- ryan
On Wed, Nov 12, 2008 at 2:11 AM, Andrew Birkett
Hi,
Is a formal proof that the Haskell language is referentially transparent? Many people state "haskell is RT" without backing up that claim. I know that, in practice, I can't write any counter-examples but that's a bit handy-wavy. Is there a formal proof that, for all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program?
(I was writing a blog post about the origins of the phrase 'referentially transparent' and it made me think about this)
Andrew
-- - http://www.nobugs.org - _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe