6.4.7. Конструкторы данных с экзистенциальными кванторами

6.4.7.1. Почему экзистенциальная квантификация?

Какое отношение это имеет к экзистенциальной квантификации? Просто MkFoo имеет (почти) изоморфный тип

MkFoo :: (exists a . (a, a -> Bool)) -> Foo

Однако программисты на Haskell могут без опасений считать, что используется приведённый выше обычный тип с универсальными кванторами, и тем самым избежать добавления новой конструкции экзистенциальной квантификации.

6.4.7.2. Экзистенциальная квантификация и классы типов

Простое расширение — разрешить произвольные контексты перед конструктором. Например:

data Baz = forall a. Eq a => Baz1 a a
         | forall b. Show b => Baz2 b (b -> b)

Два конструктора имеют ожидаемые типы:

Baz1 :: forall a. Eq a => a -> a -> Baz
Baz2 :: forall b. Show b => b -> (b -> b) -> Baz

При сопоставлении с образцом для Baz1 сопоставленные значения можно сравнивать на равенство, а при сопоставлении с образцом для Baz2 первое сопоставленное значение можно преобразовать в строку (а также применить к нему функцию). Поэтому эта программа допустима:

f :: Baz -> String
f (Baz1 p q) | p == q    = "Yes"
             | otherwise = "No"
f (Baz2 v fn)            = show (fn v)

В реализации с передачей словарей конструкторы Baz1 и Baz2 должны хранить словари для Eq и Show соответственно и извлекать их при сопоставлении с образцом.

6.4.7.3. Конструкторы записей

GHC позволяет использовать экзистенциальную квантификацию и в синтаксисе записей. Например:

data Counter a = forall self. NewCounter
    { _this    :: self
    , _inc     :: self -> self
    , _display :: self -> IO ()
    , tag      :: a
    }

Здесь tag — общедоступное поле с корректно типизированной функцией-селектором tag :: Counter a -> a. Полное описание того, как определяются типы селекторов полей верхнего уровня, см. в разделе Селекторы полей и TypeApplications.

Тип self скрыт извне; любая попытка использовать _this, _inc или _display как функции приведёт к ошибке компиляции. Иными словами, GHC определяет функцию-селектор записи только для полей, тип которых не упоминает экзистенциально квантифицированные переменные. (В этом примере для полей, для которых не будут определены селекторы записей, использовано подчёркивание, но это лишь стиль программирования; GHC их игнорирует.)

Чтобы использовать эти скрытые поля, нужно создать вспомогательные функции:

inc :: Counter a -> Counter a
inc (NewCounter x i d t) = NewCounter
    { _this = i x, _inc = i, _display = d, tag = t }

display :: Counter a -> IO ()
display NewCounter{ _this = x, _display = d } = d x

Теперь можно определить счётчики с разными внутренними реализациями:

counterA :: Counter String
counterA = NewCounter
    { _this = 0, _inc = (1+), _display = print, tag = "A" }

counterB :: Counter String
counterB = NewCounter
    { _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }

main = do
    display (inc counterA)         -- prints "1"
    display (inc (inc counterB))   -- prints "##"

Для экзистенциальной квантификации (и GADT) поддерживается синтаксис обновления записи:

setTag :: Counter a -> a -> Counter a
setTag obj t = obj{ tag = t }

Правило обновления записи таково:

типы обновляемых полей могут упоминать только универсально квантифицированные переменные типа конструктора данных. Для GADT поле может упоминать только типы, которые встречаются в типе результата конструктора в качестве простого аргумента-переменной типа.

Например:

data T a b where { T1 { f1::a, f2::b, f3::(b,c) } :: T a b } -- c is existential
upd1 t x = t { f1=x }   -- OK:   upd1 :: T a b -> a' -> T a' b
upd2 t x = t { f3=x }   -- BAD   (f3's type mentions c, which is
                        --        existentially quantified)

data G a b where { G1 { g1::a, g2::c } :: G a [c] }
upd3 g x = g { g1=x }   -- OK:   upd3 :: G a b -> c -> G c b
upd4 g x = g { g2=x }   -- BAD (g2's type mentions c, which is not a simple
                        --      type-variable argument in G1's result type)

6.4.7.4. Ограничения

Существует несколько ограничений на использование конструкторов с экзистенциальными кванторами.

• При сопоставлении с образцом каждое сопоставление вводит новый, отдельный тип для каждой экзистенциальной переменной типа. Эти типы нельзя унифицировать ни с каким другим типом, и они не могут выйти за пределы области видимости сопоставления с образцом. Например, следующие фрагменты некорректны:

  f1 (MkFoo a f) = a
  

  Здесь тип, связанный с MkFoo, «вытекает» за пределы области видимости, поскольку a является результатом f1. Чтобы понять, почему это неверно, спросим, какой тип имеет f1:

  f1 :: Foo -> a             -- Weird!
  

  Что это за «a» в типе результата? Очевидно, имеется в виду не следующее:

  f1 :: forall a. Foo -> a   -- Wrong!
  

  Исходная программа просто некорректна. Вот другой тип ошибки:

  f2 (Baz1 a b) (Baz1 p q) = a==q
  

  Допустимо написать a==b или p==q, но a==q — ошибка, поскольку это приравнивает два разных типа, возникающих из двух конструкторов Baz1.

• Нельзя сопоставлять с образцом конструктор с экзистенциальными кванторами в группе связываний let или where. Поэтому следующий код недопустим:

  f3 x = a==b where { Baz1 a b = x }
  

  Вместо этого используйте выражение case:

  f3 x = case x of Baz1 a b -> a==b
  

  В общем случае сопоставлять с образцом конструктор с экзистенциальными кванторами можно только в выражении case или в образцах определения функции. Причина этого ограничения связана с реализацией. Проверка типов групп связываний и без усложнения экзистенциальными кванторами уже доставляет массу трудностей. Кроме того, связывание с образцом, содержащим экзистенциальный квантор, на верхнем уровне модуля не имеет смысла, поскольку неясно, как предотвратить «выход» экзистенциально квантифицированного типа за пределы области видимости. Поэтому пока действует простое для формулировки ограничение. Посмотрим, насколько оно неудобно.

• Нельзя использовать экзистенциальную квантификацию в объявлениях newtype. Поэтому следующий код недопустим:

  newtype T = forall a. Ord a => MkT a
  

  Причина: значение типа T должно представляться парой из словаря для Ord t и значения типа t. Это противоречит идее о том, что newtype не должен иметь конкретного представления. Такого же эффекта и эффективности можно добиться, используя data вместо newtype. Если перегрузка не используется, есть больше оснований разрешить экзистенциально квантифицированный newtype, поскольку вариант data действительно связан с затратами на реализацию. Однако конструкторы с одним полем и экзистенциальным квантором мало полезны. Поэтому простое ограничение (никакой экзистенциальной квантификации в newtype) остаётся в силе, если не появятся убедительные причины его изменить.

• Нельзя использовать deriving для определения экземпляров типа данных с конструкторами данных, содержащими экзистенциальные кванторы. Причина в том, что в большинстве случаев это не имело бы смысла. Например:

  data T = forall a. MkT [a] deriving( Eq )
  

  Чтобы стандартным способом вывести Eq, потребовалось бы сравнивать на равенство единственный компонент двух конструкторов MkT:

  instance Eq T where
    (MkT a) == (MkT b) = ???
  

  Но a и b имеют разные типы, поэтому их нельзя сравнить. Можно придумать примеры, в которых выведенный экземпляр имел бы смысл, но гораздо проще просто запретить такие объявления. Определяйте собственные экземпляры!