Разъяснение экзистенциальных типов в Haskell

Я пытаюсь понять экзистенциальные типы в Haskell и наткнулся на PDF http://www.ii.uni.wroc.pl/~dabi/courses/ZPF15/rlasocha/prezentacja.pdf

Пожалуйста, исправьте мои следующие понимания, которые у меня есть до сих пор.

• Экзистенциальные типы, кажется, не интересуются типом, который они содержат, но соответствующие им шаблоны говорят, что существует некоторый тип, который мы не знаем, какой это тип, до тех пор, пока мы не используем Typeable или Data.
• Мы используем их, когда хотим скрыть типы (например, для гетерогенных списков) или не знаем, что это за типы во время компиляции.
• GADT«s обеспечить четкое и лучший синтаксис кода , используя экзистенциальные типы путем предоставления неявных forall» S

Мои сомнения

• На странице 20 вышеупомянутого PDF для приведенного ниже кода упоминается, что для функции невозможно требовать определенный буфер. Почему это так? Когда я пишу функцию, я точно знаю, какой буфер я буду использовать, даже если не знаю, какие данные я в нее помещу. Что плохого в том, :: Worker MemoryBuffer Intчтобы иметь Если они действительно хотят абстрагироваться от Buffer, они могут иметь тип Sum data Buffer = MemoryBuffer | NetBuffer | RandomBufferи иметь тип:: 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

• Поскольку Haskell является языком полного типа Erasure, таким как C, то как он узнает во время выполнения, какую функцию вызывать. Это что-то вроде того, что мы собираем немного информации и передаем Огромную V-Таблицу Функций, а во время выполнения это выяснит из V-Таблицы? Если это так, то какую информацию она будет хранить?

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и поместить его в мономорфизм 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Типа выше, в addtion к наличию поля для буфера и входа, а также имеет невидимую неявное поле , которое указывает на Bufferсловарь (несколько , как у-таблицы, хотя это вряд ли огромный, так как он просто содержит указатель на соответствующую 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.

На странице 20 вышеупомянутого PDF для приведенного ниже кода упоминается, что для функции невозможно требовать определенный буфер. Почему это так?

Поскольку Worker, как определено, принимает только один аргумент, тип поля ввода (переменная типа x). Например Worker Int, это тип. Переменная типа b, напротив, не является параметром Worker, а является своего рода «локальной переменной», так сказать. Это не может быть передано как в Worker Int String- это вызвало бы ошибку типа.

Если мы вместо этого определили:

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

тогда Worker Int Stringбудет работать, но тип больше не является экзистенциальным - теперь мы всегда должны также передавать тип буфера.

Поскольку Haskell является языком полного типа Erasure, таким как C, то как он узнает во время выполнения, какую функцию вызывать. Это что-то вроде того, что мы собираем немного информации и передаем Огромную V-Таблицу Функций, а во время выполнения это выяснит из V-Таблицы? Если это так, то какую информацию она будет хранить?

Это примерно правильно. Вкратце, каждый раз, когда вы применяете конструктор Worker, GHC выводит bтип из аргументов Worker, а затем ищет экземпляр Buffer b. Если это найдено, GHC включает дополнительный указатель на экземпляр в объекте. В своей простейшей форме это не слишком отличается от «указателя на vtable», который добавляется к каждому объекту в ООП при наличии виртуальных функций.

В общем случае все может быть гораздо сложнее. Компилятор может использовать другое представление и добавить больше указателей вместо одного (скажем, непосредственное добавление указателей ко всем методам экземпляра), если это ускоряет код. Кроме того, иногда компилятору необходимо использовать несколько экземпляров для удовлетворения ограничения. Например, если нам нужно сохранить экземпляр для Eq [Int]... тогда существует не один, а два: один для Intи один для списков, и эти два нужно объединить (во время выполнения, за исключением оптимизации).

Трудно догадаться, что именно делает GHC в каждом случае: это зависит от тонны оптимизаций, которые могут или не могут сработать.

Вы можете попробовать поискать в «словарной» реализации классов типов, чтобы узнать больше о том, что происходит. Вы также можете попросить GHC напечатать внутреннее оптимизированное Ядро -ddump-simplи наблюдать, как создаются, хранятся и передаются словари. Я должен предупредить вас: ядро ​​довольно низкого уровня, и поначалу его трудно прочитать.