Хабрахабр

Статически безопасная динамическая типизация à la Python

Привет, Хабр.

На днях в одном моём хобби-проекте возникла задача написания хранилища метрик.

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

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

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

Мы потребуем, чтобы тип (пусть даже и неизвестный) поддерживал сравнение в смысле упорядочивания. Естественно, мы не безумцы и не будем требовать поддержки значений совсем прям любых типов. В терминах хаскеля это означает, что мы поддерживаем такие типы a, которые реализуют тайпкласс Ord a.

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

Когда речь заходит о хранении значений, про которые известно, что они реализуют некоторый тайпкласс, в хаскеле обычно используются экзистенциальные типы:

data SomeOrd where MkSomeOrd :: Ord a => a -> SomeOrd

Так, если нам дан объект типа SomeOrd и мы сделали по нему паттерн-матчинг:

foo :: SomeOrd -> Bar
foo (MkSomeOrd val) = ... (1) ...

то в точке (1) мы не знаем, какой именно тип имеет val, но мы знаем (и, что самое главное, тайпчекер тоже знает), что val реализует тайпкласс Ord.

Однако если функции тайпкласса подразумевают два (и более) аргумента, то пользы с такой записи мало:

tryCompare :: SomeOrd -> SomeOrd -> Bool
tryCompare (MkSomeOrd val1) (MkSomeOrd val2) = ?

Получается, наш SomeOrd бесполезен. Для применения методов Ord необходимо, чтобы и val, и val2 имели один и тот же тип, но ведь это совершенно не обязано выполняться! Что же делать?

В роли рантайм-представителя типа a выступает значение типа TypeRep a, а за просьбу генерацию отвечает тайпкласс Typeable. Несмотря на то, что хаскель — компилируемый язык с агрессивным стиранием типов (после компиляции их в целом нет), компилятор всё равно может генерировать рантайм-представителей типов, если его об этом попросить.

Кстати

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

При этом если они на самом деле представляют один и тот же тип, то, очевидно, a совпадает с b. Кроме того, если у нас есть два разных экземпляра rep1 :: TypeRep a, rep2 :: TypeRep b, то мы можем их сравнить и проверить, представляют ли они один и тот же тип или нет. И, что самое главное, функция проверки представлений типов на равенство возвращает результат, способный убедить в этом тайпчекер:

eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b)

Что за ерунда здесь понаписана?

Во-первых, eqTypeRep — функция.

На это указывает часть forall k1 k2 (a :: k1) (b :: k2) — это значит, что a и b могут быть не только обычными типами вроде Int или [String], но и, например, запромоученными конструкторами (см. Во-вторых, она полиморфна, но не только по типам, но и по сортам этих типов. Но нам это всё не нужно. DataKinds и прочие потуги сделать хаскель завтипизированным).

В-третьих, она принимает два рантайм-представления потенциально разных типов, TypeRep a и TypeRep b.

Здесь происходит самое интересное. В-четвёртых, она возвращает значение типа Maybe (a :~~: b).

Если же типы таки совпадают, то функция возвращает Just val, где val имеет тип a :~~: b. Если типы не совпадают, то функция возвращает обычный Nothing, и всё в порядке. Посмотрим, что это за тип:

-- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is
-- inhabited by a terminating value if and only if @a@ is the same type as @b@.
--
-- @since 4.10.0.0
data (a :: k1) :~~: (b :: k2) where HRefl :: a :~~: a

Предположим, что мы получили значение val типа a :~~: b. Теперь давайте рассуждать. Единственный способ — при помощи конструктора HRefl, а этот конструктор требует, чтобы по обе стороны от значка :~~: стояло одно и то же. Как оно могло быть построено? Более того, если мы запаттерн-матчимся на val, то тайпчекер тоже про это будет знать. Значит, a совпадает с b. Поэтому, да, функция eqTypeRep возвращает доказательство, что два потенциально разных типа совпадают, если они на самом деле равны.

Никто не мешает нам в хаскеле написать что-то вроде Впрочем, в абзаце выше я соврал.

wrong :: Int :~~: String
wrong = wrong -- уау бесконечная рекурсия

или

wrong :: Int :~~: String
wrong = undefined

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

