Ví dụ về các loại phụ thuộc?

Question

Giả sử bạn có 3 đối tượng, một toàn cục MemoryStore, có một mảng MemorySlabCacheđối tượng và mỗi đối tượng MemorySlabCachecó một mảng MemorySlabđối tượng. Sắp xếp như thế này:

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

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

class MemorySlab {
  
}

Nhưng vấn đề là, điều này không nắm bắt được tất cả mọi thứ. Nó cũng cần nắm bắt thực tế rằng mỗi cái MemorySlabCachecó một kích thước, được sử dụng để cho biết kích thước của các MemorySlabđối tượng mà nó chứa. Vì vậy, nó là nhiều hơn như thế này:

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

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

class MemorySlab<size: Integer> {
  
}

Sau đó, chúng tôi tạo bộ nhớ đệm của mình:

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

Điều này có được tính là " kiểu phụ thuộc ", "kiểu có định nghĩa phụ thuộc vào giá trị" không? Vì kiểu của Array<MemorySlab<size>>phụ thuộc vào giá trị được gán cho sizetrường trên MemorySlabCache. Nếu không, đây là gì? Điều gì sẽ biến nó thành một ví dụ về các kiểu phụ thuộc?

Answer 1

Vì vậy, câu trả lời được cho là "có", đây là một ví dụ về các kiểu phụ thuộc. Tuy nhiên, vấn đề với rất nhiều ví dụ đơn giản mà mọi người tạo ra cho điều này là chúng không thể hiện các khía cạnh không tầm thường của việc nhập phụ thuộc.

Có thể cho rằng của bạn tốt hơn về mặt này, bởi vì loại được đề cập phụ thuộc vào một giá trị tùy ý trong MemorySlabCache. Tuy nhiên, bạn không bao giờ sử dụng một MemorySlabCachemà không có một giá trị tĩnh đã biết. Vì vậy, một ví dụ thú vị hơn sẽ như sau:

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

Vì vậy, bạn cho phép người dùng chọn kích thước bộ nhớ cache trong thời gian chạy, nhưng kích thước bộ nhớ cache vẫn được ghi lại trong loại và trình kiểm tra loại tĩnh đảm bảo rằng tất cả các hoạt động có ý nghĩa đối với kích thước, mặc dù kích thước không được biết ở dạng tĩnh (đó là một loại vấn đề khác với ví dụ của bạn; không có gì trong đó cho thấy kích thước được theo dõi quan trọng như thế nào sau đó).

Một vấn đề nhỏ hơn một chút là các số nguyên là cấu trúc quá dễ để 'giả mạo' các kiểu phụ thuộc, vì vậy các ví dụ về chúng cuối cùng sẽ bán những gì có thể khả thi với các kiểu phụ thuộc chính hãng. Ví dụ: Haskell với một số tiện ích mở rộng có thể mã hóa thậm chí một cái gì đó tương tự như ví dụ về kích thước bộ nhớ đệm thời gian chạy của tôi, mặc dù nó không thực sự có các kiểu phụ thuộc. Bạn có thể có các số nguyên cấp kiểu tĩnh đã biết và tạo một hàm cung cấp cho bạn một giá trị thích hợp cho một giá trị được nhập tĩnh dựa trên một số nguyên thời gian chạy. Tuy nhiên, các ngôn ngữ dựa trên lý thuyết kiểu phụ thuộc thường cho phép các kiểu phụ thuộc vào các giá trị của kiểu tùy ý, như kiểu hàm. Đối với những điều này (và các tính năng liên quan khác), 'giả mạo' không thực sự khả thi.