Rust Types - Taxonomy

От Nikita Bishonen • 4 минут чтения •



Привет! Сегодня я делюсь своими мыслями о таксономии типов в Раст. Это первая версия таксономии и поста, буду благодарен за любые идеи по её улучшению.

Таксономия

Таксоно́мия (от др.-греч. τάξις — строй, порядок и νόμος — закон) — учение о принципах и практике классификации и систематизации сложноорганизованных иерархически соотносящихся сущностей.

Я захотел украсить свой кабинет графической иллюстрацией “таксономии” системы типов данных, схожей с той, что использует Раст. К сожалению мои поиски не принесли желаемый результат и я решил сделать свою иллюстрацию и делюсь ею с вами в этой публикации.

Типы

Теории

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

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

HoTT

Теории типов и Раст

Собственно основным вопросом, ответ на который я искал - теория типов стоящая за Раст и её проекция на типы, которые мы используем при написании кода на Раст. Не я один задавался таким вопросом: https://users.rust-lang.org/t/practical-intro-to-type-theory/18204/5 Также есть небольшой доклад на эту тему: https://av.tib.eu/media/52178 “Ментальная модель”: https://ia0.github.io/unsafe-mental-model/type-theory.html А также интересный пост: https://www.kurtlawrence.info/blog/category-theory-with-rust-pt1 Но все они имеют много букв и не имеют “всеобъемлющего” графика, чтобы я повесил его на стену.

Таксономия Раст Типов

Taxonomy

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

П-тип

Тип произведение ни дать, ни взять. Мы компануем несколько типов в один, получаем произведение возможных значений этих типов как новое множество значений. Какие типы в Раст его реализуют?

Σ-тип

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

Типы-указатели

Раст имеет возможности для работы с памятью, поэтому язык содержит в себе и ссылки и указатели. Нас же интересуют только “высокоуровневые” концепции.

Другие типы