Данные высокого рода +16


Да-да, вам не привиделось и вы не ослышались — именно высокого рода. Род (kind) — это термин теории типов, означающий по сути тип типа [данных].

Но вначале немного лирики.

На Хабре вышло несколько статей, где подробно описывался метод валидации данных в функциональных языках.

Эта статься — мои пять копеек в этот хайп. Мы рассмотрим валидацию данных в Хаскеле.

Валидация типом


Ранее было рассмотрен пример методики валидации при помощи валидации типом:

type EmailContactInfo  = String
type PostalContactInfo = String

data ContactInfo = EmailOnly EmailContactInfo | 
                   PostOnly PostalContactInfo | 
                   EmailAndPost (EmailContactInfo, PostalContactInfo)

data Person = Person 
  { pName :: String,
  , pContactInfo :: ContactInfo,
  }

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

Валидация данными высокого рода




В этой статье мы посмотрим иной метод валидации — при помощи данных высокого рода.

Пусть у нас есть тип данных:

data Person = Person
  { pName :: String
  , pAge  :: Int
  }

И мы будем валидировать данные лишь в том случае, когда валидны все поля записи.
Поскольку Хаскель по функциональным возможностям на голову превосходит большинство функциональных языков, на нём можно легко избавится от большинства рутины.

Тут можно и поэтому данный метод широко используется среди авторов библиотек на Хаскеле.

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

Один из способов моделирования — использовать второй тип данных:

data MaybePerson = MaybePerson
  { mpName :: Maybe String
  , mpAge  :: Maybe Int
  }

где, напомню используется опциональный тип:

-- already in Prelude
data Maybe a = Nothing | Just a

Отсюда функция валидаци получается достаточно простой:

validate :: MaybePerson -> Maybe Person
validate (MaybePerson name age) =
  Person <$> name <*> age

Чуть детальнее о функциях (<$>) и (<*>)
Функция (<$>) — это лишь инфиксный синоним Функтора fmap

-- already in Prelude
fmap :: Functor f => (a -> b) -> f a -> f b

(<$>) :: Functor f => (a -> b) -> f a -> f b
(<$>) = fmap

И (<*>) — это функция применения Аппликативного Функтора

-- already in Prelude
(<*>) :: Applicative f => f (a -> b) -> f a -> f b

И для опционального типа эти функции имеют следующее определение

-- already in Prelude
(<$>) :: (a -> b) -> Maybe a -> Maybe b
_ <$> Nothing   = Nothing
f <$> (Just a)  = Just (f a)

(<*>) :: Maybe (a -> b) -> Maybe a -> Maybe b
(Just f) <*> m   = f <$> m
Nothing  <*> _   = Nothing


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

СЮРПРИЗ! ОН МОЖЕТ! Нам поможет высокий род!

В Хаскеле есть такое понятие как род, он же kind, и самое простое и достаточно точное объяснение то, что род — это тип типа [данных]. Самый широко используемый род — *, которого можно назвать «конечным»

ghci> :k Int
Int :: *

ghci> :k String
String :: *

ghci> :k Maybe Int
Maybe Int :: *

ghci> :k Maybe String
Maybe String :: *

ghci> :k [Int]
[Int] :: *

А какой род у Maybe?
ghci> :k Maybe
Maybe :: * -> *

ghci> :k []
[] :: * -> *

Это и есть пример высокого рода.

Обратите внимание, что мы можем описать как Person, так и MaybePerson следующим единственным данным высокого рода:

data Person' f = Person
  { pName :: f String
  , pAge  :: f Int
  }

Здесь мы параметризуем Person' над чем-то f (с родом * -> *), что позволяет нам сделать следующее, чтобы пользоваться исходными типами:

type Person = Person' Identity
type MaybePerson = Person' Maybe

Тут мы используем простой обёрточный тип Идентичности

-- already in Prelude
newtype Identity a = Identity { runIdentity :: a }

Хотя это работает, но немного раздражает в случае Person, так как теперь все наши данные обернуты внутри Identity:

ghci> :t pName @Identity
pName :: Person -> Identity String

ghci> :t runIdentity. pName
runIdentity. pName :: Person -> String

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

