Qual è la buona spiegazione del principio di corrispondenza di Tennent?

Non ho mai sentito prima di "Tennent's Correspondence Principle" e ancor meno di ciò che è importante nella progettazione della lingua. Cercare su google le espressioni sembra portare a un blog di Neal Gafter del 2006 che definisce ciò che pensa sia e pensa che dovrebbe applicarsi anche alle chiusure. E la maggior parte degli altri nei forum sembra fare riferimento alla voce di Gafter.

Ecco comunque una menzione di "T.C.P." di Douglas Crockford (un nome che conosco e di cui mi fido): link . In parte

There are some things that can't be enclosed that way, such as return statements and break statements, which the advocates of Tennent's Correspondence Principle (or TCP) claim is a symptom of a bad smell. Yow! Language design is already difficult enough without having to cope with olfactory hallucinations. So to better understand the problem, I bought a copy of Tennent's 1981 book, Principles of Programming Languages.

It turns out that the Correspondence Principle is descriptive, not prescriptive. He uses it to analyze the (by now forgotten) Pascal programming language, showing a correspondence between variable definitions and procedure parameters. Tennent does not identify the lack of correspondence of return statements as a problem.

Quindi sembra che il nome "Tennent's Correspondence Principle" sia usato male, e qualsiasi cosa di cui Neal parla possibilmente dovrebbe essere chiamata "Gafter's Imagined and Possibly Generalized T.C.P." ... o qualcosa di simile. In ogni caso, non abbastanza da nascondersi dietro una cortina di nomi di libri fuori stampa

Vedo questo come parte di una regola generale che un linguaggio ben progettato fa quello che un programmatore si aspetterebbe naturalmente. Se ho un blocco di codice che voglio refactoring in una chiusura, e avvolgo quel blocco con la sintassi appropriata senza pensare veramente alle singole righe di codice, allora mi aspetto che quel blocco faccia la stessa cosa nella chiusura fatto in linea. Se alcune affermazioni usano la parola chiave "this" (forse implicitamente) e il linguaggio fa "questo" usato all'interno della chiusura si riferisce ad una classe anonima usata per rappresentarlo piuttosto che alla classe che definisce il metodo che definisce la chiusura, quindi il significato di quelle affermazioni sono cambiate, il mio blocco di codice non fa più quello che penso che faccia, e devo rintracciare un bug e capire come cambiare il mio codice per lavorare nella chiusura. Un linguaggio che mi impedisce di avere questi problemi è utile.

Il problema potrebbe anche essere mitigato con un IDE con strumenti intelligenti di refactoring, in grado di estrarre chiusure, rilevare potenziali problemi e persino regolare automaticamente il codice estratto per risolvere i problemi.

Claus Reinke: riguardante il "Design del linguaggio basato su principi semantici" di Tennent
Dà un'interpretazione interessante dei principi:
"La corrispondenza è il principio che ci consente di dire che

let(this=obj, x=5) { .. }  

e

((function(x) { .. }).call(obj,5))  

dovrebbe essere equivalente e qualsiasi cosa possiamo fare in liste di parametri formali, dovremmo anche essere in grado di fare in dichiarazioni, e viceversa. "[vedi anche, Reinke, sotto.]

R. D. Tennent: Metodi di progettazione linguistica basati sui principi semantici
"Due metodi di progettazione linguistica basati su principi derivati dall'approccio denotativo alla semantica del linguaggio di programmazione sono descritti e illustrati da un'applicazione al linguaggio Pascal I principi sono, in primo luogo, la corrispondenza tra i meccanismi parametrici e dichiarativi, e in secondo luogo, un principio di astrazione per linguaggi di programmazione adattati dalla teoria degli insiemi. Diverse estensioni e generalizzazioni utili di Pascal emergono applicando questi principi, inclusa una soluzione al problema dei parametri dell'array e una funzione di modularizzazione. "

Claus Reinke: "Sulla programmazione funzionale, sulla progettazione della lingua e sulla persistenza" su Haskell

Per rispondere alla domanda perché il CP di Tennent è così importante per il design della lingua, mi piacerebbe cita Neal Gafter :

Tennent's principles are very powerful because violations of them tend to show up in the language as flaws, irregularities, unnecessary restrictions, unexpected interactions or complications, and so on.

Qualunque violazione del TCP rischia di danneggiare alcuni programmatori in futuro quando si aspetta che le chiusure funzionino come il codice di non-chiusura ma scopre che, in violazione del TCP, non lo fanno.

RE Python non segue questo principio. Generalmente, segue il principio. Esempio di base:

>>> x = ['foo']
>>> x
['foo']
>>> x = (lambda: ['foo'])()
>>> x
['foo']

Tuttavia, Python definisce espressioni e dichiarazioni separatamente. Poiché if filiali, while cicli, assegnazione distruttiva e altre istruzioni non possono essere usate in lambda espressioni, la lettera del principio di Tennent non si applica a loro. Anche così, limitarsi a usare solo le espressioni Python produce ancora un sistema completo di Turing. Quindi non vedo questo come una violazione del principio; o meglio, se viola il principio, allora nessun linguaggio che definisce le dichiarazioni e le espressioni separatamente può eventualmente conformarsi al principio.

Inoltre, se il corpo dell'espressione lambda catturasse una traccia di stack o eseguisse un'altra introspezione nella VM, ciò potrebbe causare differenze. Ma a mio avviso questo non dovrebbe essere considerato una violazione. Se expr e (lambda: expr)() necessariamente compili allo stesso bytecode, allora il principio riguarda davvero i compilatori non la semantica; ma se possono compilare un bytecode diverso, non ci si deve aspettare che lo stato VM sia identico in ciascun caso.

Una sorpresa può essere incontrata usando la sintassi di comprensione, anche se credo che questa non sia una violazione del principio di Tennent. Esempio:

>>> [x for x in xrange(10)]
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
>>> [f() for f in [lambda: x for x in xrange(10)]]  # surprise!
[9, 9, 9, 9, 9, 9, 9, 9, 9, 9]
>>> # application of Tennent principle to first expression
... [(lambda: x)() for x in xrange(10)]
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
>>> [f() for f in [(lambda x: lambda: x)(x) for x in xrange(10)]]  # force-rebind x
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
>>> map(lambda f:f(), map(lambda x: lambda: x, xrange(10)))  # no issue with this form
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9]

La sorpresa è il risultato di come vengono definite le liste di comprensione. La sopra comprensione 'sorpresa' è equivalente a questo codice:

>>> result = []
>>> for x in xrange(10):
...   # the same, mutable, variable x is used each time
...   result.append(lambda: x)
... 
>>> r2 = []
>>> for f in result:
...   r2.append(f())
... 
>>> r2
[9, 9, 9, 9, 9, 9, 9, 9, 9, 9]

Visto in questo modo, la comprensione "sorpresa" di cui sopra è meno sorprendente, e non una violazione del principio di Tennent.