GADT предоставляют ясный и лучший синтаксис для кода с использованием экзистенциальных типов, предоставляя неявные поля
. Я думаю, что существует общее согласие, что синтаксис GADT лучше. Я бы не сказал, что это потому, что GADT предоставляют неявные данные, а скорее потому, что оригинальный синтаксис, включенный с расширением ExistentialQuantification, потенциально сбивает с толку / вводит в заблуждение. Этот синтаксис, конечно, выглядит следующим образом:
data SomeType = forall a. SomeType a
или с ограничением:
data SomeShowableType = forall a. Show a => SomeShowableType a
, и я думаю, что консенсус заключается в том, что использование ключевого слова forall здесь позволяет тип, который легко спутать с совершенно другим типом:
data AnyType = AnyType (forall a. a) -- need RankNTypes extension
Для лучшего синтаксиса могло бы использоваться отдельное ключевое слово exists, поэтому вы должны написать:
data SomeType = SomeType (exists a. a) -- not valid GHC syntax
GADT Синтаксис, используется ли он с неявным или явным forall, более равномерен для этих типов и, кажется, легче для понимания. Даже с явным forall следующее определение наталкивается на мысль о том, что вы можете взять значение любого типа a и поместить его в мономорф c SomeType':
data SomeType' where
SomeType' :: forall a. (a -> SomeType') -- parentheses optional
и Легко увидеть и понять разницу между этим типом и:
data AnyType' where
AnyType' :: (forall a. a) -> AnyType'
Экзистенциальные типы, кажется, не интересуются типом, который они содержат, но сопоставление с образцом говорит, что существует какой-то тип, который мы не используем. Мы не знаем, какой это тип, до тех пор, пока мы не используем Typeable или Data.
Мы используем их, когда хотим скрыть типы (например, для гетерогенных списков), или мы не знаем, что это за типы во время компиляции. .
Полагаю, это не так уж и далеко, хотя вам не нужно использовать Typeable или Data для использования экзистенциальных типов. Я думаю, что было бы точнее сказать, что экзистенциальный тип предоставляет хорошо типизированную «рамку» вокруг неопределенного типа. Блок в некотором смысле «скрывает» тип, что позволяет составлять гетерогенный список таких блоков, игнорируя типы, которые они содержат. Оказывается, что неограниченный экзистенциал, такой как SomeType' выше, довольно бесполезен, но ограниченный тип:
data SomeShowableType' where
SomeShowableType' :: forall a. (Show a) => a -> SomeShowableType'
позволяет вам сопоставлять паттерны, чтобы заглянуть внутрь «окна» и сделать доступными объекты класса типов :
showIt :: SomeShowableType' -> String
showIt (SomeShowableType' x) = show x
Обратите внимание, что это работает для любого класса типов, а не только Typeable или Data.
Что касается вашего замешательства по поводу страницы 20 слайд-колоды, автор говорит, что для функции , которая требует экзистенциального Worker, невозможно потребовать Worker, имеющий конкретный Buffer экземпляр. Вы можете написать функцию для создания Worker, используя определенный тип Buffer, например 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
, но если вы напишите функцию, которая принимает Worker в качестве аргумента, она может использовать только общие средства класса Buffer (например, функция output):
doWork :: Worker Int -> IO ()
doWork (Worker b x) = output (show x) b
Он не может пытаться требовать, чтобы b был конкретным типом буфера, даже через сопоставление с образцом:
doWorkBroken :: Worker Int -> IO ()
doWorkBroken (Worker b x) = case b of
MemoryBuffer -> error "try this" -- type error
_ -> error "try that"
Наконец, информация времени выполнения об экзистенциальных типах становится доступной через неявные аргументы «словаря» для участвующих классов типов. Приведенный выше тип Worker, в дополнение к наличию полей для буфера и ввода, также имеет невидимое неявное поле, которое указывает на словарь Buffer (что-то вроде v-таблицы, хотя оно вряд ли огромно, поскольку содержит только указатель в соответствующую output функцию).
Внутри класс типа Buffer представлен как тип данных с функциональными полями, а экземпляры являются «словарями» этого типа:
data Buffer' b = Buffer' { output' :: String -> b -> IO () }
dBuffer_MemoryBuffer :: Buffer' MemoryBuffer
dBuffer_MemoryBuffer = Buffer' { output' = undefined }
Экзистенциальный тип имеет скрытое поле для этого словаря:
data Worker' x = forall b. Worker' { dBuffer :: Buffer' b, buffer' :: b, input' :: x }
, а функция типа doWork, которая работает с экзистенциальными значениями Worker', реализована следующим образом:
doWork' :: Worker' Int -> IO ()
doWork' (Worker' dBuf b x) = output' dBuf (show x) b
Для класса типов только с одной функцией словарь фактически оптимизирован для нового типа, поэтому в этом примере экзистенциальный тип Worker включает скрытое поле, состоящее из указателя функции на функцию output для буфера, и это единственная информация о времени выполнения, необходимая для doWork.