referential transparency, definiteness, and unfoldability

From: Sebastian Fischer <>
Date: Thu, 15 Jul 2010 11:30:35 +0200


recently someone in the Haskell Café [1] mentioned a paper I wish I
had been aware of earlier:

     Referential Transparency, Definiteness and Unfoldability
     Harald Søndergaard and Peter Sestoft
     Acta Informatica 27, 505-517 (1990)

Referential transparency means different things to different people
and this paper clarifies the different concepts involved.

Briefly expressed with CRWL notation, the following notions are

1. Referential Transparency.

A language is said to be referentially transparent if for all
expressions e and contexts C

     [| e |] = [| e' |] ==> [| C[e] |] = [| C[e'] |]

The paper defines a more detailed notion based on purely referential
positions in expressions. In CRWL, the above implication follows from
Theorem 1 of [2].

2. Definiteness.

A language is called definite if every variable denotes a single
value. So definiteness means call-time choice.

3. Unfoldability.

Unfoldability means

     f x = e ==> [| f a |] = [| e[a/x] |]

This does not hold in a non-deterministic language with call-time
choice as Wolfgang once pointed out to me [3]. Indeed, the authors of
the mentioned paper argue (on page 514) that "in the presence of non-
determinism one cannot obtain both definiteness and unfoldability".

A lazy deterministic language such as Haskell has all of the above
properties which may explain the confusion when talking about
referential transparency in that context.

Although meanwhile I've had all the mentioned insights, it was a
surprise to see them explained in such an accessible way in a paper
that has been written 20 years ago. I recommend reading it!


[2]: Paco et al. Rewriting and Call-Time choice: The HO case. FLOPS 2008

Underestimating the novelty of the future is a time-honored tradition.
curry mailing list
Received on Do Jul 15 2010 - 11:59:15 CEST

This archive was generated by hypermail 2.3.0 : Di Sep 29 2020 - 07:15:03 CEST