Cos'è la digitazione dipendente?

Question

Qualcuno può spiegare la digitazione dipendente a me? Ho poca esperienza in Haskell, Cayenne, Epigram o altre lingue funzionali, quindi i termini più semplici che puoi usare, più lo apprezzerò!

Answer 1

Considera questo: in tutti i linguaggi di programmazione decenti puoi scrivere funzioni, ad esempio

def f(arg) = result

Qui, f prende un valore arg e calcola un valore result. È una funzione dai valori ai valori.

Ora, alcune lingue ti consentono di definire valori polimorfici (aka generici):

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

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

Di solito, puoi anche avere definizioni di tipo generico:

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

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

Così tanto per ciò che offrono le lingue ordinarie. Un linguaggio viene chiamato digiunato dipendente se offre anche la quarta possibilità, vale a dire definire le funzioni da valori ai tipi. O in altre parole, parametrizzare una definizione di tipo su un valore:

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

Alcune lingue tradizionali hanno una forma falsa di questo che non deve essere confusa. Ad esempio, in C ++, i modelli possono prendere valori come parametri, ma devono essere costanti a tempo di compilazione quando applicate. Non così in un linguaggio veramente dipendente. Ad esempio, potrei usare il tipo sopra in questo modo:

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

Qui, il tipo di risultato della funzione dipende Sul valore dell'argomento effettivo j, quindi la terminologia.

Answer 2

Se ti capita di sapere C ++, è facile fornire un esempio motivante:

Diciamo che abbiamo un tipo di contenitore e due istanze

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

e considera questo frammento di codice (si può presumere che FOO non sia vuoto):

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

Questo è evidente immondizia (e probabilmente corrompe le strutture di dati), ma verificherà il controllo benissimo poiché "iteratore in foo" e "iteratore nella barra" sono lo stesso tipo, IIMap::iterator, anche se sono completamente incompatibili semanticamente.

Il problema è che un tipo di iteratore non dovrebbe dipendere solo dal contenitore genere Ma in effetti sul contenitore oggetto, cioè dovrebbe essere un "tipo di membro 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 significa digitazione dipendente.

Il motivo per cui spesso non vedi questa funzione è perché apre una grande lattina di vermi: improvvisamente finisci in situazioni in cui, per verificare al momento della compilazione se due tipi sono uguali, finisci per dimostrare due espressioni sono equivalenti (produrrà sempre lo stesso valore in fase di esecuzione). Di conseguenza, se confronti Wikipedia Elenco delle lingue digitati dipendenti con i suoi Elenco dei proverti teoremi Potresti notare una somiglianza sospetta. ;-)

Answer 3

I tipi dipendenti consentono un set più ampio di errori logici da eliminare a Tempo di compilazione. Per illustrare questo considera le seguenti specifiche sulla funzione f:

Funzione f deve prendere solo anche numeri interi come input.

Senza tipi dipendenti potresti fare qualcosa del genere:

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 pari, cioè dal punto di vista del compilatore, la seguente espressione è OK:

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

Questo programma eseguirebbe e quindi lancerebbe un'eccezione in fase di esecuzione, ovvero il programma ha un errore logico.

Ora, i tipi dipendenti ti consentono di essere molto più espressivo e ti consentirebbero 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 aiutare a leggerlo ad alta voce come

n è un membro di un insieme di numeri interi in modo tale che ogni intero sia divisibile per 2.

In questo caso il compilatore rileva al momento della compilazione un errore logico in cui è stato passato un numero dispari a f e impedirebbe l'esecuzione del programma in primo luogo:

f(1)    // compiler error

---

Ecco un esempio illustrativo usando Scala Tipi dipendenti dal percorso di come potremmo tentare di implementare la funzione f Soddisfare tale requisito:

case class Integer(v: Int) {
  object IsEven { require(v % 2 == 0) }
  object IsOdd { require(v % 2 != 0) }
}

def f(n: Integer)(implicit proof: n.IsEven.type) =  { 
  // do something with n safe in the knowledge it is even
}

val `42` = Integer(42)
implicit val proof42IsEven = `42`.IsEven

val `1` = Integer(1)
implicit val proof1IsOdd = `1`.IsOdd

f(`42`) // OK
f(`1`)  // compile-time error

La chiave è notare come valore n appare nel tipo di valore proof vale a dire n.IsEven.type:

def f(n: Integer)(implicit proof: n.IsEven.type)
      ^                           ^
      |                           |
    value                       value

Noi diciamo genere n.IsEven.type dipende da valore n Da qui il termine tipi a carico.

Answer 4

Citando i tipi di libri e i linguaggi di programmazione (30.5):

Gran parte di questo libro si è preoccupato di formalizzare meccanismi di astrazione di vario genere. Nel Lambda-Calculus semplicemente digitato, abbiamo formalizzato il funzionamento di un termine e astrarre un sotterm, producendo una funzione che può essere successivamente istanziata applicandolo a termini diversi. Nel sistemaF, abbiamo considerato il funzionamento di un termine e astrarre un tipo, producendo un termine che può essere istanziato applicandolo a vari tipi. Inλω, abbiamo ricapitolato i meccanismi del Lambda-Calcolo semplicemente tipizzato "un livello in alto", prendendo un tipo e astrarre una sottoespressione per ottenere un operatore di tipo che può essere successivamente istanziato applicandolo a diversi tipi. Un modo conveniente di pensare a tutte queste forme di astrazione è in termini di famiglie di espressioni, indicizzate da altre espressioni. Un'astrazione di Lambda ordinaria λx:T1.t2 è una famiglia di termini [x -> s]t1 indicizzato da termini s. Allo stesso modo, un'astrazione di tipo λX::K1.t2 è una famiglia di termini indicizzati per tipi e un operatore di tipo è una famiglia di tipi indicizzati per tipi.

• λx:T1.t2 Famiglia di termini indicizzati da termini

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

• λX::K1.T2 Famiglia di tipi indicizzati per tipi

Guardando questo elenco, è chiaro che esiste una possibilità che non abbiamo ancora considerato: famiglie di tipi indicizzati da termini. Questa forma di astrazione è stata anche ampiamente studiata, sotto la rubrica di tipi dipendenti.