Оба варианта реализации wrong выше не производят это самое terminating value, что возвращает нам немного рассудка и уверенности: если наша программа на хаскеле завершилась (и не натолкнулась на undefined), то тогда её результат соответствует написанным типам. Именно поэтому в процитированном чуть выше куске документаций упомянуто terminating value. Тут, впрочем, есть некоторые детали, связанные с ленивостью, но не будем вскрывать эту тему.

В более сильных языках она бы возвращала значение более сильного типа, которое не только являлось бы доказательством равенства типов, если они на самом деле равны, но и давало бы доказательство их неравенства, если они на самом деле неравны. И, кстати, второе проявление слабости хаскеля в коде выше — тип функции eqTypeRep. Неконсистентность логики хаскеля, впрочем, делает такие функции немного бессмысленными: это всё важно, когда используешь язык как прувер теорем, а не как язык программирования, а хаскель как прувер особо не используют.

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

Это приводит нас к следующей реализации нашего типа-обёртки:

data Dyn where Dyn :: Ord a => TypeRep a -> a -> Dyn toDyn :: (Typeable a, Ord a) => a -> Dyn
toDyn val = Dyn (typeOf val) val

Теперь напишем функцию, которая принимает следующее:

  1. два значения типа Dyn;
  2. функцию, которая что-то производит для двух значений любого типа,
    основываясь только на упомянутых при создании Dyn констрейнтах (за это отвечает forall),
    и которая вызывается, если оба Dyn хранят значения одного и того же типа;
  3. и функцию-fallback, которая вызывается вместо предыдущей, если типы таки разные:

withDyns :: (forall a. Ord a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn -> Dyn -> b
withDyns f def (Dyn ty1 v1) (Dyn ty2 v2) = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2

SomeTypeRep — это экзистенциальная обёртка над TypeRep a для любого a.

Теперь мы можем реализовать, например, проверку на равенство и сравнение:

instance Eq Dyn where (==) = withDyns (==) (\_ _ -> False) instance Ord Dyn where compare = withDyns compare compare

Здесь мы воспользовались тем, что SomeTypeRep можно сравнивать между собой, так что fallback-функция для упорядочивания — тоже compare.

Готово.

Только вот теперь грех не обобщить: заметим, что внутри Dyn, toDyn, withDyns мы никак не используем конкретно Ord, и это мог бы быть любой другой набор констрейнтов, поэтому мы можем включить расширение ConstraintKinds и обобщить, параметризовав Dyn конкретным набором ограничений, которые нам нужны в нашей конкретной задаче:

data Dyn ctx where Dyn :: ctx a => TypeRep a -> a -> Dyn ctx toDyn :: (Typeable a, ctx a) => a -> Dyn ctx
toDyn val = Dyn (typeOf val) val withDyns :: (forall a. ctx a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn ctx -> Dyn ctx -> b
withDyns (Dyn ty1 v1) (Dyn ty2 v2) f def = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2

Тогда Dyn Ord будет нашим искомым типом, а, скажем, Dyn Monoid позволит хранить произвольные моноиды и что-то моноидальное с ними делать.

Напишем нужные нам инстансы для нашего нового Dyn:

instance Eq (Dyn Eq) where (==) = withDyns (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns compare compare

Тайпчекер не знает, что Dyn Ord также реализует Eq,
поэтому придётся копировать всю иерархию: … только вот это не работает.

instance Eq (Dyn Eq) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Eq (Dyn Ord) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns d1 d2 compare compare

Ну, теперь точно всё.

… разве что, в современном хаскеле можно сделать так, чтобы тайпчекер сам выводил инстансы вида

instance C_i (Dyn (C_1, ... C_n)) where ...

Stay tuned. ибо там вылезает что-то прологоподобное, но я пока этого не сделал, надо будет посидеть поковырять.

Но только в известных мне языках матчиться на тип нельзя, ибо parametricity (которая в этом случае, ИМХО, трактуется слишком широко), а тут вроде вот можно. А ещё, если внимательно прищуриться, можно заметить, что наш Dyn подозрительно похож на зависимую пару вида (ty : Type ** val : ty) из завтипизированных языков.

Например, в роли ключей можно использовать идентификаторы с описанием метрик, но это уже тема для следующей статьи. Но самое главное — теперь можно спокойно иметь что-то вроде Map (Dyn Ord) SomeValue и использовать в роли ключей любые значения, покуда они сами поддерживают сравнение.

Теги
Показать больше

Похожие статьи

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»
Закрыть