Qual è il motivo di un sistema di tipo completo di Turing

Question

Scala e Haskell hanno "Sistemi di tipo completo di Turing". Solitamente, la completezza di Turing si riferisce a computations and languages. Cosa significa veramente nel contesto dei tipi?

Qualcuno potrebbe dare un esempio di come un programmatore può trarne vantaggio?

PS Non voglio confrontare i sistemi di tipi di Haskell vs Scala. È più circa il termine in generale.

PSS Se è possibile più esempi di Scala.

Answer 1

Cosa significa realmente nel contesto dei tipi?

Significa che il sistema di tipi ha caratteristiche sufficienti in esso per rappresentare calcoli arbitrari. Come prova molto breve, presento di seguito un'implementazione di livello tipo del calcolo SK; ci sono molti posti in cui si discute della completezza di questo calcolo e di cosa significhi Turing, quindi non lo ripeterò qui.

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE UndecidableInstances #-} 
{-# LANGUAGE TypeOperators #-} 

infixl 1 `App` 
data Term = S | K | App Term Term 

type family Reduce t where 
    Reduce S = S 
    Reduce K = K 
    Reduce (S `App` x `App` y `App` z) = Reduce (x `App` z `App` (y `App` z)) 
    Reduce (K `App` x `App` y) = Reduce x 
    Reduce (x `App` y) = Reduce (Reduce x `App` y) 

Si può vedere questo in azione a un prompt ghci; per esempio, nel SK calcolo, il termine SKSK riduce (eventualmente) a poco K:

> :kind! Reduce (S `App` K `App` S `App` K) 
Reduce (S `App` K `App` S `App` K) :: Term 
= 'K 

Ecco un divertente da provare così:

> type I = S `App` K `App` K 
> type Rep = S `App` I `App` I 
> :kind! Reduce (Rep `App` Rep) 

Non voglio rovinare il divertimento - - prova tu stesso. Ma sappi come terminare prima i programmi con estremo pregiudizio.

Qualcuno potrebbe dare un esempio di come un programmatore può trarne vantaggio?

Il calcolo a livello di codice arbitrario consente di esprimere invarianti arbitrari sui tipi e di verificare che il compilatore (in fase di compilazione) venga conservato. Vuoi un albero rosso-nero? Che ne dite di un albero rosso-nero che il compilatore può controllare preservando gli invarianti rosso-nero-albero? Sarebbe utile, giusto, dal momento che esclude un'intera classe di bug di implementazione? Che ne dici di un tipo per i valori XML che è staticamente noto per corrispondere a uno schema particolare? Infatti, perché non fare un ulteriore passo avanti e annotare un tipo parametrizzato il cui parametro rappresenta uno schema? Quindi è possibile leggere uno schema in fase di esecuzione e fare in modo che i controlli in fase di compilazione garantiscano che il proprio valore parametrizzato possa rappresentare solo valori ben formati in tale schema. Bello!

Oppure, forse un esempio più prosaico: cosa succede se si desidera che il compilatore verifichi di non aver mai indicizzato il dizionario con una chiave che non era presente? Con un sistema di tipi sufficientemente avanzato, puoi.

Naturalmente, c'è sempre un prezzo. In Haskell (e probabilmente in Scala?), Il prezzo di un controllo molto interessante in fase di compilazione sta spendendo un bel po 'di tempo e sforzi per convincere il compilatore che la cosa che stai verificando è vera - e questo è spesso sia un alto costo iniziale e costi di manutenzione elevati.