the un i blog
Table of Contents
1. Referential transparency
There’s a couple of variations of the notion of referential transparency that seem quite useful in expressing properties of some functional languages:
1.1. Let transparency
Call a language let-transparent if for all well-typed terms , such that does not appear freely in , the terms and behave identically. In particular, this property implies lazy evaluation for .
1.2. Soft let transparency
Call a language soft let-transparent if for all well-typed terms (or int, or any sufficiently ,,pure’’ type), such that does not appear freely in and has a normal form the terms and behave identically. This still implies somewhat lazy if your language allows for non-terminating programs, but this laziness does not have to hold for side-effect-inducing terms assuming some kind of type coloring.
1.3. Softest let transparency
Call a language softest let-transparent if for all well-typed terms (or int, or any sufficiently ,,pure’’ type), such that does not appear freely in and , both have normal forms the terms and behave identically. This does not imply lazy evaluation in any case!
idk really what these notions are useful for but i came up with them last night when trying to sleep so idk