Мономорфизм, полиморфизм и экзистенциальные типы

Роман Душкин

Аннотация: В статье описываются экзистенциальные типы данных и их применение в функциональной парадигме программирования. Даются определения необходимых понятий — мономорфизма, полиморфизма (высших рангов) и их связи с экзистенциальными типами. Примеры определений типов и функций для их обработки приводятся в основном на языке программирования Haskell.


Article describes the notion of existential types and related theoretical concepts (monomorphism, polymorphism, etc), with examples in Haskell.



Обсуждение статьи ведётся по адресу
http://community.livejournal.com/fprog/8541.html.

1  Введение

Настоящая статья продолжает цикл публикаций, посвящённых различным свойствам и аспектам систем типизации, используемых в функциональных языках программирования. Желательно, чтобы перед прочтением данной статьи читатель ознакомился с предыдущими материалами [6, 7].

Одним из наиболее интересных и важных понятий в парадигме функционального программирования является параметрический полиморфизм. В статье [7] дана классификация подвидов параметрического полиморфизма, основанная на работах [1, 5]. В целях удобства имеет смысл привести основные определения здесь, несколько расширив их.

При декларациях параметрических полиморфных типов применяются связанные типовые переменные (или переменные типов). При дальнейшем использовании таких полиморфных типов типовые переменные конкретизируются определёнными типами — происходит подстановка значения переменной в виде конкретного типа (примерно так же, как происходит подстановка конкретного значения в λ-терм при β-редукции). Другими словами, типовые переменные могут рассматриваться в качестве формальных параметров, которые получают значения аргументов в процессе конкретизации.

В зависимости от того, какие значения могут принимать типовые переменные, различают два подвида параметрического полиморфизма:

  1. Предикативный параметрический полиморфизм проявляется тогда, когда в качестве значений типовых переменных могут быть подставлены только мономорфные типы («монотипы»), то есть такие типы, в определениях которых не используются типовые переменные.
  2. Непредикативный параметрический полиморфизм позволяет конкретизировать типовые переменные произвольными типами (мономорфными и полиморфными), в том числе и рекурсивно: если в определении типа τ используется типовая переменная α, то при конкретизации вместо неё может быть подставлен сам тип τ. В данном случае слово «непредикативный» обозначает, что при определении сущности возможно использование ссылки на саму определяемую сущность, что потенциально может привести к парадоксам типа канторовского и расселовского. Иногда непредикативный полиморфизм называют полиморфизмом первого класса.

Существует еще одна система классификации параметрических полиморфных типов, основаная на понятии ранга. В данной классификации выделяют три подвида параметрического полиморфизма:

  1. Полиморфизм ранга 1 (также предварённый полиморфизм или let-полиморфизм) предполагает, что в качестве типовых переменных могут быть подставлены только монотипы. Соответственно, предварённый полиморфизм может быть только предикативным. В языках семейства ML (включая язык Haskell стандарта 98 года без расширений) используется именно этот вид параметрического полиморфизма.
  2. Полиморфизм ранга k (при k > 1) позволяет конкретизировать типовые переменные полиморфными типами ранга не выше (k - 1). В [2] доказано, что вывод типов возможен для k = 2, но для больших k задача вывода типов неразрешима.
  3. Полиморфизм высшего ранга (полиморфизм ранга N) проявляется тогда, когда конкретизация типовых переменных может производиться произвольными типами, в том числе и полиморфными любого ранга. Непредикативный полиморфизм высшего ранга является наиболее общим видом параметрического полиморфизма.

В языках функционального программирования со статической типизацией чаще всего используется предикативный предварённый полиморфизм, так как он проще всего обрабатывается при автоматическом выводе типов. Этот вид параметрического полиморфизма был впервые реализован в языке программирования ML, после чего успешно показал себя в других языках. В частности, как уже упомянуто, стандарт Haskell-98 использует именно его.

Тем не менее, этот подвид не позволяет решать часто возникающие в программировании задачи, связанные, например, с хранением в контейнерных типах данных значений различных типов. В языках с динамической типизацией, таких как LISP, нет никаких проблем в создании списочных структур, элементами которых могут быть как атомы, так и другие списочные структуры. При этом в качестве атомов могут одновременно выступать значения разных типов — и значения истинности, и символы, и значения численных типов. Но подобные структуры данных невозможны в языке Haskell стандарта Haskell-98. Тип [a] при конкретизации (получении конкретного значения типовой переменной a) сможет содержать значения только того типа, которым конкретизирована типовая переменная. Невозможно создать список, в котором одновременно будут содержаться и числа, и символы, и иные произвольные значения.

