[Haskell-cafe] Proof that Haskell is RT

[Lennart Augustsson]

Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Since you are talking to the outside world any behaviour is acceptable.
All the weird interactions between getContents and writing the same
file from the same program could, in principle, happen if a different
program wrote the file.
The unsafePerformIO function can break RT, but I think everyone is
aware of that. :)

  -- Lennart

On Wed, Nov 12, 2008 at 6:47 PM, Ryan Ingram <ryani.spam at gmail.com> wrote:
> 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 <andy at nobugs.org> wrote:
>> 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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>