6.4.6. Существенно квантифицированные конструкторы данных

6.4.6.1. Почему существенная квантификация?

Что это имеет общего с существенной квантификацией? Просто то, что MkFoo имеет (почти) изоморфный тип

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

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

6.4.6.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.6.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 "##"

Синтаксис обновления записей поддерживается для существенных квантификаторов (и GADТ):

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

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

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

Например:

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.6.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 имеют разные типы и поэтому не могут быть сравнены. Можно вообразить примеры, в которых полученный экземпляр имел бы смысл, но проще просто запретить такие объявления. Определяйте собственные экземпляры!