ตัวอย่าง Dependent types?

Question

สมมติว่าคุณมีออบเจ็กต์ 3 อันคือโกลบอลMemoryStoreซึ่งมีอาร์เรย์ของMemorySlabCacheอ็อบเจกต์และแต่ละอ็อบเจกต์MemorySlabCacheมีอาร์เรย์ของMemorySlabอ็อบเจกต์ เรียงตามนี้:

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

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

class MemorySlab {
  
}

แต่สิ่งนี้ไม่ได้จับภาพทุกอย่าง นอกจากนี้ยังต้องจับความจริงที่ว่าแต่ละชิ้นMemorySlabCacheมีขนาดซึ่งใช้เพื่อบอกขนาดของMemorySlabวัตถุนั้น ๆ ดังนั้นจึงเป็นเช่นนี้มากกว่า :

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

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

class MemorySlab<size: Integer> {
  
}

จากนั้นเราสร้างแคชของเรา:

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

สิ่งนี้นับเป็น " ประเภทที่ขึ้นกับ " "ประเภทที่มีคำจำกัดความขึ้นอยู่กับค่า"หรือไม่ ตั้งแต่ประเภทของArray<MemorySlab<size>>จะขึ้นอยู่กับค่าที่ได้รับมอบหมายให้ข้อมูลเกี่ยวกับsize MemorySlabCacheถ้าไม่นี่คืออะไร? อะไรที่จะทำให้เป็นตัวอย่างของประเภทที่ขึ้นต่อกัน?

Answer 1

ดังนั้นคำตอบคือ "ใช่" นี่คือตัวอย่างของประเภทที่ต้องพึ่งพา อย่างไรก็ตามปัญหาของตัวอย่างง่ายๆจำนวนมากที่ผู้คนสร้างขึ้นคือพวกเขาไม่ได้แสดงให้เห็นถึงแง่มุมที่ไม่สำคัญของการพิมพ์ขึ้นอยู่กับ

สมมติว่าคุณดีกว่าในแง่นี้เนื่องจากประเภทที่เป็นปัญหาขึ้นอยู่กับค่าโดยพลการในMemorySlabCache. อย่างไรก็ตามคุณไม่เคยใช้ค่าที่MemorySlabCacheไม่ทราบค่าคงที่ ตัวอย่างที่น่าสนใจกว่าก็คือ:

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

ดังนั้นคุณจึงอนุญาตให้ผู้ใช้เลือกขนาดแคชที่รันไทม์ แต่ขนาดแคชยังคงถูกบันทึกไว้ในประเภทและตัวตรวจสอบประเภทแบบคงที่จะช่วยให้มั่นใจได้ว่าการดำเนินการทั้งหมดเหมาะสมกับขนาดแม้ว่าจะไม่ทราบขนาดแบบคงที่ก็ตาม (ซึ่งเป็นอีกปัญหาหนึ่งในตัวอย่างของคุณไม่มีอะไรที่แสดงให้เห็นว่าขนาดที่ติดตามมีความสำคัญอย่างไรในภายหลัง)

ปัญหาเล็กน้อยกว่าคือจำนวนเต็มเป็นโครงสร้างที่ง่ายเกินไปสำหรับประเภทที่ขึ้นกับ 'ปลอม' ดังนั้นตัวอย่างที่พวกเขาจบลงด้วยการขายสิ่งที่อาจเป็นไปได้กับประเภทที่ขึ้นกับของแท้ ตัวอย่างเช่น Haskell ที่มีส่วนขยายบางอย่างสามารถเข้ารหัสได้แม้กระทั่งสิ่งที่คล้ายกับตัวอย่างขนาดรันไทม์แคชของฉันแม้ว่าจะไม่มีประเภทที่ขึ้นต่อกันก็ตาม คุณสามารถมีจำนวนเต็มระดับชนิดที่ทราบแบบคงที่และสร้างฟังก์ชันที่ให้ค่าที่เหมาะสมสำหรับค่าที่พิมพ์แบบคงที่ตามจำนวนเต็มรันไทม์ อย่างไรก็ตามภาษาที่อิงตามทฤษฎีประเภทขึ้นอยู่กับประเภทโดยทั่วไปจะให้ประเภทขึ้นอยู่กับค่าของประเภทที่กำหนดเองเช่นประเภทฟังก์ชัน สำหรับสิ่งเหล่านี้ (และคุณสมบัติอื่น ๆ ที่เกี่ยวข้อง) 'การแกล้งทำ' ไม่สามารถทำได้จริงๆ