Sono sicuro che nei tipi Haskell vengono sempre cancellati prima dell'ora di esecuzione. Cosa succede in caso di Agda?I tipi vengono cancellati prima del runtime
Le informazioni di tipo dipendente vengono trasmesse all'esecuzione?
Quale runtime? Ci sono almeno quattro backend: quelli che hanno come target GHC (chiamato MAlonzo), UHC, Epic e JavaScript. Alcuni dettagli iniziali possono essere trovati in the Agda wiki: puoi leggere come il backend Epic cancella i tipi lì o in questo paper (il capitolo "3.3 Cancellazione"). In breve, i backend Epic e UHC cancellano tutti i tipi che riceve una funzione completamente applicata, ma non esegue la cancellazione completa in quanto può cambiare la semantica di un programma (citata da un paper sul backend UHC):
tipo definizione
I rimanenti termini
Π,SeteLevelsono significativo per la verifica del tipo soltanto. In Agda, un valore di tipoSetoLevelnon può essere verificato o il modello corrisponde. Poiché Agda applica il valore impossibile osservare qualsiasi valore di questi tipi, non è possibile che influenzi la semantica runtime. Per l'esecuzione di un programma, è quindi sicuro sostituire tutte le occorrenze di tali valori con il valore dell'unità⊤.Si potrebbe anche essere tentati di rimuovere completamente i valori di questi tipi di . Ciò potrebbe potenzialmente alterare la semantica del programma tradotto . Agda non valuta le espressioni sotto lambda; l'eliminazione delle astrazioni lambda che prendono le espressioni di tipo potrebbe rimuovere lambda di blocco della valutazione. Una cancellazione parziale dei tipi è possibile in in modo corretto. Le applicazioni con funzioni saturate, ad esempio, possono sempre essere ottimizzate in questo modo. Una descrizione più dettagliata di quando tali tipi possono essere cancellati può essere trovata nel lavoro precedente di Letouzey.
Non sono sicuro di cosa fa Agda ma Idris cerca di buttare via il più possibile. Non sono sicuro di Agda, ma sarebbe una buona cosa fare il più possibile, direi. – Jake