Wyjaśnienie dotyczące rodzajów egzystencjalnych w Haskell

Usiłuję zrozumieć typy egzystencjalne w Haskell i natknąłem się na plik PDF http://www.ii.uni.wroc.pl/~dabi/courses/ZPF15/rlasocha/prezentacja.pdf

Popraw moje poniższe rozumienie, które mam do tej pory.

• Typy egzystencjalne nie wydają się być zainteresowane zawartym w nich typem, ale dopasowanie do nich wzoru mówi, że istnieje jakiś typ, którego nie wiemy, dopóki nie użyjemy Typeable lub Data.
• Używamy ich, gdy chcemy ukryć typy (np. Dla list heterogenicznych) lub nie bardzo wiemy, jakie typy w czasie kompilacji.
• GADT„s zapewniają jasny i lepsze składni do kodu za pomocą egzystencjalnych Rodzaje dostarczając ukryte forall” s

Moje wątpliwości

• Na stronie 20 powyższego pliku PDF wspomniano w poniższym kodzie, że funkcja nie może żądać określonego bufora. Dlaczego tak jest Kiedy opracowuję Funkcję, dokładnie wiem, jakiego rodzaju bufora użyję, chociaż może nie wiem, jakie dane do niego wstawię. Co jest złego w posiadaniu :: Worker MemoryBuffer IntJeśli naprawdę chcą abstrakcji nad Buforem, mogą mieć typ Sum data Buffer = MemoryBuffer | NetBuffer | RandomBufferi mieć podobny typ:: Worker Buffer Int

data Worker x = forall b. Buffer b => Worker {buffer :: b, input :: x}
data MemoryBuffer = MemoryBuffer

memoryWorker = Worker MemoryBuffer (1 :: Int)
memoryWorker :: Worker Int

• Ponieważ Haskell jest językiem wymazywania pełnego typu, takim jak C, to skąd w Runtime wie, którą funkcję wywołać. Czy to tak, jakbyśmy zachowali kilka informacji i przekazali Ogromny V-Tabela Funkcji, a w czasie wykonywania wyliczy z V-Tabela? Jeśli tak, to jakie informacje będzie przechowywać?

GADT zapewniają przejrzystą i lepszą składnię kodu przy użyciu typów egzystencjalnych, zapewniając niejawne forall

Myślę, że istnieje ogólna zgoda co do tego, że składnia GADT jest lepsza. Nie powiedziałbym, że dzieje się tak dlatego, że GADT zapewniają niejawne foralls, ale dlatego, że oryginalna składnia, włączona z ExistentialQuantificationrozszerzeniem, jest potencjalnie myląca / myląca. Ta składnia wygląda następująco:

data SomeType = forall a. SomeType a

lub z ograniczeniem:

data SomeShowableType = forall a. Show a => SomeShowableType a

i myślę, że zgoda polega na tym, że użycie słowa kluczowego w tym forallmiejscu pozwala łatwo pomylić typ z zupełnie innym typem:

data AnyType = AnyType (forall a. a)    -- need RankNTypes extension

Lepsza składnia mogła użyć osobnego existssłowa kluczowego, więc możesz napisać:

data SomeType = SomeType (exists a. a)   -- not valid GHC syntax

Składnia GADT, używana jawnie lub jawnie forall, jest bardziej jednolita dla tych typów i wydaje się łatwiejsza do zrozumienia. Nawet z wyraźnym wyjaśnieniem forallw poniższej definicji można przyjąć wartość dowolnego typu ai umieścić ją w monomorficznym SomeType':

data SomeType' where
    SomeType' :: forall a. (a -> SomeType')   -- parentheses optional

i łatwo jest zobaczyć i zrozumieć różnicę między tym typem a:

data AnyType' where
    AnyType' :: (forall a. a) -> AnyType'

Typy egzystencjalne nie wydają się być zainteresowane zawartym w nich typem, ale dopasowanie do nich wzoru mówi, że istnieje jakiś typ, którego nie wiemy, dopóki nie użyjemy Typeable lub Data.

Używamy ich, gdy chcemy ukryć typy (np. Dla list heterogenicznych) lub nie bardzo wiemy, jakie typy w czasie kompilacji.

Sądzę, że nie są one zbyt odległe, chociaż nie musisz używać Typeableani Dataużywać typów egzystencjalnych. Myślę, że bardziej trafne byłoby stwierdzenie, że typ egzystencjalny zapewnia dobrze wpisane „pole” wokół nieokreślonego typu. Pole „ukrywa” typ w pewnym sensie, co pozwala ci stworzyć heterogeniczną listę takich pól, ignorując zawarte w nich typy. Okazuje się, że nieograniczony egzystencjalny, jak SomeType'wyżej, jest dość bezużyteczny, ale ograniczony typ:

data SomeShowableType' where
    SomeShowableType' :: forall a. (Show a) => a -> SomeShowableType'

pozwala wzorować dopasowanie, aby zajrzeć do „pudełka” i udostępnić obiekty klasy typu:

