Contoh Jenis Bergantung?

Question

Katakanlah Anda memiliki 3 objek, global MemoryStore, yang memiliki larik MemorySlabCacheobjek, dan masing-masing MemorySlabCachememiliki larik MemorySlabobjek. Semacam seperti ini:

class MemoryStore {
  caches: Array<MemorySlabCache> = []
}

class MemorySlabCache {
  size: Integer
  slabs: Array<MemorySlab> = []
}

class MemorySlab {
  
}

Tapi masalahnya, ini tidak mencakup semuanya. Ini juga perlu menangkap fakta bahwa masing-masing MemorySlabCachememiliki ukuran, yang digunakan untuk mengetahui ukuran MemorySlabobjek yang dikandungnya. Jadi lebih seperti ini:

class MemoryStore {
  caches: Array<MemorySlabCache> = []
}

class MemorySlabCache {
  size: Integer
  slabs: Array<MemorySlab<size>> = []
}

class MemorySlab<size: Integer> {
  
}

Kemudian kami membuat cache kami:

let 4bytes = new MemorySlabCache(size: 4)
let 8bytes = new MemorySlabCache(size: 8)
...
let 32bytes = new MemorySlabCache(size: 32)
...
store.caches.push(4bytes, 8bytes, ..., 32bytes, ...)

Apakah ini dihitung sebagai " tipe dependen ", "tipe yang definisinya bergantung pada nilai" ? Karena jenisnya Array<MemorySlab<size>>tergantung pada nilai yang ditetapkan ke sizebidang tersebut MemorySlabCache. Jika tidak, apa ini? Apa yang membuatnya menjadi contoh tipe dependen?

Answer 1

Jadi, jawabannya bisa dibilang "ya", ini adalah contoh tipe dependen. Namun, masalah dengan banyak contoh sederhana yang dibuat orang untuk ini adalah mereka tidak mendemonstrasikan aspek non-sepele dari pengetikan dependen.

Bisa dibilang milik Anda lebih baik dalam hal ini, karena jenis yang dipermasalahkan bergantung pada nilai arbitrer di MemorySlabCache. Namun, Anda tidak pernah menggunakan MemorySlabCachetanpa nilai yang diketahui secara statis. Contoh yang lebih menarik seperti ini:

let cacheSize = readInteger(stdin)
store.caches.push(new MemorySlabCache(cacheSize))

Jadi, Anda mengizinkan pengguna untuk memilih ukuran cache saat runtime, tetapi ukuran cache masih dicatat dalam jenisnya, dan pemeriksa jenis secara statis memastikan bahwa semua operasi masuk akal sehubungan dengan ukurannya, meskipun ukurannya tidak diketahui secara statis (yang merupakan jenis masalah lain dengan contoh Anda; tidak ada di dalamnya yang menunjukkan bagaimana ukuran yang dilacak penting kemudian).

Masalah yang agak lebih kecil adalah bahwa bilangan bulat adalah struktur yang terlalu mudah untuk 'memalsukan' tipe dependen, jadi contoh dengan mereka berakhir di bawah penjualan apa yang mungkin layak dengan tipe dependen asli. Misalnya, Haskell dengan beberapa ekstensi dapat menyandikan bahkan sesuatu yang mirip dengan contoh ukuran cache runtime saya, meskipun itu tidak benar-benar memiliki tipe yang bergantung. Anda dapat memiliki bilangan bulat tingkat-jenis yang dikenal secara statis, dan membuat fungsi yang memberi Anda kembali nilai yang sesuai untuk nilai yang diketik secara statis berdasarkan integer waktu proses. Namun, bahasa berdasarkan teori tipe dependen umumnya membiarkan tipe bergantung pada nilai tipe arbitrer, seperti tipe fungsi. Untuk ini (dan fitur terkait lainnya), 'berpura-pura' tidak dapat dilakukan.