ExistentialQuantification давайте скроем переменную типа. Это можно было бы сделать для единообразного управления разными типами значений.
Антипаттерн класса экзистенциального типа
В Haskell воссоздание антипаттерна класса экзистенциального типа является почти ритуалом. Вот как это происходит.
Вы хотите составить список вещей, которые можно показать, например:
map show [1, 'h', True] -- This won't compile
За исключением того, что Haskell не может напрямую создавать список разных типов. Однако вы можете составить список показываемых вещей. ExistentialQuantification поможет вам в этом:
data Showable = forall a. Show a => Showable a instance Show Showable where show (Showable x) = show x
Showable - это тип, который скрывает тип a с помощью количественной оценки существования, которая должна иметь Show экземпляр. Теперь мы можем создать список из Showable вещей:
map show [Showable1,Showable'h',Showable True] -- compiles!
Так что все кажется хорошо, за исключением того, что это был очень косвенный способ написать:
[show 1, show 'h', show True]
Хуже того, типы с экзистенциальными типами не являются стандартными типами, поэтому работать с ними труднее, чем с типами Haskell 2010 (обратите внимание, что я не смог получить экземпляр Show).
Антипаттерн класса экзистенциального типа задерживает использование методов класса типа с дополнительным типом-оболочкой, но мы можем просто сделать вызовы функций заранее. Если нам действительно нужно отложить выполнение метода, мы можем без особого труда: Haskell ленив.
Шаблон 1: Промежуточное значение
Как только вы поймете, что создание унифицированного типа для приложения метода класса типов не является хорошим использованием классов типов, возникает вопрос о том, что такое хорошее использование.
Шаблон «Промежуточное значение» - это способ скрыть ненужный тип, который используется внутри функции (-ями).
Хороший пример - тип Fold из пакета foldl:
data Fold a b -- | @Fold @ @ step @ @ initial @ @ extract@ = forall x. Fold (x -> a -> x) x (x -> b)
Тип Fold содержит начальное значение x (второй аргумент конструктора). При первом вызове «шага» (первый аргумент) ему передается начальное x, и результатом «шага» является обратная связь с самим собой снова и снова. Наконец, в конце вычисления результат «шага» (x) преобразуется в b последним аргументом «извлечение».
После создания Fold невозможно определить тип x. Хотя это нормально. Важно только то, что x того же типа, что и для функций «step» и «extract».
Тип x выставлять незачем. Если бы Fold был Fold x a b вместо Fold a b, это сделало бы библиотеку излишне сложной в использовании (и в некоторых случаях невозможной для написания) без реальной пользы.
Другой пример этого паттерна - свободный аппликатив (шляпа Дэвида Ривера).
Паттерн 2: скрытые типы, которые можно скрыть
Основное правило состоит в том, что, когда кто-то скрывает тип с экзистенциальным, его нельзя получить. Однако это еще не все.
В GHC есть функция, называемая равенством типов, которая включается несколькими расширениями, одним из которых является GADTs.
При равенстве типов я могу написать конструктор:
data Hideable a = a ~ Int => IntHideable a
| a ~ Char => CharHideable
Тогда я могу скрыть a новым типом и экзистенциальным:
data AnyHideable = forall a. AnyHideable (Hideable a)
Если я сопоставлю образец на AnyHideable, я не буду знать, какой у меня тип Hideable.
incHideable :: Hideable Int -> Int incHideable (IntHideable x) = x + 1 foo :: AnyHideable -> IO () foo (AnyHideable x) = case x of -- x is of type Hideable a ...
Однако, когда я сопоставляю шаблон в конструкторе IntHideable, он переносит ограничение a ~ Int в область видимости.
incHideable :: Hideable Int -> Int
incHideable (IntHideable x) = x + 1
foo :: AnyHideable -> IO ()
foo (AnyHideable x) = case x of
IntHideable {} -> print $ incHideable x -- x is a (Hideable Int)
...
На этом этапе компилятор будет знать, что Hideable a на самом деле Hideable Int, и я могу использовать на нем incHideable.
Хорошо, это надуманный пример. Дело в том, что мы можем перейти от унифицированного типа AnyHideable и восстановить информацию о типе Hideable a. Экзистенциально количественно определенный AnyHideable может быть приятным, потому что мы относимся к нему единообразно, но если мы хотим работать с конкретным Hideable, мы можем сделать это с помощью сопоставления с образцом.
Большинство Haskeller не видели, чтобы равенство типов использовалось таким образом, но это потому, что GHC имеет хороший синтаксис для таких типов, в основном синтаксис GADT. Тот же тип, написанный с синтаксисом GADT, выглядит так:
data Hideable a where IntHideable :: Int -> Hideable Int CharHideable :: Char -> Hideable Char
Под капотом творится такая же магия равенства.
Обновление от 29 мая: Дэвид Фойер указал на Reddit, что есть еще несколько примеров, которые я обсуждаю ниже.
Паттерн 3: Структуры данных, выровненные по типу
Структуры данных с выравниванием по типу позволяют создавать списки, последовательности, деревья и другие структуры данных, в которых новые данные совпадают с типами старых данных.
Здесь я создаю выровненный по типу список для хорошо типизированных путей между состояниями TCP. Я создаю вид и отдельные типы для состояний (State), и каждый переход или стрелка на диаграмме состояний является конструктором в GADT (тип Path).
data State = Closed | Listen | SynSent | SynReceived | Established
| CloseWait | LastAck | FinWait1 | FinWait2 | Closing
| TimeWait
data Path :: State -> State -> * where
ServerStart :: Path Closed Closed
PassiveOpen :: Path Closed Listen
ServerClose :: Path Listen Closed
ServerSynRecieved :: Path Listen SynReceived
ClientSynRecieved :: Path SynReceived SynReceived
SynResponded :: Path SynReceived Established
ToFinWait1 :: Path Established FinWait1
ActiveOpen :: Path Closed SynSent
PassiveToActive :: Path Listen SynSent
ClientClose :: Path SynSent Closed
FinishHandshake :: Path SynSent Established
PassiveClose :: Path Established CloseWait
ToLastAck :: Path CloseWait LastAck
EarlyClose :: Path SynReceived FinWait1
ActiveClose :: Path Established FinWait1
SimulatanousClose :: Path FinWait1 Closing
SimulatanousCloseAck :: Path Closing TimeWait
FastClose :: Path FinWait1 TimeWait
CloseAcknowledge :: Path FinWait1 FinWait2
FinishClose :: Path FinWait2 TimeWait
Waited :: Path TimeWait Closed
(:::) :: Path a b -> Path b c -> Path a c
connectAndClose :: Path Closed Closed
connectAndClose = ServerStart ::: ActiveOpen ::: ClientClose
Количественная оценка существования неявно используется в конструкторе :::, чтобы скрыть промежуточные типы (b). connectAndClose - это пример действительного пути, который проходит через Closed, SynSent и обратно в Closed состояния. Промежуточное состояние SynSent должно совпадать, но оно не отображается в типе connectAndClose.
Структуры данных, выровненные по типу, могут использоваться для создания программ с более точным типом и могут привести к улучшениям алгоритмов (см. Отражение без сожалений).
Отношение к RankNTypes
В квантификации существования используется синтаксис forall почти неотличимым отRankNTypes способом. Это приводит многих хаскеллеров к выводу, что они похожи на расширения. Хотя экзистенциальная количественная оценка использует один и тот же синтаксис, она используется для разных целей (даже если да, полиморфизм более высокого ранга может кодировать экзистенциальную количественную оценку).
Вывод
ExistentialQuantification - это способ GHC скрыть информацию о типе. В некоторых ситуациях эту информацию можно восстановить или можно скрыть информацию вместе с функциями для работы со скрытым типом. Если держаться подальше от антипаттерна класса экзистенциального типа, есть шанс, что ExistentialQuantification не будут так часто использоваться. Это нормально.