{-# LANGUAGE TypeFamilies #-}

-- "Higher-Kinded Data"
type family HKD f a where
  HKD Identity a = a
  HKD f        a = f a

data Person' f = Person
  { pName :: HKD f String
  , pAge  :: HKD f Int
  } deriving (Generic)

Вывод Generic нам нужно для 2й части статьи.

Использование семьи типов HKD означает, что GHC автоматически стирает любые обертки Identity в наших представлениях:

ghci> :t pName @Identity
pName :: Person -> String

ghci> :t pName @Maybe
pName :: Person -> Maybe String

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

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

Мы теперь можем переписать её с помощью нашей новой техники:

validate :: Person' Maybe -> Maybe Person
validate (Person name age) =
  Person <$> name <*> age

Не очень интересное изменение? Но интрига заключается в том, как мало нужно менять. Как вы можете видеть, только наш тип и шаблон совпадают с нашей первоначальной реализацией. Что здесь аккуратно, так это то, что мы теперь консолидировали Person и MaybePerson в одно и то же представление, и поэтому они больше не связаны только в номинальном смысле.

Generics и более общая функция валидации


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

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

Можно было бы использовать Шаблонный Хаскель (TemplateHaskell), но он порождает код и используется лишь в крайних случаях. Мы не будем.

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

Мы в итоге хотим получить что-то вроде:

validate :: _ => d Maybe -> Maybe (d Identity)

С точки зрения Generics любой тип наиболее обще можно разделить на несколько конструкций:

-- undefined data, lifted version of Empty
data    V1        p
-- Unit: used for constructors without arguments, lifted version of ()
data    U1        p = U1
-- a container for a c, Constants, additional parameters and recursion of kind *
newtype K1    i c p = K1 { unK1 :: c } 
-- a wrapper, Meta-information (constructor names, etc.)
newtype M1  i t f p = M1 { unM1 :: f p } 

-- Sums: encode choice between constructors, lifted version of Either
data    (:+:) f g p = L1 (f p) | R1 (g p) 
-- Products: encode multiple arguments to constructors, lifted version of (,)
data    (:*:) f g p = (f p) :*: (g p) 

То есть могут существовать неинецилизированные структуры, безаргументные структуры, константные структуры, мета-информационные (конструкторы и др). А так же объединения структур — суммарные или объединения типа ИЛИ-ИЛИ и мультипликационные, они же кортержные объединения или записи.

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

{-# LANGUAGE MultiParamTypeClasses #-}

class GValidate i o where
  gvalidate :: i p -> Maybe (o p)

Можно использовать «мягкие и медленные» правила для рассуждений о том, как должен выглядеть ваш тип класса, но в целом вам понадобится как входной, так и выходной параметр. Они оба должны быть рода * -> *, а затем передавать этот экзистенциализированный p, благодаря темным, нечестивым причинам, известных не человечеству. Затем пользуясь небольшим контрольным списком, проходим, чтобы помочь обернуть голову вокруг этого кошмарного адского ландшафта, который мы обойдём позже последовательно.

Во всяком случае, наш класс уже у нас в руках, теперь просто нужно выписывать экземпляры нашего класса для разных типов GHC.Generic. Мы можем начать с базового случая, который мы должны уметь проверять, а именно Maybe k:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators     #-}

instance GValidate (K1 a (Maybe k)) (K1 a k) where
  -- gvalidate :: K1 a (Maybe k) -> Maybe (K1 a k)
  gvalidate (K1 k) = K1 <$> k
  {-# INLINE gvalidate #-}

K1 представляет собой «константный тип», что означает, что именно здесь заканчивается наша структурная рекурсия. В примере с нашим Person' это будет pName :: HKD f String.

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

Мы можем начать с мультипликативных структур — если мы имеем GValidate i o и GValidate i' o', мы должны иметь возможность запускать их параллельно:

instance (GValidate i o, GValidate i' o')
    => GValidate (i :*: i') (o :*: o') where
  gvalidate (l :*: r) = (:*:)
                    <$> gvalidate l
                    <*> gvalidate r
  {-# INLINE gvalidate #-}

Если K1 относится непосредственно к селекторам нашего Person', (: * :) примерно соответствует синтаксису запятой, которой мы разделяем наши поля в записи.

Мы можем определить аналогичный экземпляр GValidate для копроизведений или суммарных структур (соответствующие значения разделяются | в определении данных):

instance (GValidate i o, GValidate i' o')
    => GValidate (i :+: i') (o :+: o') where
  gvalidate (L1 l) = L1 <$> gvalidate l
  gvalidate (R1 r) = R1 <$> gvalidate r
  {-# INLINE gvalidate #-}

Кроме того, раз мы не заботимся о поиске метаданных, мы можем просто определить GValidate i o над конструктором метаданных:

instance GValidate i o
    => GValidate (M1 _a _b i) (M1 _a' _b' o) where
  gvalidate (M1 x) = M1 <$> gvalidate x
  {-# INLINE gvalidate #-}

Теперь остались неинтересные нам структуры для полного описания. Им предоставим следующие тривиальные экземпляры для нежилых типов (V1) и для конструкторов без каких-либо параметров (U1):

instance GValidate V1 V1 where
  gvalidate = undefined
  {-# INLINE gvalidate #-}

instance GValidate U1 U1 where
  gvalidate U1 = Just U1
  {-# INLINE gvalidate #-}

Использование undefined здесь безопасно, поскольку его можно вызвать только со значением V1. К счастью для нас, V1 необитаем и неинициализирован, поэтому этого никогда не может произойти, значит мы морально правы в нашем использовании undefined.

Без дальнейших церемоний, теперь, когда у нас есть весь этот механизм, мы можем, наконец, написать не-общую версию валидации:

{-# LANGUAGE FlexibleContexts #-}

validate
    :: ( Generic (f Maybe)
       , Generic (f Identity)
       , GValidate (Rep (f Maybe))
                   (Rep (f Identity))
       )
    => f Maybe
    -> Maybe (f Identity)
validate = fmap to . gvalidate . from

Каждый раз можно получить широкую улыбку, когда подпись для функции длиннее фактической реализации; это означает, что мы наняли компилятор для написания кода за нас. Что здесь важно для валидации, так это то, что в нем нет упоминаний о Person'; эта функция будет работать для любого типа, определенного как данные высокого рода. Вуаля!

Итоги


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

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

Счастливого применения высоких родов!

Оригинал: Higher-Kinded Data

Вы можете помочь и перевести немного средств на развитие сайта



Комментарии (7):

  1. Dair_Targ
    /#19343352 / +2

    Интересная статья! Спасибо за перевод.


    После прочтения остался вопрос: тут вся валидация — это проверка того, что Maybe-поля обязательно присутствуют. Интересно было бы взглянуть на примеры, когда:


    1. Нужно проверить, что возраст не меньше 18, а имя написано латиницей
    2. Имя должно начинаться на "Ы", если возраст между 34 и 42 годами, и на "Ъ", если возраст между 101 и 111 годами
    3. Получить не Maybe Person, а Either WhyInvalid Person с описанием того, почему проверка не понравилась.

    Примерно так обычно выглядит продуктовая валидация исходя из моего опыта — поэтому и интересно взглянуть на то, как Higher-Kinded Data помогает в этих случаях.

    • Vitter
      /#19344356

      На третий вопрос — проще, чем кажется. Вместо типа Person' Maybe надо использовать тип Person' (Either WhyInvalid). И дописать обобщёную функции валидации для типа Either (отличатья будет не телом функции, лишь типом).
      Что касается первого и второго вопроса — валидировать поля можно при заполнении типа Person' Maybe.

      mPerson :: Perosn' Maybe
      mPerson = Peson {
        ...
        pAge = readMaybe ioAge >= (\age -> if age< 18 then Nothing else Just age),
       ...
      }
      

      Более подробно — можете глянуть мою статью Зачем нужны все эти функторы и монады?
      Что касается более вычурной валидации — просто вынести валидацию из тела записи в дополнительную функцию
      mPerson :: Perosn' Maybe
      mPerson = 
        let pAge = readMaybe ioAge >= (\age -> if age < 18 then Nothing else Just age) in
        let pName = pAge >= (\age -> 
            if age > 34 && age < 42 then ... 
            else if age > 101 && age < 11 then ...
            else ... ) in
        Peson {
      ...
      pName = pName,
      pAge = pAge,
      ...
      }
      

  2. 0xd34df00d
    /#19346270 / +1

    Идея с HKD и отдельным инстансом для Identity красивая, утащил себе в копилку паттернов, спасибо!


    Впрочем, эта статья скорее не совсем про валидацию, а про то, как представлять валидированные данные и получать их из невалидированных. То есть, логика валидации остаётся где-то там, в стороне. И в типах не выражается гарантии, что бизнес-логика не сделает вдруг из валидных данных невалидные где-то по ходу дела.

  3. iokasimov
    /#19349030

    Я прочитал статью несколько раз и все равно ничего не понял. Какую задачу тут помогли решить поднятые до «родов» (впервые слышу такой перевод, я привык к «видам») параметризованные типы данных?

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

    -- Этот код будет работать и для Identity, так как Identity так же имеет экземпляр класса Applicative:
    Person <$> name <*> age
    


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

    • Vitter
      /#19351890

      Хороший вопрос.
      1) Род или вид — ещё нет устойчивых наименований, я всё же склоняюсь к наименованиям русскоязычной теории категорий
      2) Мы всё же поднимаем параметры не до родов, поскольку любой тип итак имеет род (как правило звёздочку), а до более высоких родов (чем звёздочка)
      3) Ответ на основной ваш вопрос — для того, чтоб совместить 2 типа данных(или более) в один.
      4) Да, существует функтор для Identity, но функцию validate мы применяем к Person' Maybe, а не Person' Identity

      • iokasimov
        /#19352186

        1) Я сомневаюсь, что kind как-то вообще связан с теорией категорий (может вы спутали с теорией типов?), скиньте мне пожалуйста ссылку, если я не прав.
        2) Параметризованные типы — это типы, имеющие параметры, а не сами параметры.
        3) Какие 2 типа данных имеются ввиду? И зачем иметь два разных типа?
        4) Я не имел ввиду функцию `validate`. Не думаю, что это выглядит как ответ на вопрос.

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

        • Vitter
          /#19352332

          1) упс, сори, да, теория типов
          2) это не противоречит тому, что сказал я
          3) Зачем 2 разных типа — это отдельный вопрос. Person' Maybe и Person' Identity
          4) функторы/мондаы/… спокойно проникают сквозь обёртку Identity. При этом нет необходимости разворачивать Identity а в а, это делает за нас семейство типов.
          Об этом была моя предыдущая статья Великая сила newtypes про coerce

          Как на меня — это прекрасная статья для ознакомления с семьями/семействами типов, высокими родами и генериками. Пример мышления далеко ЗА императивным мышлением