Referential transparency

by Colin Adams (modified: 2007 May 10)

I used to see mention of a keyword "pure", but it didn't make it into either edition of ECMA.

I would have thought that it would be extremely useful to indicate that a function is referentially transparent. Compilers could cache the results. Automatic reasoning tools would benefit. And I would think that the (eventual) verifying compiler would need it.

For instance, how is a verifying compiler supposed to be able to tell that a call to a function to get the time of day is not referentially transparent? I would imagine it is necessary to do so to detect certain logic errors.

Comments

Bertrand Meyer (16 years ago 18/5/2007)
Not a matter of keywords

The keyword is "only".

There is extensive work going on at ETH on this topic. Two somewhat competing approaches are being pursued, one by Bernd Schoeller as part of his thesis, using frame specifications (modifies/uses), the other by me using no language mechanism whatsoever but static analysis. In both cases you will see publications and implementations soon.
- Colin Adams (16 years ago 18/5/2007)
  Thank you. I look forward to seeing the publications.
  
  As for the only keyword, I thought this only listed attributes that were being modified - maybe your plans include extending it to formal arguments? But even so, that only applies to side effects.
  
  So a function like:
```
utc_system_clock: DT_UTC_SYSTEM_CLOCK is
		-- UTC system clock
	once
		create Result.make
	ensure
		utc_system_clock_not_void: Result /= Void
	end
```
  which has no side effects, but is still not referentially transparent isn't really covered.
  
  Personally, I would like to see it become a language rule that all functions must be referentially transparent, but this really needs the compiler to be able to enforce it, and I guess that is quite a fair way off for now. Colin Adams
  - Colin Adams (16 years ago 18/5/2007)
    I shouldn't really submit so late at night
    
    I meant to have added a subsequent call on the object thus: time_now: DT_TIME is -- Current time -- (Create a new time object at each call.) do create Result.make_from_storage (0) set_time_to_now (Result) ensure time_now_not_void: Result /= Void end l_time := utc_system_clock.time_now
    
    There is no side effect, and so nothing to apply the only keyword too, but you cannot substitute l_time wherever you subsequently see utc_system_clock.time_now. Colin Adams
  - Bertrand Meyer (16 years ago 18/5/2007)
    Delicate issue
    
    As a matter of fact, it is easy to ensure the rule at the compiler level. Just prohibit any assignments etc., and recursively any calls to routines not satisfying this property. The problem is to have a practical rule. For example we probably want to accept object creation, which is not really a side effect since it does not modify an existing object. But then the restrictions on the creation procedure are not trivial: we want to allow assignment to fields of the new object, but of that one only.
    
    Also, assignments to secret attributes should be OK in some cases. And what if the class contains some bookkeeping, for example to count the number of calls to a function? This is harmless for the purposes of the function, but it is a side effect. What about a function that causes a side effect and then cancels it (e.g. an implementation of i_th (i) in lists which goes to position i, gets the element, then returns to the original position)? This may be acceptable as essentially pure in some cases, but not in e.g. contracts.
    
    The basic problem in all such cases is not writing the compiler checks but deciding what we want in the first place.
    
    By the way, "only" includes pure as a special case: followed by an empty list.