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.