Сейчас будет очень плохо сформулированные вопросы :с 1) Существует ли возможность в идрисе создать биекцию между значениями и типами т.е. 42 :: Num 42, например? 2) Существует ли возможность автоматизировать это создание? 3) Существует ли возможность при этом всём сохранить человечность кода?

А чего не в чатик по идрису?

Синглтоны хочешь?

Конечно. Правда завсегдатаи с этим чатом сильно пересекаются: https://t.me/joinchat/AAAAAD9SWO_tLd7rJ9S7Ig

идрис же выводит тип по реализации, минимум чтобы проверить

но например sort : List a -> List a reverse : List a -> List a, а мне хотелось бы узнать возможность биекции реализация <-> тип

то тогда любая функция которая имеет такой тип будет сортировкой

автоматически её вывести из такого плохого описания нельзя

Написать дсл, который будет дублировать стейтменты идриса)

Ну так ты же хотел биекцию. Может ошибаюсь, но если две вещи эквивалентны, то уже биекция невозможна

но это же то, что система типов принципиально и дает

Было бы все так легко, все бы писали верифицированный код)

"Монады являются моноидами, ведь как известно, монада — это всего лишь моноид в категории эндофункторов, а монадические законы — не более чем определение моноида в контексте продолжений" Всего лишь. Как известно. С очевидностью следует. Пиздить вас кочергой.

Слова "тактики и стратегии" в идрисе точно есть, видел в доке

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

ага, особенно политологу это полезно (кем ортега типа является)

ага, особенно политологу это полезно (кем ортега типа является)

а зачем политологу знать активно теоркат, кроме как для собственного развития?

ну если тебе не интересно то зачем ты изучаешь?