Przykład typów zależnych?

Question

Załóżmy, że masz 3 obiekty, globalne MemoryStore, które mają tablicę MemorySlabCacheobiektów, a każdy MemorySlabCachema tablicę MemorySlabobiektów. Coś w ten sposób:

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

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

class MemorySlab {
  
}

Ale chodzi o to, że to nie uchwyci wszystkiego. Musi również uchwycić fakt, że każdy MemorySlabCachema rozmiar, który służy do określenia, jaki rozmiar MemorySlabzawiera obiekty. Więc wygląda to bardziej tak:

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

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

class MemorySlab<size: Integer> {
  
}

Następnie tworzymy nasze cache:

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

Czy liczy się to jako „ typ zależny ”, „typ, którego definicja zależy od wartości” ? Ponieważ rodzaj Array<MemorySlab<size>>zależy od wartości przypisanej do sizepola na MemorySlabCache. Jeśli nie, co to jest? Co uczyniłoby to przykładem typów zależnych?

Answer 1

Tak więc odpowiedź prawdopodobnie brzmi „tak”, to jest przykład typów zależnych. Jednak problem z wieloma prostymi przykładami, które ludzie w tym celu tworzą, polega na tym, że nie demonstrują one nietrywialnych aspektów zależnego pisania.

Prawdopodobnie twój jest lepszy pod tym względem, ponieważ dany typ zależy od dowolnej wartości w MemorySlabCache. Jednak nigdy nie używasz wartości MemorySlabCachebez statycznie znanej wartości. Więc bardziej interesujący byłby przykład:

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

Dlatego pozwalasz użytkownikowi wybrać rozmiar pamięci podręcznej w czasie wykonywania, ale rozmiar pamięci podręcznej jest nadal rejestrowany w typie, a narzędzie do sprawdzania typów zapewnia statycznie, że wszystkie operacje mają sens w odniesieniu do rozmiaru, nawet jeśli rozmiar nie jest statycznie znany (co jest kolejnym problemem z twoim przykładem; nic w nim nie pokazuje, jakie znaczenie ma później śledzony rozmiar).

Nieco mniejszym problemem jest to, że liczby całkowite są zbyt łatwą strukturą, aby „sfałszować” typy zależne, więc przykłady z nimi kończą się sprzedażą tego, co może być wykonalne w przypadku prawdziwych typów zależnych. Na przykład Haskell z niektórymi rozszerzeniami może zakodować nawet coś podobnego do mojego przykładu rozmiaru pamięci podręcznej czasu wykonywania, nawet jeśli tak naprawdę nie ma typów zależnych. Możesz mieć statycznie znane liczby całkowite na poziomie typu i utworzyć funkcję, która zwraca odpowiednią wartość dla wartości wpisanej statycznie na podstawie liczby całkowitej czasu wykonywania. Jednak języki oparte na teorii typów zależnych generalnie pozwalają, aby typy zależały od wartości dowolnych typów, takich jak typy funkcji. W przypadku tych (i innych funkcji pokrewnych) „udawanie” jest niewykonalne.