# 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