Доброго времени суток, уважаемый хабраюзер!

Прочитав несколько книг по типизированному лямбда исчислению, а именно по зависимым типам, увидел интересную закономерность: везде первым примером приводится определение типа «отсортированный список». Все бы хорошо, но дальше этого определения ничего не было. Вот я и придумал восполнить этот пробел и реализовать функцию, принимающую список, и возвращающую другой список и два доказательства. Одно доказывает, что результат — это перестановка входа, а другое доказывает, что результат — отсортированный список.

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

Доброго времени суток, уважаемое Хабрасообщество.
Недавно приходилось наблюдать дискуссию о каррировании и частичном применении. Суть этой полемики состояла в том, что лучше, для практических целей, иметь в языке программирования: встроенное частичное применение (например, как в Nemerle) или встроенное каррирование (как, например, в Haskell).