Когда у меня есть тип «enum», то есть алгебраический тип данных, в котором ни один из случаев не заключает в себе какие-либо другие данные, я обычно предпочитаю проецировать парсер / принтер вне отображения на строку, чтобы убедиться, что парсери принтер остается в синхронизации, когда я меняю код.Например, в Idris:
data RPS = Rock | Paper | Scissors
Eq RPS where
Rock == Rock = True
Paper == Paper = True
Scissors == Scissors = True
_ == _ = False
StrMap : List (RPS, String)
StrMap =
[ (Rock, "rock")
, (Paper, "paper")
, (Scissors, "scissors")
]
я мог бы реализовать функцию печати следующим образом:
print' : RPS -> Maybe String
print' rps = lookup rps StrMap
Проблема в том, что я не хочу Maybe здесь.Я хотел бы гарантировать во время компиляции, что я охватил все мои дела, так же, как я мог бы, если бы написал эту функцию путем разделения дел на RPS, где включился бы инструмент проверки исчерпаемости, и я мог бы просто получить print : RPS -> string.В Идрисе я знаю, как восстановить это с помощью доказательства (разве вы просто не любите Идриса!):
print_exhaustive : (rps : RPS) -> IsJust (print' rps)
print_exhaustive Rock = ItIsJust
print_exhaustive Paper = ItIsJust
print_exhaustive Scissors = ItIsJust
justGetIt : (m : Maybe a) -> IsJust m -> a
justGetIt (Just y) ItIsJust = y
print : RPS -> String
print rps with (isItJust (print' rps))
| Yes itIs = justGetIt (print' rps) itIs
| No itsNot = absurd $ itsNot $ print_exhaustive rps
Теперь, на мой взгляд, это фантастика.Я могу объявить ровно в одном месте моего кода, какова корреляция между регистром перечисления и связанной с ним строкой, и у меня может быть функция print и функция parse, написанные с ней (функция parseздесь опущено как не относящееся к вопросу, но тривиально для реализации).И не только это, но я смог убедить проверяющего, что моя подпись print : RPS -> String, которую я хотел, не поддельная, и я избежал использования каких-либо частичных функций!Вот как мне нравится работать.
Однако на работе большая часть моего кода находится на F #, а не в Idris, поэтому вместо этого я использую FsCheck для квази-доказательной исчерпанности с помощью теста на основе свойств.,Это не так уж плохо, но
- Тест на основе свойств не совмещен с
StrMap;это в другой сборке.Мне нравится сопоставлять мои инварианты с тем, на что они ссылаются, насколько это возможно. - Вы можете продвинуться дальше в процессе сборки, прежде чем столкнетесь с ошибкой, если вы, например, добавили случай и забыли изменить
StrMap;если бы вы просто сидели там и перекомпилировали, как я часто это делаю, вы бы пропустили его, пока не выполнили тесты. - Я должен использовать неисчерпывающие функции для его реализации из-за более слабой системы типов.Это портит ясность того, чему я пытаюсь научить своих коллег;Я пытался убедить их во славе тотального функционального программирования.
Мы только что начали новый проект на Хаскеле, и я натолкнулся на такой сценарий.Конечно, я могу использовать QuickCheck и fromJust и реализовать стратегию F #, и это должно быть хорошо.
Но мне интересно то, что сообщество и экосистема Haskell подчеркивают соответствие Curry-Howard таким образом,что сообщество и экосистема F # этого не делают, и, поскольку в последние дни были добавлены всевозможные необычные расширения, позволяющие использовать зависимые типы, не могу ли я вместо этого следовать своей стратегии Idris для этого?Кто-то сказал мне, что я должен быть в состоянии перевести все, что я могу написать в Idris, на Haskell, не теряя при этом безопасность типов, если я включил достаточно расширений (и был готов ввести достаточно многословия и т. Д.).Я не знаю, правда это или нет, но если это правда, я хотел бы знать, какие расширения включить и какой код писать, чтобы следовать моей стратегии Idris для этого в Haskell.Также стоит отметить: я мог бы поверить, что моя стратегия Idris - не самый простой / элегантный способ сделать это на этом языке.
Как я могу перевести этот код Idris в Haskell, чтобы реализовать print :: RPS -> String безвызывая какие-либо частичные функции?