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

Я расскажу немного об истории вопроса, а затем покажу, как зависимые типы могут спасти мир.

Что такое зависимый тип?

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

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

Рассмотрим беззнаковый целочисленный тип: UInt¹

UInt(exactly: 1)   // 1
UInt(exactly: 1.0) // 1
UInt(exactly: -1) // nil

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

Когда вы используете UInt, вы передаете информацию о том, что имеете дело с положительным целым числом. Это полезно.

Время спасать мир!

Представим, что мы пишем программное обеспечение для атомной электростанции².

Если реактор перегреется, это может вызвать климатическое событие и привести к концу жизни на Земле. Нам нужна функция для его охлаждения:

func addCoolantToNuclearPowerPlant(gallons: Int)

Потенциально вы могли бы назвать это с отрицательным числом:

func doEmergencyStuff() {
    addCoolantToNuclearPowerPlant(gallons: -1000000)
}

Вы только что слили всю воду и спровоцировали ядерную катастрофу. Легко понять, почему тип UInt был бы более безопасным выбором для этого параметра.

func addCoolantToNuclearPowerPlant(gallons: UInt)

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

Из проверки вы заметите, что существует неявная зависимость от значения параметра.

Мы можем и должны сделать неявное явным, определив новый зависимый тип. Назовем это Coolant.

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

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

Краткое резюме:

  1. Мы поняли, что функция охлаждения принимает значение, к которому предъявляется неявное требование. Мы могли сказать, что это было требование, потому что функция проверяла значение перед его использованием.

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

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

Хорошо, вернемся к спасению мира.

Проблемы с инвентаризацией:

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

Было бы легко сделать что-то вроде:

if !inventory.coolantSupply.isEmpty { ... }

Это могло привести к ядерному расплаву. Наличие Coolant не означает, что у вас действительно есть Coolant.

Нам нужно изменить наше определение Coolant, чтобы оно не было отказоустойчивым. Давайте сделаем это, определив другой зависимый тип, AtLeastTenThousand, чтобы представить число не менее 10 000.

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

Краткое резюме:

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

  1. Выявлено, что инициализатор для нашего зависимого типа Coolant принимает значение, для которого имеется неявное требование. Мы могли сказать, что это было требование, потому что инициализатор проверял значение перед его использованием.

2. Мы переместили это неявное требование в новый зависимый тип AtLeastTenThousand, который может быть создан только со значением, которое явно удовлетворяет требованию.

3. Мы использовали этот новый тип в инициализаторе, тем самым переместив логику из инициализатора Coolant в тип параметра, который инициализатор принимает.

Это Overkill?

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

Эта аварийная функция по-прежнему должна будет следить за тем, чтобы вход Coolant был действителен.

В этом случае легко упустить из виду преимущество наличия зависимого типа для Coolant. В небольшом примере вы, вероятно, правы, вероятно, это излишне. С таким же успехом мы могли бы написать:

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

Добавление требования к зависимому типу:

Это неплохо, но мы упустили одну вещь. Наша функция вводит в заблуждение. Он говорит, что принимает галлоны, но ничто в Coolant не обеспечивает этого подразумеваемого требования. Давайте перепишем Coolant, чтобы обеспечить соблюдение этого требования, используя тип Foundation Measurement.

Это лучше, поскольку теперь наш код будет правильно обрабатывать преобразование единиц измерения. Однако мы «сломали» Coolant, сделав его отказоустойчивым. Еще раз мы можем очистить это, используя зависимый тип. Назовем это Gallon.

Теперь мы можем провести рефакторинг Coolant, чтобы снова работать без сбоев:

Краткое резюме:

При использовании Coolant возникла потенциальная проблема из-за отсутствия ясности в отношении единиц измерения. Мы решили эту проблему, выполнив следующие шаги, чтобы гарантировать, что Coolant может быть создан только с правильным типом измерения.

  1. Выявлено, что инициализатор для нашего зависимого типа Coolant принимает значение UnitVolume, которое имеет неявное требование. Мы могли сказать, что это было требование, потому что инициализатор проверял значение перед его использованием.

2. Мы переместили это неявное требование в новый зависимый тип Gallon, который может быть создан только со значением, которое явно удовлетворяет требованию.

3. Мы использовали этот новый тип в инициализаторе, тем самым переместив логику из инициализатора Coolant в тип параметра, который инициализатор принимает.

Последняя вещь:

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

Coolant теперь должен выглядеть так:

Это небольшое изменение, но выполнять преобразование в Double в момент использования некрасиво. Почему бы не переместить еще одну часть информации в наш Зависимый Тип?

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

Тестирование зависимых типов:

Я не упоминал о тестировании до сих пор, потому что существует множество статей о тестировании базовых классов и структур, и это в основном все.

Надо сказать, что это одна из радостей этих типов. Если у вас есть тщательно протестированная реализация AtLeastTenThousand и Gallons, вам не нужно тестировать Coolant, потому что во всем этом нет логики.

Заключение:

Я думаю, что эта цитата суммирует для меня привлекательность зависимых типов.

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

- Торстен Альтенкирх, Конор Макбрайд и Джеймс МакКинна: ​​Почему зависимые типы имеют значение. Апрель 2005 г.

Это вкратце. Он перемещает Type Safety на самый низкий уровень, который вы можете.

Возможно, вы заметили, что на протяжении всего этого процесса мы следовали довольно четкой схеме.

  1. Обратите внимание на то, что значение имеет требование (больше, меньше, есть, содержит и т. Д.) В зависимости от того, как оно используется
  2. Переместите это требование на уровень ниже в новый тип, который может быть создан только в том случае, если значение соответствует требованию.
  3. Используйте этот новый зависимый тип вместо старого значения
  4. Повторяйте, пока все не станет настолько маленьким и надежным, насколько это возможно.

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

Или вы можете просто полить его водой.

Спасибо за прочтение!!!

[1] Я понимаю, что UInt - это скорее удобная оболочка, которую Swift предоставляет для доступа к UInt8 или UInt16 и др., Так что вам не нужно уделять столько внимания управлению памятью. Назвать его зависимым типом будет с натяжкой, но это помогает мне проиллюстрировать пример.

[2] Я не инженер-ядерщик. Если это прочитает тот, кто много знает об атомных электростанциях; Мне очень жаль.