showIt :: SomeShowableType' -> String
showIt (SomeShowableType' x) = show x

Zauważ, że działa to dla dowolnej klasy typu, nie tylko Typeablelub Data.

Jeśli chodzi o zamieszanie związane ze stroną 20 pokładu slajdów, autor twierdzi, że nie jest możliwe, aby funkcja wymagająca egzystencji Worker wymagała Workerposiadania określonej Bufferinstancji. Możesz napisać funkcję, aby utworzyć Workerokreślony typ Buffer, na przykład MemoryBuffer:

class Buffer b where
  output :: String -> b -> IO ()
data Worker x = forall b. Buffer b => Worker {buffer :: b, input :: x}
data MemoryBuffer = MemoryBuffer
instance Buffer MemoryBuffer

memoryWorker = Worker MemoryBuffer (1 :: Int)
memoryWorker :: Worker Int

ale jeśli napiszesz funkcję, która przyjmuje Workerargument jako, może korzystać tylko z funkcji Bufferklasy ogólnej (np. funkcji output):

doWork :: Worker Int -> IO ()
doWork (Worker b x) = output (show x) b

Nie może próbować wymagać bokreślonego typu bufora, nawet poprzez dopasowanie wzorca:

doWorkBroken :: Worker Int -> IO ()
doWorkBroken (Worker b x) = case b of
  MemoryBuffer -> error "try this"       -- type error
  _            -> error "try that"

Wreszcie informacje o środowisku wykonawczym dotyczące typów egzystencjalnych są udostępniane za pośrednictwem niejawnych argumentów „słownika” dla zaangażowanych klas typów. Powyższy Workertyp, oprócz pól dla bufora i danych wejściowych, ma także niewidoczne pole niejawne, które wskazuje na Buffersłownik (trochę jak tabela v, choć nie jest to ogromne, ponieważ zawiera tylko wskaźnik do odpowiedniej outputfunkcji).

Wewnętrznie klasa typu Bufferjest reprezentowana jako typ danych z polami funkcyjnymi, a instancje to „słowniki” tego typu:

data Buffer' b = Buffer' { output' :: String -> b -> IO () }

dBuffer_MemoryBuffer :: Buffer' MemoryBuffer
dBuffer_MemoryBuffer = Buffer' { output' = undefined }

Typ egzystencjalny ma ukryte pole dla tego słownika:

data Worker' x = forall b. Worker' { dBuffer :: Buffer' b, buffer' :: b, input' :: x }

a taka funkcja, doWorkktóra działa na Worker'wartościach egzystencjalnych , jest implementowana jako:

doWork' :: Worker' Int -> IO ()
doWork' (Worker' dBuf b x) = output' dBuf (show x) b

W przypadku klasy typu z tylko jedną funkcją słownik jest w rzeczywistości zoptymalizowany pod kątem nowego typu, więc w tym przykładzie Workertyp egzystencjalny zawiera ukryte pole, które składa się ze wskaźnika outputfunkcji do bufora, i to jedyne potrzebne informacje o środowisku wykonawczym przez doWork.

Na stronie 20 powyższego pliku PDF wspomniano w poniższym kodzie, że funkcja nie może żądać określonego bufora. Dlaczego tak jest

Ponieważ Workerzgodnie z definicją przyjmuje tylko jeden argument, typ pola „wejściowego” (zmienna typu x). Np. Worker IntJest typem. Zmienna typu bzamiast tego nie jest parametrem Worker, ale jest swego rodzaju „zmienną lokalną”, że tak powiem. Nie można go przekazać jako w Worker Int String- spowoduje to błąd typu.

Jeśli zamiast tego zdefiniowaliśmy:

data Worker x b = Worker {buffer :: b, input :: x}

wtedy Worker Int Stringdziałałoby, ale ten typ nie jest już egzystencjalny - teraz zawsze musimy również przekazać typ bufora.

Ponieważ Haskell jest językiem wymazywania pełnego typu, takim jak C, to skąd w Runtime wie, którą funkcję wywołać. Czy to tak, jakbyśmy zachowali kilka informacji i przekazali Ogromny V-Tabela Funkcji, a w czasie wykonywania wyliczy z V-Tabela? Jeśli tak, to jakie informacje będzie przechowywać?

Jest to mniej więcej poprawne. Krótko mówiąc, za każdym razem, gdy zastosujesz konstruktor Worker, GHC wyszukuje btyp na podstawie argumentów Worker, a następnie wyszukuje instancję Buffer b. Jeśli to zostanie znalezione, GHC dołącza dodatkowy wskaźnik do instancji w obiekcie. W najprostszej formie nie różni się to zbytnio od „wskaźnika do vtable”, który jest dodawany do każdego obiektu w OOP, gdy obecne są funkcje wirtualne.

W ogólnym przypadku może być jednak znacznie bardziej skomplikowany. Kompilator może użyć innej reprezentacji i dodać więcej wskaźników zamiast jednego (powiedzmy, bezpośrednio dodając wskaźniki do wszystkich metod instancji), jeśli przyspieszy to kod. Czasami kompilator musi także używać wielu instancji, aby spełnić ograniczenie. Na przykład, jeśli musimy zapisać instancję dla Eq [Int]..., to nie ma jednego, ale dwa: jeden dla Inti jeden dla list, a oba muszą być połączone (w czasie wykonywania, optymalizacja blokowania).

Trudno zgadnąć, co dokładnie robi GHC w każdym przypadku: zależy to od mnóstwa optymalizacji, które mogą lub nie mogą zostać uruchomione.

Możesz wypróbować googling dla „klasowej” implementacji klas typów, aby dowiedzieć się więcej o tym, co się dzieje. Możesz także poprosić GHC o wydrukowanie wewnętrznego zoptymalizowanego rdzenia -ddump-simpli obserwowanie konstruowania, przechowywania i przekazywania słowników. Muszę cię ostrzec: rdzeń ma raczej niski poziom i na początku może być trudny do odczytania.