Для преодоления этого ограничения компилятор GHC предлагает расширения языка, позволяющие использовать так называемые экзистенциальные типы (от англ. «existential types»). Эти типы и являются предметом рассмотрения данной статьи.

2  Пара нетривиальных задач для статически типизированных языков

Статическая типизация предполагает, что типы всех выражений, используемых в программе, известны на этапе компиляции. При этом типы могут быть либо явно указаны разработчиком, либо вычислены самим компилятором при помощи механизма вывода типов (с автоматическим выводом типов можно ознакомиться в [9], где также имеется обширный список литературы по данной тематике). Это накладывает ряд ограничений на способы определения структур данных и функций для их обработки.

Одна из главных трудностей, с которой сталкивается разработчик на языке программирования ML, Haskell или подобном, заключается в невозможности создать так называемые неоднородные типы (или, как их ещё называют, гетерогенные типы, от англ. «heterogeneous types»). Неоднородными типами называются такие типы, которые могут содержать в себе значения разных типов. Например, неоднородные списки могут одновременно содержать целые числа, символы, другие списки, деревья и т. д., неоднородные двоичные деревья могут содержать в своих вершинах значения совершенно произвольных типов. При этом надо отметить, что разные значения находятся в рамках одного конструктора, то есть по своей сути гетерогенные типы уже не являются «классическими» алгебраическими типами данных, как они описаны в [6].

Как упомянуто во введении, в языках с динамической типизацией создание таких типов данных не является проблемой. Язык LISP изначально оперирует именно такими структурами данных. В языке программирования JavaScript также можно без проблем определять массивы, каждый элемент которых имеет тип, отличающийся от типов других элементов.

К сожалению, функциональные статически типизированные языки программирования не позволяют просто так создавать неоднородные типы. Например, в языке Haskell сигнатура

f :: [a] -> a

представляет собой сигнатуру полиморфной функции. При вызове такой функции происходит конкретизация типа a и все экземпляры типовой переменной в этой сигнатуре получают одно и то же значение. Другими словами, первый компонент сигнатуры [a] представляет собой список значений типа a, поэтому при конкретизации типа все элементы списка будут обязаны иметь один и тот же тип. Это требование становится понятным, если вспомнить определение списка1:

data [a] = [] | a : [a]

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

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

Хорошо, если все типы таких программных сущностей составляют достаточно ограниченное множество, тогда на языке Haskell можно определить алгебраический тип данных, каждый из конструкторов которого отвечает за одну «разновидность» обрабатываемой сущности. Но как быть, если функции-обработчики необходимо создавать динамически? И каким образом в изначально однородный список положить неоднородные данные, типы которых могут быть неизвестны на стадии компиляции?

Ответы на эти вопросы в процедурных и объектно-ориентированных языках программирования несложны. В языке C можно просто использовать список указателей на void, а при получении очередного объекта через такой указатель вызывать необходимую функцию для его обработки на основании некоторой метаинформации, приходящей с каждым объектом. В объектно-ориентированных языках программирования для этих целей имеется специальный метод, который так и называется — динамическая диспетчеризация [4].

В качестве примера можно привести задачу вывода на экран географической карты. Файл с описанием карты представляет собой поток разнообразных фигур — точек, линий, полигонов, эллипсов и т. д. Решение этой задачи на языке C++ обычно приводят в учебниках по этому языку в части, описывающей механизм наследования. Создаётся базовый класс TFigure, у которого имеется виртуальный метод render. От класса TFigure наследуются разнообразные классы TPoint, TLine, TPolygon, TEllipse и т. д. по количеству используемых для описания карты фигур. В функцию-диспетчеризатор передаётся список значений типа TFigure, для каждой из которых вызывается метод render, а механизм динамической диспетчеризации позаботится о том, чтобы был вызван правильный метод, связанный с конкретным типом фигуры.

Другой задачей, где традиционные строго типизированные функциональные языки терпят фиаско по сравнению с императивным подходом, является работа с изменяемым состоянием. Опасности изменяемого состояния, а также некоторые методы исключения таких опасностей из разрабатываемых программных продуктов приведены в статье [8]. Тем не менее, некоторые алгоритмы не могут быть эффективно реализованы без изменяемых состояний, а некоторые задачи вообще могут быть «извращены» при помощи использования неизменяемых программных сущностей.

Работа с изменяемыми состояниями в процедурных и объектно-ориентированных языках программирования не представляет никакой сложности, поскольку в самой императивной парадигме одним из главных методов работы с объектами является так называемое «деструктивное присваивание» — прямая замена содержимого ячейки памяти, на которую ссылается объект. В императивной парадигме программирования операция присваивания значения является столь широко используемой, что разработчик не задумывается о том, сколько раз и как часто он меняет состояния используемых в его программном продукте объектов.

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

Из-за необходимости реализации системы ввода-вывода в языке программирования Haskell появляется «неуклюжая» монада IO, которая обеспечивает ввод и вывод, то есть вводит в язык Haskell недетерминированные функции ввода и функции вывода с побочными эффектами. Получается противоречивая ситуация: язык Haskell идеологически объявлен чистым (то есть недопускающим недетерминизма и использования побочных эффектов), но в то же время подсистема ввода-вывода необходима ему для обеспечения универсальности. Из-за этого монада IO в языке Haskell сделана обособленной — ввод и вывод может осуществляться только в ней. В других функциональных языках программирования подсистемы ввода-вывода также основаны на каких-нибудь допущениях.

Далее в статье будут рассмотрены приёмы использования экзистенциальных типов, дающие ответы на следующие вопросы:

  1. Каким образом можно определить и в дальнейшем использовать неоднородные типы данных?
  2. Что можно сделать для создания в рамках функциональной парадигмы безопасных механизмов работы с изменяемым состоянием, которые в то же время оставались бы в рамках чистоты и детерминизма?

3  Экзистенциальные типы и их использование в языке Haskell

Как же экзистенциальные типы позволяют ответить на поставленные в предыдущем разделе вопросы?

3.1  Неоднородные типы

Неоднородные контейнерные структуры данных (неоднородные типы) позволяют хранить значения различных типов, никак не связанных друг с другом. Задача создания таких структур данных достаточно легко решается в объектно-ориентированном стиле при помощи механизма наследования и динамической диспетчеризации. Но эта же задача оказывается нетривиальной для функциональной парадигмы.

В языке Haskell, например, несложно определить нужное количество алгебраических типов данных, каждый из которых является экземпляром какого-нибудь одного специального класса типов. Этот общий класс предоставит для типов общие интерфейсные методы. Однако задачи это не решит — каким образом упаковать значения этих различных типов в один контейнер? Мономорфный тип этого не позволит, поскольку при конкретизации типовой переменной будет выбран только один тип из всего множества, пусть хотя бы каждый тип из этого множества имеет экземпляр одного и того же класса.

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

id :: a -> a

В предыдущей статье цикла [7] уже показана математическая формула для этой функции, а именно:

  # (id ≡ Λ α . λ xα . x) = ∀ α . α → α     (1)

Здесь используется квантор всеобщности (), присутствующий в нотации языка Haskell неявно (в действительности надо было бы написать так: id :: forall a . a -> a).

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

Что было бы, если бы была возможность ставить квантор всеобщности в произвольном месте сигнатуры, связывая типовую переменную только в определённой её части? Это позволило бы не упоминать её в сигнатуре самого алгебраического типа.

Теперь можно обратиться к задаче из предыдущего раздела о выводе на экран географической карты. Нет необходимости определять единый алгебраический тип данных наподобие следующего:

data Figure = Point (Int, Int) | Line (Int, Int) (Int, Int) | Polygon [(Int, Int)] | Ellipse (Int, Int) Int Int

Это решение было бы крайне плохо масштабируемо, поскольку для добавления поддержки нового типа фигур пришлось бы дополнять этот тип, что приводило бы к необходимости значительного рефакторинга всего программного проекта. Вместо этого имеет смысл определить класс, содержащий функцию render (результатом выполнения которой может являться отображение фигуры на экране):

class Figure a where render :: a -> IO ()

Для работы с этим классом необходимо подготовить набор специальных алгебраических типов данных и экземпляров класса Figure для них.

data Point = Point (Int, Int) instance Figure Point where render (Point (x, y)) = ...

И так для каждого типа фигур, составляющих карту и выводимых на экран. Это решение уже является вполне естественным для языка Haskell и хорошо масштабируется — в любой момент можно определить дополнительные типы фигур и реализовать для них экземпляры класса Figure.

Но как же быть с организацией неоднородной структуры данных? Здесь и приходят на помощь экзистенциальные типы. Для создания неоднородного списка, который будет содержать все считанные из файла геометрические фигуры, необходимо определить экзистенциальный тип-обёртку:

data GeoObject = forall a . Figure a => GeoObject a

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

Ключевое слово forall не входит в стандарт Haskell-98, поэтому для его использования необходимо подключить дополнительные языковые расширения, например, так:

