Статически безопасная динамическая типизация à 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) = ?

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

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

Кроме того, если у нас есть два разных экземпляра rep1 :: TypeRep a, rep2 :: TypeRep b, то мы можем их сравнить и проверить, представляют ли они один и тот же тип или нет. При этом если они на самом деле представляют один и тот же тип, то, очевидно, a совпадает с 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). Здесь происходит самое интересное.

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

-- | 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, а этот конструктор требует, чтобы по обе стороны от значка :~~: стояло одно и то же. Значит, a совпадает с b. Более того, если мы запаттерн-матчимся на val, то тайпчекер тоже про это будет знать. Поэтому, да, функция eqTypeRep возвращает доказательство, что два потенциально разных типа совпадают, если они на самом деле равны.

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

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

или

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

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

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

И, кстати, второе проявление слабости хаскеля в коде выше — тип функции 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.

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

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

Автор: 0xd34df00d

Источник