Values, Computations, and Referential Transparency

Riffing off of Programming Paradigms and the Procedural Paradox, by Eric Normand (which you should definitely read, if you haven’t).

I think the most important thing to add is that, in (lazy) purely functional languages (/ styles), functions are completely orthogonal to data, computations, and effects (/ actions).  Data, computations, and actions are types of expressions:

• 2 is a datum
• 2 + 2 is a computation
• print 2 is an action

and then you can classify functions according to what their function body is:

• λ 'x. [x] is a (parameterized) datum
• λ 'x. x + x is a (parameterized) computation
• λ 'x. print x is a (parameterized) action

Now, in a pure-functional language, data and computations have the same type, while data/computations and actions have different types.  So the type system doesn’t reflect the datum / computation / action distinction as well as we’d like.  (Despite that being a really useful distinction).

Global Script Core maintains a lifted / unlifted distinction. This distinguishes proper values / data from the value-or-non-termination things that normal lazy languages, like source-level Global Script, use. It lets the optimizer keep track of expressions that are guaranteed to terminate and variables that are always bound to (run-time) values.

The distinction between data and expressions is not the same as the lifted / unlifted distinction! 2 + 2 is a perfectly sensible unlifted expression (it’s guaranteed to terminate), but it remains a computation; while something like for rec 'xn ∝ 3 @ xn. xn is (probably) a value, even though it’s only allowed due to lifting. I don’t think that a recursive definition makes something a computation, unless the right-hand-side is already a computation.

The question is, should values and computations have different types? An expression and its value are clearly different things, or the concept of an expression evaluation wouldn’t make sense. On the other hand, when we write ‘2 + 2’ in a Global Script program, we intend it to be replaced with its denotation – which is a value. This is the original meaning of referential transparency, and it’s something Global Script shares with mathematical and (mostly) non-mathematical English (unlike side-effects, which are purely a programming-language invention).

So conflating values and computations in the type system has a respectable pedigree. In natural-language logic, when a statement needs to be referred to directly (as opposed to its meaning or truth-value), it’s put in quotes: “The statement that ‘Elizabeth II is the Queen of the United Kingdom’ is true now, but was false 100 years ago” [giving two examples]. In programming language theory, brackets are used instead: “2 + 2” is 4, but “[| 2 + 2 |]” is an expression. Global Script can do the same thing using the gs{} QLO, which quotes an expression (and explicitly captures variables from its enclosing scope). So λ 'x. 2 + x is a parameterized (computed) number, while λ 'x. gs{2 + x} is a parameterized expression.

I think that’s a reasonably clear way of making the distinction in the language, but the distinction itself is probably worth bringing up with student programmers.

Advertisement