Che cos'è la digitazione dipendente?

Question

Qualcuno può spiegare la digitazione dipendente da me? Ho poca esperienza in Haskell, Cayenne, Epigram o in altri linguaggi funzionali, quindi il più semplice dei termini che puoi usare, più lo apprezzerò!

Answer 1

Considerare questo: in tutti i linguaggi di programmazione decenti è possibile scrivere funzioni, ad es.

def f(arg) = result 

Qui, f assume un valore arg e calcola un valore result. È una funzione da valori a valori.

Ora, alcune lingue consentono di definire i valori polimorfiche (aka generici):

def empty<T> = new List<T>() 

Qui, empty prende un tipo T e calcola un valore. È una funzione da tipi a valori.

Di solito, si può anche avere definizioni generiche tipo:

type Matrix<T> = List<List<T>> 

Questa definizione prende un tipo e restituisce un tipo. Può essere visto come una funzione da tipi a tipi.

Questo per quanto riguarda le lingue ordinarie. Una lingua è chiamata tipicamente digitata se offre anche la quarta possibilità, ovvero la definizione di funzioni da valori a tipi. O in altre parole, la parametrizzazione di una definizione di tipo per un valore di:

type BoundedInt(n) = {i:Int | i<=n} 

Alcuni linguaggi tradizionali hanno una qualche forma falsi di questo che non deve essere confuso. Per esempio. in C++, i modelli possono assumere valori come parametri, ma devono essere costanti in fase di compilazione quando applicati. Non così in un linguaggio tipicamente dipendente. Per esempio, ho potuto utilizzare il tipo di cui sopra in questo modo:

def min(i : Int, j : Int) : BoundedInt(j) = 
    if i < j then i else j 

Edit: Ecco, della funzione tipo di risultato dipende sul valore dell'argomento reale j, in tal modo la terminologia.

Answer 2

citando il libro Tipi e linguaggi di programmazione (30,5):

Gran parte di questo libro è stata interessata con formalizzare l'astrazione meccanismi di vario genere. Nel lambda-calcolo semplicemente digitato, abbiamo formalizzato l'operazione di prendere un termine e astraendo un sottotermine , ottenendo una funzione che può successivamente essere istanziata da applicandolo a termini differenti. Nel sistema F, abbiamo considerato l'operazione di prendere un termine e di estrarre un tipo, ottenendo un termine che può essere istanziato applicandolo a vari tipi. Nel numero λω, abbiamo ricapitolato i meccanismi del lambda-calcolo semplicemente "uno di livello superiore", prendendo un tipo e estraendo una sottoespressione per ottenere un operatore di tipo che può essere istanziato in seguito applicandolo a tipi diversi. Un modo conveniente di pensare a tutte queste forme di astrazione è in termini di famiglie di espressioni, indicizzate da altre espressioni . Un'ordinaria astrazione lambda λx:T1.t2 è una famiglia di termini [x -> s]t1 indicizzati dai termini s. Allo stesso modo, un'astrazione di tipo λX::K1.t2 è una famiglia di termini indicizzati dai tipi e un operatore di tipo è una famiglia di tipi indicizzati per tipo.

• λx:T1.t2 famiglia di termini indicizzati dai termini

• λX::K1.t2 famiglia di termini indicizzati dai tipi

• λX::K1.T2 famiglia di tipi indicizzate da tipi

Guardando questa lista, è chiaro che c'è una possibilità che abbiamo Non ancora considerati: famiglie di tipi indicizzati in termini. Questa forma di astrazione è stata anche ampiamente studiata, sotto la rubrica dei tipi dipendenti.

Answer 3

Se vi capita di conoscere C++ è facile fornire un esempio motivante:

Diciamo che abbiamo un certo tipo di contenitore e due istanze dello stesso

typedef std::map<int,int> IIMap; 
IIMap foo; 
IIMap bar; 

e considerare questo frammento di codice (si può assumere foo non è vuoto):

IIMap::iterator i = foo.begin(); 
bar.erase(i); 

Questo è evidente garbage (e probabilmente corrompe la struttura dei dati s), ma sarà tipicamente corretto, dal momento che "iteratore in foo" e "iteratore in barra" sono dello stesso tipo, IIMap::iterator, anche se sono completamente incompatibili semanticamente.

Il problema è che un tipo iteratore non dovrebbe dipendere solo sul contenitore tipo ma in realtà sul contenitore oggetto, cioè dovrebbe essere un "Tipo di utente non statico":

foo.iterator i = foo.begin(); 
bar.erase(i); // ERROR: bar.iterator argument expected 

Tale caratteristica, la capacità di esprimere un tipo (foo.iterator) che dipende da un termine (foo), è esattamente ciò che dipende dalla digitazione.

Il motivo per cui non si vede spesso questa funzionalità è perché apre una grande quantità di worm: si finisce improvvisamente in situazioni in cui, per verificare in fase di compilazione se due tipi sono uguali, si finisce per avere per dimostrare che due espressioni sono equivalenti (fornirà sempre lo stesso valore in fase di esecuzione). Di conseguenza, se si confronta wikipedia list of dependently typed languages con il suo list of theorem provers si potrebbe notare una somiglianza sospetta. ;-)

Answer 4

tipi dipendenti consentono grande insieme di logic errors essere eliminati in fase di compilazione . Per illustrare questo in considerazione le seguenti specifiche sulla funzione f:

Funzione f deve prendere solo anche interi come input.

Senza di tipi dipendenti si potrebbe fare qualcosa di simile:

def f(n: Integer) := { 
    if n mod 2 != 0 then 
    throw RuntimeException 
    else 
    // do something with n 
} 

Qui il compilatore non può rilevare se n è davvero ancora, cioè, dal punto di vista del compilatore la seguente espressione è ok:

f(1) // compiles OK despite being a logic error! 

Questo programma viene eseguito e genera un'eccezione in fase di esecuzione, ovvero il programma ha un errore logico.

Ora, tipi dipendenti consentono di essere molto più espressivo e si dovrebbe consentire di scrivere qualcosa del genere:

def f(n: {n: Integer | n mod 2 == 0}) := { 
    // do something with n 
} 

Qui n è di tipo dipendente {n: Integer | n mod 2 == 0}. Potrebbe essere utile per leggere ad alta voce come

n è un membro di un insieme di numeri tali che ogni intero è divisibile per 2.

In questo caso il compilatore di rilevare in fase di compilazione un errore logico in cui è stato superato un numero dispari di f e da impedire la programma da eseguire, in primo luogo:

f(1) // compiler error