Scala utilizza un sistema di tipi basato su Sistema F ω, che normalmente si dice che sia fortemente normalizzante. La forte normalizzazione implica la non completezza di Turing.Quale proprietà del sistema di tipi Scala lo rende Turing-completo?
Tuttavia, il sistema di tipo Scala è completo di Turing.
Quali modifiche/aggiunte/modifiche rendono il sistema di tipi di Scala completo di Turing rispetto agli algoritmi e ai sistemi formali?
Non è una risposta esauriente, ma il motivo è che è possibile definire i tipi ricorsivi.
Ho già fatto domande simili (about what a non-Turing complete language might look like). Le risposte erano nella forma: una lingua completa di Turing deve supportare looping o ricorsione arbitrari. Il sistema di tipi Scala supporta quest'ultimo
Ricorsivo i tipi esistono nella maggior parte delle lingue, inclusi Java e Pascal. Qualsiasi tipo che si riferisce a se stesso (come una lista collegata) è ricorsivo. È necessario un modo per eseguire il calcolo a livello di testo, ad esempio un'applicazione di tipo. In Scala, hai membri di tipo e applicazione di tipo parziale in alias di tipi. –
Intendevo i tipi ricorsivi nel senso della codifica peano: http://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/ usando 'type', non' class' o ' trait'. Pensavo che fosse ragionevolmente ovvio dato il contesto. Come ho detto, sto echeggiando qui, quello che mi è stato detto sulla completezza di Turing. –
[Tipi ricorsivi] (http://en.wikipedia.org/wiki/Recursive_data_type) possono essere utilizzati per codificare numeri come dici tu, ma non sono sufficienti per la completezza di Turing. Quello che vuoi è un modo per calcolare, in questo caso usando l'applicazione di tipo (che a sua volta usa la sostituzione). I membri del tipo Scala lo rendono piuttosto facile, sebbene Java esegua sostituzioni simili per i generici. –
Collegamenti/riferimenti? (Per gli spettatori, come me :-) –
Il fatto che System F sia fortemente normalizzato implica che System F non sia Turing completo. Non implica che il suo sistema di tipi non lo sia. E infatti è stato dimostrato che [typechecking un Sistema F senza restrizioni è indecidibile] (http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.6483) – sepp2k
@ sepp2k - yikes, the la cosa peggiore della completezza di Turing e ce l'ha. – Malvolio