Универсальная и экзистенциальная квантификация в Haskell

В логике есть два распространенных квантора: универсальный квантор и экзистенциальный квантор. Вы можете узнать их как ∀ (для всех) и ∃ (существует).

Они актуальны и для хаскеллеров, поскольку в Haskell возможны как универсальные, так и экзистенциальные квантификаторы.

В этой статье мы рассмотрим оба типа квантификации.

Вы узнаете, как:

• Сделать универсальную квантификацию явной с помощью ExplicitForAll.
• Создавать неоднородный список с экзистенциальными типами данных.
• Использовать экзистенциально квантифицированные переменные типов, чтобы инстанцирование происходило в месте определения.

Универсальная квантификация

В Haskell все переменные типа универсально квантифицированы по умолчанию. Это происходит неявно.

В качестве примера посмотрите на функцию id.

id :: a -> a

Мы можем думать об этом как о «для всех типов aaa эта функция принимает значение этого типа и возвращает значение того же типа».

С помощью расширения ExplicitForAll мы можем записать это в явном виде.

{-# LANGUAGE ExplicitForAll #-}

id :: forall a. a -> a

Синтаксис прост — в начале объявления функции или экземпляра, до использования каких-либо ограничений или аргументов, мы используем квантификатор forall, чтобы ввести все переменные типа, которые мы будем использовать позже.

Здесь мы вводим четыре переменные: a, b, c и m:

func :: forall a b c m. a -> b -> m c -- OK, it compiles

Все переменные типа, которые вы вводите в сигнатуру типа, должны принадлежать ровно одному forall. Ни больше, ни меньше.

func :: forall a b c. a -> b -> m c -- Error, type variable `m` is not introduced

Конечно, мы также можем добавлять ограничения. Например, мы можем указать, что переменная m должна быть экземпляром типового класса Monad.

func :: forall a b c m. Monad m => a -> b -> m c

Пока что это может показаться не очень полезным. Ничего не меняется, когда мы добавляем квантификатор, потому что он уже есть (хотя и неявный). Сам по себе ExplicitForAll мало что делает.

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

Практические случаи использования универсального квантификатора

Переупорядочивание переменных типа

С помощью ExplicitForAll вы можете изменить порядок появления переменных типа в квантификаторе forall.

Почему это полезно? Представим, что вы хотите определить функцию с 10 переменными типа.

veryLongFunction :: a -> b -> c -> d -> e -> f -> g -> h -> i -> j
veryLongFunction = ...

(Да, есть реальные примеры таких функций).

И когда вы используете ее, вы хотите инстанцировать последнюю переменную типа в явном виде.

Инстанцирование

Прежде чем мы продолжим, небольшое замечание о инстанцировании переменных типа — процессе подключения типа для замены переменной типа.

Вы можете либо позволить GHC выполнить инстанцирование неявно:

fst :: forall a b. (a, b) -> a
fst (x, _) = x

pair :: (Int, String)
pair = (1, "a")

-- The argument of `fst` is of type `(Int, String)`,
-- so GHC infers how to instantiate its type variables:
-- a=Int, b=String.
x = fst pair

Или вы можете сделать это явно с помощью расширения TypeApplications:

{-# LANGUAGE TypeApplications #-}

-- Explicitly instantiate fst's first type variable to Int
-- and the second type variable to String.
x = fst @Int @String pair

TypeApplications назначает типы переменным типа в порядке их появления в (неявном или явном) forall.

Явное инстанцирование с помощью TypeApplications часто используется для того, чтобы помочь GHC, когда ему трудно определить тип, или просто для того, чтобы сделать код более читабельным.

Итак, без явного forall вы бы написали что-то вроде этого:

veryLongFunction :: a -> b -> c -> d -> e -> f -> g -> h -> i -> j
veryLongFunction = ...

func = veryLongFunction @_ @_ @_ @_ @_ @_ @_ @_ @_ @Integer ...

Довольно длинно, верно? Однако это можно упростить с помощью явного forall:

veryLongFunction :: forall j a b c d e f g h i. a -> b -> c -> d -> e -> f -> g -> h -> i -> j
veryLongFunction = ...

func = veryLongFunction @Integer ...

Поскольку j является первой переменной типа в объявлении veryLongFunction, вы можете явно инстанцировать только j и опустить остальные.

Поддержка ScopedTypeVariables

Распространенным расширением, которому требуется ExplicitForAll, является ScopedTypeVariables.

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

example :: a -> [a] -> [a]
example x rest = pair ++ rest
  where
    pair :: [a]
    pair = [x, x]

Это кажется разумным, потому что похоже, что обе функции ссылаются на одну и ту же переменную типа a. Однако на самом деле GHC вставляет неявный forall в обе функции. Другими словами, каждая функция имеет свою собственную переменную типа a.

example :: forall a. a -> [a] -> [a]
example x rest = pair ++ rest
  where
    pair :: forall a. [a]
    pair = [x, x]

Мы можем переименовать одну из этих переменных типа, чтобы сделать проблему еще более очевидной:

example :: forall a. a -> [a] -> [a]
example x rest = pair ++ rest
  where
    pair :: forall b. [b]
    pair = [x, x]

Теперь ясно, что pair — это полиморфная функция, которая обещает вернуть список любого типа b, но ее реализация на самом деле возвращает список типа a.

Мы хотели сказать, что pair должна быть мономорфной функцией, возвращающей список типа a, объявленного в example.

Чтобы исправить это, мы можем включить расширение ScopedTypeVariables. При этом переменные типа, объявленные в явном forall, будут скопированы поверх всех сопутствующих определений, например pair.

{-# LANGUAGE ScopedTypeVariables #-}

example :: forall a. a -> [a] -> [a]
example x rest = pair ++ rest
  where
    pair :: [a]
    pair = [x, x]

Выше приведены лишь два из многих примеров, где полезно использовать ExplicitForAll. Другие расширения, которые выигрывают от использования ExplicitForAll, это LiberalTypeSynonyms, RankNTypes и многие другие.

Экзистенциальная квантификация

Как было сказано ранее, помимо универсальной квантификации, Haskell также поддерживает экзистенциальную квантификацию. Это тоже можно сделать с помощью ключевого слова forall.

Это можно сделать потому, что эти две конструкции — (exists x. p x) -> q и forall x. (p x -> q) — эквивалентны в терминах логики предикатов первого порядка. Теоретическое доказательство этого утверждения вы можете найти в этой теме.

В этом разделе мы рассмотрим экзистенциальную квантификацию в типах данных и сигнатурах функций.

Экзистенциальная квантификация в типах данных

Во-первых, чтобы объявить экзистенциально квантифицированные типы данных, необходимо включить либо ExistentialQuantification, либо расширение GADTs.

Классическим мотивирующим примером являются неоднородные списки. Тип [] в Haskell представляет однородный список: список, все элементы которого имеют одинаковый тип. Вы не можете иметь список, в котором первый элемент — Int, а второй — String.

Однако вы можете эмулировать неоднородный список, обернув все элементы в экзистенциальный тип.

Вы можете определить экзистенциальный тип, используя forall в левой части имени конструктора.

data Elem = forall a. MkElem a

Это эффективно «прячет» тип элемента a внутри конструктора MkElem.

multitypedList :: [Elem]
multitypedList = [MkElem "a", MkElem 1, MkElem (Just 5)]

Однако это не очень полезно. Когда мы выполняем pattern match на MkElem, тип внутреннего значения не известен во время компиляции.

useElem :: Elem -> Int
useElem (MkElem (x :: Int)) = x + 1
                 ^^^^^^^^
-- • Couldn't match expected type ‘a’ with actual type ‘Int’

Мы ничего не можем с этим сделать, даже вывести в stdout.

printElem :: Elem -> IO ()
printElem (MkElem x) =
  print x
  ^^^^^^^
-- • No instance for (Show a) arising from a use of ‘print’
-- Possible fix:
-- add (Show a) to the context of the data constructor ‘MkElem’

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

data Elem = forall a. (Show a) => MkElem a

multitypedList :: [Elem]
multitypedList = [MkElem "a", MkElem 1, MkElem (Just 5)]

printElem :: Elem -> IO ()
printElem (MkElem x) =
  -- We can use `print` here because we have a `Show a` instance in scope.
  print x

main :: IO ()
main = forM_ multitypedList printElem

λ> "a"
λ> 1
λ> Just 5

Обратите внимание, что поскольку переменная типа a «спрятана» внутри конструктора MkElem, вы можете использовать только ограничения, объявленные в конструкторе. Вы не можете ограничивать его дальше.

allEqual :: Eq ??? => [Elem] -> Bool -- There is no type variable that you can add a constraint to.
allEqual = ...

Другим полезным примером скрытия переменных типа является обертка SomeException.

data SomeException = forall e. Exception e => SomeException e

Все исключения, когда они выбрасываются, оборачиваются в SomeException. Если вы хотите перехватить все брошенные исключения, вы можете использовать catchAll для перехвата SomeException.

Когда вы выполняете pattern match на конструкторе SomeException, его экземпляр Exception попадает в область видимости. Exception подразумевает Typeable и Show, поэтому эти экземпляры также попадают в область видимости.

exceptionHandler :: SomeException -> IO ()
exceptionHandler (SomeException (ex :: e)) =
  -- The following instances are in scope here:
  -- `Exception e`, `Typeable e`, `Show e`
  ...

Эти три экземпляра — вся информация о ex, которую мы имеем во время компиляции. К счастью, экземпляр Typeable, который у нас есть в области видимости, позволяет нам выполнять aruntime cast, и именно это делают такие функции, как catch и fromException.

Экзистенциальная квантификация в сигнатурах функций

Переменные типа функции также могут быть экзистенциально квантифицированы.

Прежде чем продолжить, давайте сначала рассмотрим типы более высокого ранга.

Типы более высокого ранга

По умолчанию Haskell98 поддерживает типы ранга-0 и ранга-1.

Типы ранга-0 — это просто мономорфные типы (также называемые монотипами), т.е. они не имеют переменных типа:

f :: Int -> Int

Типы ранга-1 имеют forall, который не появляется слева от любой стрелки. Переменные типа, связанные этим forall, универсально квантифицированы.

f :: forall a. a -> a

-- Keep in mind that the `->` operator has precedence over `.`
-- so this is equivalent to:
f :: forall a. (a -> a)

Включив расширение RankNTypes, мы открываем типы более высокого ранга. Подобно тому, как функции высшего порядка принимают в качестве аргументов другие функции, типы высшего ранга принимают в качестве аргументов типы низшего ранга.

Типы ранга 2 принимают в качестве аргумента тип ранга 1 (но не выше). Другими словами, они могут иметь forall, который появляется слева от одной стрелки. Переменные типа, связанные этим forall, экзистенциально квантифицированы.

f :: (forall a. (a -> a)) -> Int

Аналогично, типы ранга 3 принимают в качестве аргумента тип ранга 2 (но не выше). Аргумент forall находится слева от двух стрелок.

Здесь a универсально квантифицируется.

f :: ((forall a. (a -> a)) -> Int) -> Int

В общем случае:

• Тип ранга n — это функция, старший аргумент которой равен n-1.
• Переменная типа универсально квантифицирована, если она ограничена forall, появляющимся слева от четного числа стрелок.
• Переменная типа экзистенциально квантифицирована, если она ограничена forall, появляющимся слева от нечетного числа стрелок.

Вот еще один пример для наглядности:

f :: forall a. a -> (forall b. Show b => b -> IO ()) -> IO ()

Здесь f — тип ранга 2 с двумя переменными типа: универсальной переменной типа a и экзистенциальной переменной типа b.

Но что значит для переменной типа быть экзистенциально квантифицированной?

Если универсально квантифицированные переменные типа инстанцируются на «месте использования» (т.е. пользователь функции должен выбрать, какого типа он хочет видеть эту переменную типа), то экзистенциально квантифицированные переменные типа инстанцируются на «месте определения» (где определяется функция). Другими словами, определение функции свободно выбирать, как инстанцировать переменную типа; но пользователь функции — нет.

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

func :: _ -> IO ()
func log = do
  username <- getUsername
  log username

  userCount <- getUserCount
  log userCount

getUsername :: IO String
getUsername = undefined

getUserCount :: IO Int
getUserCount = undefined

main :: IO ()
main = do
  -- log to the console
  func print

  -- log to a logfile
  func (appendFile "logfile.log" . show)

Какой тип должна иметь функция log? Поскольку она записывает в журнал как String, так и Int, можно подумать, что для ее реализации достаточно добавить функцию с сигнатурой a -> IO и ограничением Show a.

log :: Show a => a -> IO ()

Однако, если мы попробуем следующее:

func :: Show a => (a -> IO ()) -> IO ()
func log = ...

Мы увидим эту ошибку компилятора:

  log username
      ^^^^^^^^
Couldn't match expected type `a` with actual type `String`...

Мы получаем эту ошибку, потому что:

2. Мы пытаемся инстанцировать его в месте определения func (log username пытается инстанцировать переменную типа a с String и log userCount пытается инстанцировать переменную типа b с Int).

Поскольку мы хотим, чтобы a инстанцировалась в месте определения func (а не в месте использования), нам нужно, чтобы a была экзистенциально квантифицирована.

{-# LANGUAGE RankNTypes #-}

func :: (forall a. Show a => a -> IO ()) -> IO ()

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

func :: (forall a. Show a => a -> IO ()) -> IO ()
func log = do
  username <- getUsername
  log @String username

  userCount <- getUserCount
  log @Int userCount

Обратите внимание, что применение типов здесь не является строго необходимым, компилятор достаточно умен, чтобы вывести нужные типы, но они помогают читабельности.

Связь между экзистенциальными типами и экзистенциально квантифицированными переменными

Наконец, следует отметить, что экзистенциальные типы изоморфны функциям с экзистенциально квантифицированными переменными (т.е. они эквивалентны), отсюда и их название.

Например, тип Elem, который мы рассматривали ранее, эквивалентен следующей функции CPS:

data Elem = forall a. Show a => MkElem a

type Elem' = forall r. (forall a. Show a => a -> r) -> r

И мы можем доказать этот изоморфизм:

elemToElem' :: Elem -> Elem'
elemToElem' (MkElem a) f = f a

elem'ToElem :: Elem' -> Elem
elem'ToElem f = f (a -> MkElem a)

Резюме

Мы рассмотрели универсальную и экзистенциальную квантификацию в Haskell. С помощью нескольких расширений и ключевого слова forall квантификация позволяет еще больше расширить богатую систему типов языка и выразить идеи, которые ранее были невозможны.

Для получения дополнительных уроков по Haskell вы можете заглянуть в наш раздел Haskell или следить за нами в Twitter.

Если вы заметили какие-либо проблемы с текстом блога или вам нужна помощь в его понимании, вы можете оставить вопрос в репозитории блога на GitHub.