Mentre ci sono / c'erano diverse lingue con tipi dipendenti , come Agda , Coq o Epigram , nessuno sembrava ottenere un'adozione più ampia. Nonostante i tipi dipendenti consentano una sicurezza di tipo molto strong, fino alla scrittura di specifiche complete del programma. Qualcuno ha analizzato quali sono i principali blocchi per tali linguaggi a diventare più diffusi?
Non è sufficiente che una lingua abbia una bella funzionalità, ma ha anche bisogno di un'applicazione accattivante . Ad esempio, i linguaggi di programmazione funzionale non hanno preso realmente piede in commercio fino alla crescita dei big data in generale e di Scala e Apache Spark in particolare, ed è ancora largamente limitata a tali nicchie.
Personalmente, penso che la "killer app" della tipizzazione dipendente sia il suo potenziale per gli strumenti. Se hai mai guardato uno dei colloqui di sviluppo basati sui tipi di Edwin Brady, saprai cosa significare. Può scrivere una firma del tipo, quindi premere alcuni tasti di scelta rapida per scrivere il corpo della funzione. Con un po 'di raffinatezza e UX, penso che a un certo punto potrebbe rendere dipendente la digitazione di una caratteristica linguistica indispensabile.
Leggi altre domande sui tag functional-programming