|
|
| Line 7: |
Line 7: |
| </blockquote> | | </blockquote> |
|
| |
|
| A programming language is trivially denotative if it only permits programs to be defined in terms of denotative expressions.
| | Mathematics itself is trivially denotative: |
| | |
| == Being privately imperative ==
| |
| | |
| [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.144.2237&rep=rep1&type=pdf In 1994] researchers discovered a way to denotatively accommodate the imperative style by excluding the use of <i>externally visible</i> side-effects. For example:
| |
|
| |
|
| <blockquote> | | <blockquote> |
| <haskell>
| | When a mathematician develops a theorem, she or he defines symbols, then writes |
| type Graph = Array Vertex [Vertex]
| | down facts that relate those symbols. The order of those facts is unimportant, so long as all the |
| data Tree a = Node a [Tree a]
| | symbols used are defined, and it certainly does not matter where each fact is written on the paper! |
| | | A proof is a static thing—its parts just <i>are</i>, they do not <i>act</i>. |
| dfs :: Graph -> [Vertex] -> [Tree Vertex]
| |
| dfs g vs = runST (
| |
| newSTArray (bounds g) False >>= \ marks ->
| |
| search marks vs
| |
| )
| |
| where search :: STArray s Vertex Bool -> [Vertex]
| |
| -> ST s [Tree Vertex]
| |
| search marks [] = return []
| |
| search marks (v:vs) = readSTArray marks v >>= \ visited ->
| |
| if visited then
| |
| search marks vs
| |
| else
| |
| writeSTArray marks v True >>
| |
| search marks (g!v) >>= \ ts ->
| |
| search marks vs >>= \ us ->
| |
| return ((Node v ts): us)
| |
| </haskell> | |
|
| |
|
| :<small>from Figure 2 (page 17 of 51) of [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.52.3656&rep=rep1&type=pdf State in Haskell]</small> | | :<small>[https://digitalcommons.newhaven.edu/cgi/viewcontent.cgi?article=1000&context=electricalcomputerengineering-books The Anatomy of Programming Languages] (page 354 of 600).</small> |
| </blockquote> | | </blockquote> |
|
| |
|
| Even though <code>dfs</code>'s local definition:
| | so <math>[\![{E}]\!]_{mathematics} {{=}} {E}</math> if <math>{E}</math> is a mathematical expression. |
| | |
| <haskell>
| |
| search :: STArray s Vertex Bool -> [Vertex] -> ST s [Tree Vertex]
| |
| </haskell>
| |
| | |
| uses mutability and sequencing, the use of <code>runST</code> keeps those imperative details confined to <code>dfs</code>, hence its denotative type:
| |
| | |
| <haskell>
| |
| dfs :: Graph -> [Vertex] -> [Tree Vertex]
| |
| </haskell> | |
| | |
| Therefore to be denotative, a programming language only needs to avoid using side effects which are externally visible: namely those of I/O.
| |
| | |
| == Practical considerations ==
| |
| | |
| But most users <i>want</i> to interact with their programs, including those written in denotative languages! That requires I/O to be managed by the denotative language's implementation, with parts of it written in a non-denotative (I/O-capable) programming language.
| |
| | |
| This need for a non-denotative language though presents a dilemma:
| |
| | |
| * if it's too different from the denotative language, it's likely that users will [https://discourse.dhall-lang.org/t/proposal-do-notation-syntax/99 request] or [https://discourse.dhall-lang.org/t/a-failed-attempt-at-doing-io-with-dhall/565 attempt to add] an I/O mechanism to the denotative language (to avoid having to extend the implementation);
| |
| | |
| * if it's quite similar to the denotative language, users could do all their programming in it and simply ignore the denotative language (as writing a program in multiple languages is often tedious).
| |
|
| |
|
| It remains to be seen whether these two opposing requirements can be reconciled.
| | A programming language is denotative if it only allows programs to be defined in terms of denotative expressions. |
|
| |
|
|
| |
|
| [[Category:Glossary]] | | [[Category:Glossary]] |
Revision as of 20:00, 22 January 2025
On page 8 of The Next 700 Programming Languages, Peter Landin introduces the word denotative
as the direct opposite of the term imperative
. To be considered denotative, Landin stipulates the following conditions for the expressions of a programming language:
(a) each expression has a nesting subexpression structure,
(b) each subexpression denotes something (usually a number, truth value or numerical function),
(c) the thing an expression denotes, i.e., its "value", depends only on the values of its subexpressions, not on other properties of them.
Mathematics itself is trivially denotative:
When a mathematician develops a theorem, she or he defines symbols, then writes
down facts that relate those symbols. The order of those facts is unimportant, so long as all the
symbols used are defined, and it certainly does not matter where each fact is written on the paper!
A proof is a static thing—its parts just are, they do not act.
- The Anatomy of Programming Languages (page 354 of 600).
so if is a mathematical expression.
A programming language is denotative if it only allows programs to be defined in terms of denotative expressions.