Il sistema di tipi in Scala è completato da Turing. Prova? Esempio? Benefici?

Question

Ci sono affermazioni che il sistema di tipi di Scala sia completato da Turing. Le mie domande sono:

1. Esiste una prova formale per questo?

2. Come apparirebbe un semplice calcolo nel sistema di tipi Scala?

3. Questo è di qualche vantaggio per Scala - la lingua? Questo rende Scala più "potente" in qualche modo rispetto alle lingue senza un sistema di tipo completo di Turing?

Immagino che questo si applichi alle lingue e ai sistemi di tipi in generale.

Answer 1

C'è un post di blog da qualche parte con un'implementazione di livello tipo del calcolo del combinatore SKI, che è noto per essere completato da Turing.

I sistemi di tipo Turing-completi hanno sostanzialmente gli stessi vantaggi e gli stessi inconvenienti dei linguaggi completi di Turing: puoi fare qualsiasi cosa, ma puoi dimostrarti molto poco. In particolare, non puoi provare che alla fine farai qualcosa.

Un esempio di calcolo a livello di carattere sono i nuovi trasformatori di raccolta preservazione di tipo in Scala 2.8. In Scala 2.8, metodi come map, filter e così via sono garantiti per restituire una collezione dello stesso tipo su cui sono stati chiamati. Quindi, se si filter a Set[Int], si ottiene un Set[Int] e se si map a List[String] si ottiene un List[Whatever the return type of the anonymous function is].

Ora, come potete vedere, map può effettivamente trasformare il tipo di elemento. Quindi, cosa succede se il nuovo tipo di elemento non può essere rappresentato con il tipo di raccolta originale? Esempio: a BitSet può contenere solo numeri interi a larghezza fissa. Quindi, cosa succede se si dispone di un BitSet[Short] e si mappa ogni numero con la sua rappresentazione di stringa?

someBitSet map { _.toString() } 

Il risultato sarebbe essere un BitSet[String], ma questo è impossibile. Quindi, Scala sceglie il supertipo più derivato di BitSet, che può contenere un String, che in questo caso è un Set[String].

Tutto questo calcolo è in corso durante di compilazione, o più precisamente durante tipo tempo controllo, utilizzando le funzioni di tipo-livello. Pertanto, è staticamente garantito che sia sicuro per il tipo, anche se i tipi sono effettivamente calcolati e quindi non noti in fase di progettazione.

Answer 2

Il mio blog post sulla codifica del calcolo SCI nel sistema di tipo Scala mostra la completezza di Turing.

Per alcuni semplici calcoli a livello di testo sono disponibili anche alcuni esempi su come codificare i numeri naturali e l'aggiunta/multiplication.

Infine, vi è un ottimo series of articles sulla programmazione a livello di tipo sul blog di Apocalisp.