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

Естественно, что ограничения подобного рода хочется выразить не только в документации к проекту и именах переменных, но и в системе типов, чтобы обеспечить их проверку компилятором. Некоторые языки (Agda, Idris, Whiley) позволяют создание зависимых типов из коробки, а такие языки как Haskell и Scala обеспечивают их поддержку на уровне библиотек.

Самой популярной библиотекой подобного плана в Scala является Refined, вдохновленная одноименным аналогом из Haskell. Суммарно в библиотеке поддерживается несколько десятков операций над типами. Вот так, к примеру, с её помощью будет записан тип строки, представляющей из себя непустой набор цифр: MatchesRegex[W.`"[0-9]+"`.T]. Несмотря на (порой значительное) увеличение времени компиляции, библиотека однозначно рекомендуется к ознакомлению.

Scala bin

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

Естественно, что ограничения подобного рода хочется выразить не только в документации к проекту и именах переменных, но и в системе типов, чтобы обеспечить их проверку компилятором. Некоторые языки (Agda, Idris, Whiley) позволяют создание зависимых типов из коробки, а такие языки как Haskell и Scala обеспечивают их поддержку на уровне библиотек.

Самой популярной библиотекой подобного плана в Scala является Refined, вдохновленная одноименным аналогом из Haskell. Суммарно в библиотеке поддерживается несколько десятков операций над типами. Вот так, к примеру, с её помощью будет записан тип строки, представляющей из себя непустой набор цифр: MatchesRegex[W.`"[0-9]+"`.T]. Несмотря на (порой значительное) увеличение времени компиляции, библиотека однозначно рекомендуется к ознакомлению.

GitHub

GitHub - agda/agda: Agda is a dependently typed programming language / interactive theorem prover.

Agda is a dependently typed programming language / interactive theorem prover. - agda/agda

hottg.com/scalabin/41

180 viewsedited  Mar 12, 2019 at 20:34