{-# LANGUAGE ExistentialQuantification #-}

Теперь при помощи типа GeoObject можно определить неоднородный список объектов, составляющих географическую карту:

geolist :: [GeoObject] geolist = [GeoObject (Point (0, 0)), GeoObject (Line (1, 1) (2, 2)), GeoObject (Polygon [(1, 1), (1, -1), (-1, -1), (-1, 1)]), GeoObject (Ellipse (0, 0) 1 1)]

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

dispatch :: [GeoObject] -> IO () dispatch [] = return () dispatch ((GeoObject g):gs) = do render g dispatch gs

Или ещё проще:

dispatch :: [GeoObject] -> IO () dispatch = sequence_ . map render

Как теперь видно, благодаря использованию экзистенциального типа из функции dispatch исчезает типовая переменная. Но сама по себе эта функция уже не может считаться мономорфной — типовая переменная вместе с квантором всеобщности скрыта в определении экзистенциального типа GeoObject. Таким образом функция dispatch оказывается полиморфной функцией ранга 2, поскольку её параметром является полиморфный объект ранга 1 — список элементов, каждый из которых сам по себе является полиморфным объектом ранга 0, то есть имеет монотип.

Функция dispatch не знает, значения каких типов могут содержаться в качестве объектов неоднородного списка типа [GeoObject]. Это общее свойство полиморфизма — использующие программные сущности не могут знать типов используемых объектов (поскольку эти типы вообще могут быть не конкретизированы в случае полиморфизма высших рангов). Поэтому всё, что может делать функция с получаемыми на вход объектами неизвестных типов, это применять к ним какие-либо заведомо применимые функции. Именно поэтому важно либо иметь общий интерфейс для таких типов (ограничение на наличие экземпляра одного и того же класса), либо на вход диспетчеризатору фактическим параметром передавать функцию для обработки значений соответствующего типа.

3.2  Работа с изменяемыми состояниями в функциональном стиле

Один из «отцов-основателей» языка Haskell С. Л. Пейтон-Джонс в своё время озаботился трудностями манипулирования изменяемым состоянием в этом языке и разработал монаду ST (от англ. «State Transformer» — преобразователь состояний), совмещающую в себе свойства монад IO и State. Детально библиотека, реализующая данную монаду, описана в работе [3].

В контексте данной статьи монада ST интересна тем, что реализует работу с изменяемым состоянием, но в совершенно функциональном стиле, сохраняя все важные свойства и принципы функциональной парадигмы: независимость результата от порядка вычислений, ссылочную прозрачность, ленивость, возможность извлечения объектов из монады ST (то есть, возможность получить «чистое» значение в результате вычисления с состоянием в монаде ST). Как видно, эти свойства вполне отвечают требованиям, поставленным в предыдущем разделе, и позволяют заявить, что в языке Haskell имеется чисто функциональный инструмент для эффективного решения императивных задач.

В цели настоящей статьи не входит подробное описание монады ST. Интересен другой её аспект — реализация монады ST основана на параметрическом полиморфизме ранга 2.

Тип «действия» (от англ. «action») в монаде ST таков:

ST s a

Здесь тип a возвращается «действием» типа s. Самое интересное — сигнатура функции, позволяющей извлечь значение из монады ST:

runST :: (forall s . ST s a) -> a

Как видно, в этой сигнатуре используется параметрический полиморфизм ранга 2. Квантор всеобщности для типовой переменной s находится не на самом верхнем уровне, как для типовой переменной a (для неё квантор всеобщности в сигнатуре не показан, поскольку он подразумевается), а на один уровень ниже. Это скрывает типовую переменную s, а используемые для работы конкретные типы становятся неизвестны вне монады ST, что и обеспечивает безопасность типизации.

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

import Data.STRef import Control.Monad import Control.Monad.ST productST :: Num a => [a] -> a productST xs = runST $ do n <- newSTRef 1 mapM_ (\x -> modifySTRef n (* x)) xs readSTRef n

Вызов функции productST приводит к выполнению последовательности из трёх монадических действий, записанных после ключевого слова do. Результат выполнения этой последовательности находится в монаде ST, поэтому для получения «чистого» значения из этой монады используется функция runST. Сама функция productST ничего не знает о том, как именно и с какими возможными побочными эффектами производятся вычисления внутри монады ST, всё это сокрыто от неё посредством использования экзистенциального типа и параметрического полиморфизма ранга 2.

Последовательность монадических действий в функции productST написана во вполне императивном духе. Первое действие — запись в именованное состояние («переменную») n начального значения 1. Далее производятся циклические вычисления при помощи функции mapM_, для каждого элемента x из списка xs выполняется действие modifySTRef n (* x). Это действие модифицирует значение «переменной» n при помощи заданной функции (в данном случае — (* x), то есть операции умножения на очередное значение из списка). Императивный аналог этого фрагмента кода — n = n * x.

Третье монадическое действие считывает значение, хранящееся в «переменной» n, и возвращает его. Далее это значение, обёрнутое монадой ST, попадает на вход функции runST, которая, как уже сказано, возвращает его в чистом виде.

Чтобы понять способ выполнения циклических монадических действий, имеет смысл привести определения используемых для этого функций (благо они совершенно краткие):

mapM_ :: Monad m => (a -> m b) -> [a] -> m () mapM_ f xs = sequence_ (map f xs) sequence_ :: Monad m => [m a] -> m () sequence_ xs = foldr (>>) (return ()) xs

Здесь функции map и foldr являются стандартными. Знак подчёркивания (_) в наименованиях монадических функций указывает на то, что функции игнорируют результаты вычислений, но используют только побочные эффекты выполняемых монадических действий. Функция sequence_ выполняет последовательность монадических действий, хранящихся в заданном списке. Функция mapM_ строит такой список при помощи заданной функции f и исходного списка, после чего передаёт построенный список монадических действий функции sequence_.

Теперь читатель вполне готов реализовать другие функции обработки списков в подобном квази-императивном стиле.

Таким образом использование в определении монады ST экзистенциального типа позволяет решить важную задачу — сокрытие реального типа действий, используемых в монаде. Обработка этих действий может производиться только средствами, предоставленными монадой (функциями, написанными её разработчиками). Это значит, что налицо определение абстрактного типа данных. И действительно, экзистенциальные типы в данном отношении используются в качестве инструмента повышения уровня абстрактности — реальный тип используемых выражений неизвестен, а потому их обработка может вестись только посредством имеющегося в наличии «интерфейса». Если обратиться к более раннему примеру с динамической диспетчеризацией, то в нём это свойство экзистенциальных типов проявляется ещё нагляднее, поскольку определённый класс Figure предоставляет интерфейс для обработки неоднородного списка.

4  Заключение

В данной статье лишь кратко рассказано про отдельные аспекты применения параметрического полиморфизма высших рангов и экзистенциальных типов в языке программирования Haskell. Предложенные примеры демонстрируют решения задач, которые не могут быть эффективно решены традиционными методами функционального программирования (использование неоднородных структур данных и работа с изменяемым состоянием в функциональном стиле). Это открывает читателю новые направления изучения систем типов, используемых в информатике как в теории, так и на практике.

Дополнительно надо отметить, что одной из важнейших теоретических основ для изучения и использования параметрического полиморфизма является так называемая «Система F». Этому формализму будет посвящена одна из грядущих статей.

Автор благодарит своих коллег Д. А. Антонюка и Е. Р. Кирпичёва за помощь, оказанную ими при подготовке данной статьи.

Список литературы

[1]
Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17:471–522, 1985.
[2]
Kfoury A. J. and Wells J. B. Principality and decidable type inference for finite-rank intersection types. ACM Symposium on Principles of Programming Languages (POPL), pages 161–174, 1999.
[3]
Launchbury J. and Peyton-Jones S. L. Lazy functional state threads. Programming Languages Design and Implementation, 1994.
[4]
Lippman S. B. Inside the C++ Object Model. Addison-Wesley, 1996.
[5]
Benjamin C. Pierce. Types and Programming Languages. The MIT Press, Cambridge, Massachusetts, 2002. в сети Интернет по адресу http://newstar.rinet.ru/~goga/tapl/ опубликован перевод книги на русский язык.
[6]
Душкин Р. В. Алгебраические типы данных и их использование в программировании. «Практика функционального программирования», 2(2):86–105, 2009.
[7]
Душкин Р. В. Полиморфизм в языке Haskell. «Практика функционального программирования», 3(3):67–81, 2009.
[8]
Кирпичёв Е. Р. Изменяемое состояние: опасности и борьба с ними. «Практика функционального программирования», 1(1):29–49, 2009.
[9]
Кирпичёв Е. Р. Элементы функциональных языков. «Практика функционального программирования», 3(3):83–196, 2009.

1
Необходимо напомнить, что данное определение некорректно с точки зрения синтаксиса языка Haskell, оно «вшито» в язык в подобном виде. Разработчик не может создавать собственные определения типов подобного вида.
2
Пример этот, конечно, искусственный — реализовать подобную функцию очень легко и без использования монады ST. Тем не менее, он иллюстрирует использование императивного стиля в функциональном языке.

Этот документ был получен из LATEX при помощи HEVEA