В процессе написания программ мы часто сталкиваемся с данными, для которых возможен только ограниченный набор значений. Например, возраст, который не может быть отрицательным или email, который может иметь только определенный формат строки. При использовании примитивных типов (Int
, String
) приходится писать различные валидаторы, поскольку такие типы:
могут представлять все что угодно
могут содержать все что угодно
Тут еще можно упомянуть антипаттерн Primitive Obsession.
Если у нас есть некоторая функция, которая принимает в аргументы имя, email и возраст, описанные примитивными типами:
def foo(name: String, email: String, age: Int) = {
// что-то делаем с name, email и age
}
Пользователь или мы сами можем случайно передать ей некорректные значения.
val result = foo("???", "", -20) // не ок
Добавление валидации в самом примитивном виде может выглядеть как то так.
def foo(name: String, email: String, age: Int) = {
if (!validateName(name) || !validateEmail(email) || !validateAge(age))
// Ошибка валидации
// Если валидация прошла успешно, то используем name, email и age
}
Теперь функция foo
делает не только то, для чего она действительно была создана, но еще и ответственна за то, чтобы в ней производилась валидация (тем самым нарушая первый принцип SOLID).
Может помогут псевдонимы типов (Type alias)?
Псевдонимы типов не помогут, поскольку они так же продолжают представлять примитивные типы.
type Name = String
type Email = String
type Age = Int
def foo(name: Name, email: Email, age: Age) = ???
val name: Name = "Mark"
val email: Email = "mark@email.com"
val age: Age = 42
foo(name, email, age) // ок
foo(email, name, age) // вообще не ок
И компилятор не сможет сообщить, что мы допустили ошибку, случайно поменяв email
и name
местами.
А value class-ы?
Обернув примитивные типы в кейс-классы (тем самым создав спец. типы), мы не можем просто так взять и подсунуть Name
вместо Email
.
final case class Name(value: String) extends AnyVal
final case class Email(value: String) extends AnyVal
final case class Age(value: Int) extends AnyVal
def foo(name: Name, email: Email, age: Age) = ???
foo(Name("Mark"), Email("mark@email.com"), Age(42)) // ок
foo(Email("mark@email.com"), Name("Mark"), Age(42)) // ошибка компиляции
// type mismatch;
// found : org.github.ainr.experiments.Main.Email
// required: org.github.ainr.experiments.Main.Name
Но эти типы все еще могут принимать любые значения.
val email = Email("blah blah blah") // не ок
Используем refined (уточненные) типы
Refined - это небольшая библиотека для Scala, позволяющая описать тип с помощью предикатов, ограничивающих набор значений, который может принимать этот тип.
Для использования refined-типов необходимо подключить библиотеку refined добавив следующую строчку в build.sbt
libraryDependencies += "eu.timepit" %% "refined" % "0.9.27"
Предварительно проверив не появилась ли версия поновее.
Начнем с чего-нибудь простого. Например, возраст не может быть отрицательным числом. С помощью предиката NonNegative
уточняем тип Int
создав при этом тип Age
.
import eu.timepit.refined.api.Refined
import eu.timepit.refined.auto._
import eu.timepit.refined.numeric._
type Age = Int Refined NonNegative
При попытке присвоить значение несоответствующее предикату код даже не скомпилируется.
val age: Age = -1
// Predicate (-1 < 0) did not fail.
// val positiveInteger: Age = -1
Так же предикаты могут быть скомбинированы. К примеру, тут создается тип, который может принимать только положительные нечетные числа.
type OddPositive = Int Refined (Odd And Positive)
val anOddPositive: OddPositive = 3
Refined очень полезен для уточнения строковых типов с помощью готовых предикатов.
val nonEmptyString: NonEmptyString = ""
// Predicate isEmpty() did not fail.
// val nonEmptyString: NonEmptyString = ""
type URL = String Refined Url
val url: URL = "http://github.com"
type EndsWithDot = String Refined EndsWith["."]
val endsWithDot: EndsWithDot = "Hello world."
Так и предикатов на основе самодельных регулярных выражений.
type Name = String Refined MatchesRegex["""[A-Z][a-z]+"""]
type Email = String Refined MatchesRegex["""(\w)+@([\w\.]+)"""]
Взаимодействие с библиотеками
Давайте рассмотрим пример взаимодействия с другими библиотеками, например circe, который используется для работы с json. Допустим, что у нас есть некоторый сервис с методом /api/foo
через который с фронта прилетает json. Нам нужно преобразовать этот json в кейс-класс Foo
поля которого имеют refined-типы.
import eu.timepit.refined.api.Refined
import eu.timepit.refined.string._
import eu.timepit.refined.numeric._
type Name = String Refined MatchesRegex["""[A-Z][a-z]+"""]
type Email = String Refined MatchesRegex["""(\w)+@([\w\.]+)"""]
type Age = Int Refined NonNegative
case class Foo(name: Name, email: Email, age: Age)
Для того чтобы circe мог работать с refined-типами ему требуются инстансы с кодеками для refined-типов. Они определены в отдельном расширении circe-refined
для подключения которого нужно добавить следующую строчку в build.sbt
.
libraryDependencies += "io.circe" %% "circe-refined" % "0.14.1"
И сделать импорт там, где будет выполняться json-преобразование.
import io.circe.generic.auto._, io.circe.parser._
import io.circe.refined._
val json =
"""
|{
| "name": "Martin",
| "email": "martin?email.com", // ошибка
| "age": 55
|}
|""".stripMargin
val decodedFoo: Either[circe.Error, Foo] = decode[Foo](json)
// Left(DecodingFailure(Predicate failed: "martin?email.com".matches("(\w)+@([\w\.]+)")., List(DownField(email))))
Собственно, если json будет содержать некорректные значения, то мы в результате получим Either
с ошибкой декодирования (DecodingFailure
).
Неполный список доступных расширений для интеграции различных библиотек с refined-типами приведен в документации.
И кстати, преобразование примитивных типов в refined-типы в рантайме происходит примерно следующим способом.
import eu.timepit.refined.api.RefType
import eu.timepit.refined.api.Refined
import eu.timepit.refined.string._
type Email = String Refined MatchesRegex["""(\w)+@([\w\.]+)"""]
val badEmail = "bad email"
val email = RefType.applyRef[Email](badEmail)
// email = Left(Predicate failed: "bad email".matches("(\w)+@([\w\.]+)").)
Вместо заключения
Целью этого небольшого поста ставил обозначить проблему, для решения которой были созданы refined-типы и продемонстрировать некоторые возможности библиотеки.
Более подробно с примерами и списком предикатов можно ознакомиться в гитхабе проекта.
Комментарии (33)
0xd34df00d
23.08.2021 02:04+5Может ли предикат у типа зависеть от другого значения? Например, может ли у меня там рядом с возрастом быть поле «стаж», которое не больше этого возраста?
XoJIoD
23.08.2021 10:34Для этого вы можете использовать паттерн Smart Constructor (https://medium.com/@supermanue/smart-constructors-in-scala-fa5a03e25326) совместно с Refined
0xd34df00d
23.08.2021 18:38+2Smart constructor заставляет меня опираться на корректность логики в конструкторе, и после того, как эта логика выполнилась, никаких свидетельств её выполнения у меня нет. Если упрощать, нельзя написать весь прочий код так, чтобы я удалил соответствующий
if
в этом умном конструкторе, а компилятор на меня ругнулся.
pecheny
23.08.2021 06:24+3В качестве попытки немного обобщить и систематизировать вводную часть. Когда мы хотим определить некоторый тип через констрейны, чтобы сузить круг возможных значений, то есть два принципиально разных взаимодополняющих подхода: валидация данных в рантайме и валидация во время компиляции.
Пример ручного написания рантайм-валидации как демонстрация нарушения SRP мне кажется притянутым за уши – достаточно вынести валидацию в отдельный метод.
Если я правильно понял, то предложенная библиотека сочетает в себе генерацию валидаторов и их использование и для генерации рантайм-бойлерплейта, и для проверки доступных литералов во время компиляции.
Первый вопрос – это вариация вопроса 0xd34df00d, который в общем случае сведется к зависимым типам. А именно: есть ли у нас, например, возможнасть имея два NonNegative в компайл-тайме получать NonNegative в результате их сложения, но не получать в результате разности? Получать в результате разности только если первое значение больше/равно второго?
Теперь к разделу про взаимодействие с библиотеками. (Побуду занудой, пример, похоже не о «взаимодеиствии с библиотеками вообще», а о «взаимодействии с библиотеками, зависящими от refined» – это немного другое). Вопрос второй – по «case class Foo».
Скалу я не знаю, но знаю, что case-классы в ней – это реализация ADT плюс некоторые особенности. В данном примере кейс-класс с единственным конструктором используется из-за каких-то дополнительных особенноестей? Можно ли использовать просто value-классы или обычные мутабельные классы?
Сам я больше работаю с haxe, поэтому приведу встречные примеры, присущие этому языку. Во-первых в языке есть абстрактные типы – компайл-тайм абстрацкии над другими типами с zero-cost оверхэдом, которые среди прочего позволяют писать рантайм-валидации в теле конструтора. После компиляции тело конструктора/методов/операторов по желанию либо заинлайнятся, либо вынесутся в статический метод. Кроме того, над абстрактами можно определять операции над любыми комбинациями с другими типами. То есть в примере с NonNegative мы легко можем определить операцию сложения с гарантиями компилятора, но для вычетания – только сгенерировать рантайм-проверки. Так как зависимых типов тут нет.
Алгебраические типы в haxe тоже есть, но с абстрактами они никак не связаны и могут использоваться с ними в сочетании в любых комбинациях.
Кроме того, у haxe есть удобный апи для метапрограммирования, который позволяет делать описанное в статье. В качестве примера могу привести коллекцию библиотек haxetink.github.io.XoJIoD
23.08.2021 10:46Добавить перегруженные методы для refined типа можно, через обычные extension methods, сильно специфического для Refined ничего в этом плане нет, кроме "поднятия" обернутого типа
Зависимые типы в Scala есть, поэтому разницу двух NonNegatives на этапе компиляции сделать можно, если это литералы (значения известны также на этапе компиляции)
Refined это сторонняя библиотека и в плане использования типов ничем не отличается от любых других типов, будь то в кейс или обычных классах и полях0xd34df00d
23.08.2021 18:01+1Зависимые типы в Scala есть, поэтому разницу двух NonNegatives на этапе компиляции сделать можно, если это литералы (значения известны также на этапе компиляции)
Это не зависимые типы. Для полных завтипов это же можно сделать и для значений, известных только в рантайме (и вычитание тоже в рантайме, конечно).
XoJIoD
23.08.2021 18:04Каким образом? Вот я ввел с консоли два NonNegative, как ваш код вернет NonNegative для x - y?
0xd34df00d
23.08.2021 18:15+1А у меня компилятор потребует в компил-тайме наличия рантайм-проверки, что одно из них меньше другого.
При этом, например, если в одном месте мне нужно получить
x - y
, а в другом —2 * x - y
, то проверку я могу сделать всё равно один раз, для первого вычитания. Для второго вычитания я могу статически доказать, что если первая проверка выполняется, то и вторая — тоже.XoJIoD
23.08.2021 18:18Какой именно проверки? Есть пример на каком-то реальном языке? В Scala тоже можно потребовать какой-нибудь имлиситный параметр и создавать его в if'e :)
0xd34df00d
23.08.2021 19:32+3В Scala тоже можно потребовать какой-нибудь имлиситный параметр и создавать его в if'e :)
Тут ключевой момент вот в чём. Его тип может зависеть от соответствующих значений? Ну, чтобы тип имплиситного параметра указывал на то, что это именно свидетельство того, что x меньше y?
Какой именно проверки? Есть пример на каком-то реальном языке?
Вот вам на идрисе, где есть полноценные завтипы:
import Data.String %default total main : IO () main = do x <- cast <$> getLine y <- cast <$> getLine case isLTE y x of Yes y_LTE_x => printLn (x - y) No _ => printLn "not smaller"
Я считываю два числа и проверяю (через
isLTE
), что одно из них меньше или равно, чем другое. Если это так (Yes
), то там рядом вy_LTE_x
будет соответствующее свидетельство. Где оно используется? В случае идриса — неявно одним из аргументов-
:Prelude.Nat.(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
При этом, если вам нужно посчитать
2 * x - y
(или, в альтернативной ветке,y - x
), то больше никаких проверок в рантайме вам делать не нужно. Вы просто пишете несколько лемм (которые проверяются статически и в результирующий код не войдут). Например, что если y ≤ x, то y ≤ 2x:lteTwice : LTE y x -> LTE y (2 * x) lteTwice lte = lteTransitive lte (lteAddRight _)
и что если не y ≤ x, то x ≤ y:
lteContra : (Not (LTE y x)) -> LTE x y lteContra {x = Z} notLTE = LTEZero lteContra {y = Z} {x = (S k)} notLTE = void $ notLTE LTEZero lteContra {y = (S y)} {x = (S x)} notLTE = LTESucc $ lteContra $ \lte => notLTE (LTESucc lte)
после чего используете их:
main : IO () main = do x <- cast <$> getLine y <- cast <$> getLine case isLTE y x of Yes y_LTE_x => do printLn (x - y) let y_LTE_2x = lteTwice y_LTE_x printLn (2 * x - y) No not_y_LTE_x => let x_LTE_y = lteContra not_y_LTE_x in printLn (y - x)
К слову, довольно важный момент ещё вот в чём: проверка в
isLTE
, что y ≤ x, достаточно сильная, чтобы из её неудачи можно было сделать вывод x ≤ y. Для какого-нибудь потенциальногоisLTEMaybe : (x, y : Nat) -> Maybe (LTE x y)
это не так, и функция, всегда возвращающаяNothing
, вполне будет тайпчекаться.XoJIoD
23.08.2021 20:20Тут ключевой момент вот в чём. Его тип может зависеть от соответствующих значений? Ну, чтобы тип имплиситного параметра указывал на то, что это именно свидетельство того, что x меньше y?
Я думаю, элегантного решения ни во 2, ни в 3 Scala действительно нет
XoJIoD
23.08.2021 20:51Из зала подсказали :)
https://scastie.scala-lang.org/jDwimqoSTHqoAk1D6wse2g0xd34df00d
23.08.2021 20:59Что такое
x.type
?Олсо, поменял местами
x
иy
вwhen
, код всё ещё компилируется. Ерунда какая-то.XoJIoD
23.08.2021 21:04Что такое
x.type
?тип переменной х
Олсо, поменял местами
x
иy
вwhen
, код всё ещё компилируется. Ерунда какая-то.разумеется, компилируется, ведь Lte это просто кастомный класс в сниппете. Он скомпилируется даже если назовете его Unicorn. Могу переложить в пакет Prelude, если так будет лучше :)
0xd34df00d
23.08.2021 21:16То есть, этот
LTE
не помнит на уровне типов, на каких значениях он был построен? Ну тогда это совсем не то.В этих наших идрисах
> :doc LTE Data type Prelude.Nat.LTE : (n : Nat) -> (m : Nat) -> Type Proofs that n is less than or equal to m Arguments: n : Nat -- the smaller number m : Nat -- the larger number The function is: public export Constructors: LTEZero : LTE 0 right Zero is the smallest Nat The function is: public export LTESucc : LTE left right -> LTE (S left) (S right) If n <= m, then n + 1 <= m + 1 The function is: public export
XoJIoD
23.08.2021 21:19Помнит, x.type != Int, это тип конкретной переменной x, которая в скоупе:
scala> val x = 15 val x: Int = 15 scala> val y: x.type = x val y: x.type = 15 scala> val y: x.type = 15 ^ error: type mismatch; found : Int(15) required: x.type
0xd34df00d
23.08.2021 21:22Интересно.
Тогда могут в зале там как-нибудь допилить
LTE
до того, чтобы при неправильном порядке сравнения вwhen
оно не компилировалось? А то сейчас, действительно, толку с него нет.
XoJIoD
23.08.2021 21:23Для этого его достаточно положить в [стандартную] библиотеку, в Idris'е же оно не из вакуума появляется
0xd34df00d
23.08.2021 21:28+1Я могу написать
LTE
иisLTE
(аналог вашегоLte
) с нуля сам, и сделать это так, что неправильный порядок сравнения вisLTE
приведёт к ошибке компиляции. Лежит ли оно тут в стандартной библиотеке или ещё где, неважно.
XoJIoD
23.08.2021 21:31А для Int'ов? Я посмотрел реализацию LTE в Idris и, кажется, придумал как сделать то же самое в Scala 3 (через https://dotty.epfl.ch/docs/reference/new-types/match-types.html)
Но тогда мне придется писать еще свою реализацию Nat, а я, право, ленивый
0xd34df00d
23.08.2021 21:35А интами в завтипизированных языках никто не пользуется :]
А своя реализация
Nat
— ну, во всяких идрисах это тоже не очень сложно,data Nat : Type where Z : Nat S : Nat -> Nat
XoJIoD
23.08.2021 22:46https://scastie.scala-lang.org/yqOOLQ3aS2SsQsDlsKsjVQ
переполнение стека исправлять не буду, я обошелся Scala 2 :)
0xd34df00d
23.08.2021 23:01+1О, прикольно. Это очень похоже на то, что в хаскеле (который не завтипизированный, увы) достигается через синглтоны и немного TH-магии.
0xd34df00d
24.08.2021 18:36+1А, ну это чтобы руками не писать отображение рантайм-значений на уровень типов. Например, можно в ридмишке по синглтонам посмотреть, как эта магия используется.
SerafimArts
23.08.2021 20:21Я извиняюсь, что лезу не в свой огород (не пишу на Scala), но разве для подобных ограничений не существует подход с DbC (контрактным программированием)?
Он менее элегантен, однако констреинты не будут проверяться в рантайме, а значит и выше производительность. Плюс подход с пре/пост-кондишенами и инвариантами более явен и ориентирован не на сам тип "Email", а тип в рамках какого-либо скоупа/контекста (например "String" внутри "User").
Но даже не взирая на различия — задачи идентичные: Специализация примитивных типов.
js605451
Я правильно понимаю, что это работает только для валидации, которая не требует какого-то внешнего контекста? Вот например если я хочу Email проверять не только синтаксически, но ещё и на тему отсутствия в блеклисте в БД.
Второй вопрос - в сценарии с десериализацией DTO, состоящего из name/email/age - правильно понимаю, что ошибка десериализации будет содержать только первую ошибку? Т.е. если email и age оба некорректные, то на email оно упадёт, а на age даже не посмотрит?
hakain Автор
Я полагаю нет смысла лезть в БД с синтаксически неверным email. Т.е. для проверки отсутствия почты в блеклисте уже работаем с уточненным типом
Email
В данном случае видно, что декодер возвращает тип
Either
, что по умолчанию подразумевает Fail fast (падаем при первой ошибке). А для Fail slow, к примеру, может использоваться cats.Validated