Apakah ada sistem tipe (statis) yang berupaya memformalkan karakteristik kinerja program? Saya tidak dapat menemukan upaya semacam itu.
Karena sistem tipe adalah (salah satu) alat paling ampuh dalam gudang programmer untuk membuat pernyataan tentang program, dan karena ada banyak contoh di mana kinerja sangat penting, tampaknya tidak akan terlalu jauh untuk membayangkan upaya telah dilakukan untuk membuat sistem tipe yang mencoba membuat setidaknya beberapa pernyataan tentang karakteristik penyimpanan dan runtime program.
language-design
Klaas van Schelven
sumber
sumber
if condition then expensive_operation else cheap_operation?if (likely(operation_went_fine)) { // Do something } else if (unlikely(error_occured)) { // Do something else }Jawaban:
Anda bisa membayangkan sistem tipe yang cukup canggih untuk dikaitkan dengan WCET atau kompleksitas program. Kemudian, masalahnya adalah membuat penganalisis jenis suara (atau pemeriksa) - yaitu aturan pengetikan - untuk membuatnya mungkin, dan menerapkannya secara cukup efisien untuk menjadikannya cukup berguna.
Sebagian besar sistem tipe cukup sederhana untuk dapat dengan cepat dihitung dalam praktiknya (setidaknya untuk serangkaian program yang masuk akal yang dapat ditulis oleh pengembang manusia secara manual).
Beberapa bahasa pemrograman akademis (misalnya AGDA ) memiliki sistem tipe yang sangat canggih yang Turing-complete, sehingga kompiler mereka mungkin membutuhkan banyak waktu (mungkin tak terbatas).
(Jika saya mengerti dengan baik, pekerjaan PhD Jérémie Salvucci yang sedang berlangsung di LIP6 di Paris cukup terkait dengan pertanyaan Anda; Saya telah mengiriminya email tentang itu; Anda mungkin mencari daerah dan jenis ...).
Namun waspadalah terhadap teorema Rice & masalah Hentikan . Jenis sistem mungkin tidak selalu menjadi peluru perak yang Anda inginkan (lihat buku no no bullet silver ).
sumber
Tampaknya sangat mungkin untuk membuat sistem tipe yang mengategorikan karakteristik kinerja tipe(misalnya "cepat / lambat untuk akses serial," cepat / lambat untuk akses acak "," memori efisien / tidak efisien "). Ciri-ciri tersebut dapat berupa tipe abstrak yang ditempatkan ke dalam hierarki sedemikian rupa sehingga semakin banyak jenis konkret yang diwarisi darinya. Namun, kinerja setiap program yang menggunakan tipe-tipe itu akan tergantung pada cara mereka sebenarnya digunakan / diakses.Untuk tipe sistem untuk membuat pernyataan tentang program itu sendiri, penggunaan (akses ke) tipe-tipe itu sendiri akan direpresentasikan sebagai tipe Ini berarti menghentikan penggunaan struktur kontrol built-in (misalnya untuk / sementara loop) dan alih-alih menggunakan tipe yang mengimplementasikannya. Oleh karena itu hirarki dapat memiliki tipe akses serial abstrak dan turunan daftar-akses-serial, tree-serial jenis -access dan sebagainya.Efisiensi penggunaan mungkin kemudian setidaknya sebagian dinyatakan oleh kombinasi dan penerapan jenis-jenis ini satu sama lain.
Dalam bahasa fungsional seperti Haskell - yang hampir tidak memiliki struktur kontrol - ini bagi saya cukup praktis dan dapat ditegakkan. Di Jawa, bagaimanapun, sistem seperti tampaknya jauh lebih sedikit dicapai (tidak begitu banyak dari pelaksanaan sejak keberlakuan / kepercayaan dari hasil).
Haskell sudah memungkinkan kita untuk menyatakan secara pasti seberapa besar suatu program murni dan menyediakan cara untuk membatasi kegiatan tertentu dalam kotak tertutup. Karena paralelisme / konkurensi di Haskell diimplementasikan melalui sistem tipe , dapat dikatakan bahwa itu sudah menjadi bagian dari perjalanan ke sana (dengan apa yang Anda inginkan). Sebaliknya, bahasa imperatif (bahkan yang diketik secara statis seperti Java) menawarkan banyak cara bagi para pembuat kode untuk menumbangkan upaya ini.
sumber