Или как параметрические типы бесплатно влекут за собой теоремы

Вот конкретное решение для 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 здесь, для реализации наших конкретных функций. Учитывая их очень общий характер, с ними намного проще писать «очевидно правильные» программы.

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

Ссылки и дополнительная литература: