Или как параметрические типы бесплатно влекут за собой теоремы
Вот конкретное решение для FizzBuzz.
Хорошо! Но что, если мы захотим отразить некоторые наши ожидания от этой программы в наших типах? Одним из примеров является то, что когда вы получаете Val
обратно от fizzbuzz
, он содержит значение, которое вы ему передали.
Прямо сейчас мы всегда можем вернуть Val 42
в этом случае, и он все равно будет проверять тип, это плохо!
Ответ заключается в решении более общей проблемы. Давайте введем параметр типа в нашем FizzResult
случае и вынесем за скобки общую структуру fizzbuzz
функции.
В этой версии мы видим, что единственное разумное значение, которое мы можем вернуть в случае Val
, - это то же значение, которое мы получили в качестве входных данных, у нас нет других способов получить a
!
Благодаря этому мы можем увидеть, как использование переменных типа, решая более общую проблему, ограничивает то, что мы можем делать, и приводит нас к правильности.
Можем ли мы на самом деле сделать лучше и сделать так, чтобы наша mkFizzBuzz
функция возвращала FizzBuzz
только тогда, когда выполняются оба предиката, Fizz
, когда выполняется только первый предикат, Buzz
, когда выполняется только второй, и, наконец, Val x
только когда оба предиката не выполняются ?
Ответ: Да!
И мы можем использовать стратегию, очень похожую на описанную выше.
Идея заключается в следующем: для каждого из предикатов добавьте два параметра типа. Они будут соответствовать случаю, когда предикат истинен, а когда - ложен. Называя первый предикат p
, а второй r
, мы получаем следующий тип:
И соответственно модифицируем наш mkFizzBuzz
:
Если вы посмотрите на код достаточно долго (или, что еще лучше, попытаетесь придумать свой собственный), вы увидите, что это единственная возможная функция для сигнатуры этого типа.
Причина в том, что вам нужно:
pt
иrt
для производстваFizzBuzz pt rt
pt
иrf
для производстваFizz pt rf
- И так далее
И получить их можно только по результатам предикатов ¹. В некотором смысле эти новые предикаты несут «свидетелей» их истинности / ложности, а именно значения типа pt
и pf
соответственно.
Теперь мы можем, наконец, реализовать желаемую версию fizzbuzz :: Int -> FizzBuzz
с точки зрения правильного типа mkFizzBuzz
:
Надеюсь, это иллюстрирует ценность использования общих комбинаторов более высокого порядка, таких как mkFizzBuzz
здесь, для реализации наших конкретных функций. Учитывая их очень общий характер, с ними намного проще писать «очевидно правильные» программы.
Примеры этих типов комбинаторов, которые используются в повседневной жизни, включают карты, складки, фильтры и многие другие.
Ссылки и дополнительная литература:
- [1] Я использую слово предикат здесь несколько либерально в том смысле, что это функции формы
a -> Either b c
, а не более знакомойa -> Bool
. - Ваддлер П., теоремы бесплатно!
- Милевски Б. Параметричность: деньги напрасно и теоремы бесплатно
- Готовый исходный код для финальной версии