2014-12-29 15 views
5

In Scala Language Specs (versione 2.9 - 11 giugno 2014), nella sezione sui tipi esistenziali viene usato il termine "sostituzione", tuttavia, il significato di sostituzione non sembra essere definito nelle Specifiche della lingua di Scala.Qual è la definizione del termine "sostituzione" nella Specifica lingua di Scala?

Qualcuno potrebbe spiegare cosa significa sostituzione in questo contesto?

Significa che una variabile di tipo in un'espressione di tipo è sostituita con un altro tipo concreto o tipo di variabile o tipo costruttore?

Se la sostituzione è pensata per essere un tipo concreto, allora vengono considerati i tipi concreti? Quelli che sono in ambito come un nome semplice?

Quale sarebbe una definizione significativa per il concetto di "sostituzione" in questo contesto?

Cosa viene sostituito con cosa?

enter image description here

+0

Solo supposizioni, ma forse si riferisce al [principio di sostituzione Liskov] (https://en.wikipedia.org/wiki/Liskov_substitution_principle) –

risposta

2

Si riferisce al concetto di sostituzione lambda-calcolo. Da un punto di vista pratico, è una sostituzione di variabili libere con quelle limitate. Per una definizione più formale, puoi guardare la teoria del calcolo lambda.

+0

Grazie per la preziosa intuizione. Solitamente leggo il libro di Pierce sui tipi, quindi ho una conoscenza di base del calcolo λ. Per me non è chiaro cosa significa variabile in questo caso? Quale può essere una variabile? Qualsiasi tipo? Qualsiasi tipo di costruttore? Tipi di cemento? Tipi più elevati di tipo? – jhegedus

+0

Non capisco cosa intendi dicendo: sostituire le variabili libere con quelle limitate? Per quanto ne so, la sostituzione avviene nel calcolo λ quando si applica un termine a un altro termine, ad esempio X Y. In tal caso, un parametro formale in X (una variabile associata) viene sostituito dal parametro Y effettivo che potrebbe contenere variabili libere. Non penso che le variabili libere vengano sostituite con qualcosa durante l'applicazione (che viene eseguita per sostituzione). – jhegedus

Problemi correlati