Самое время уже кровососов заводить пока лысеть не начал и стояк не пропал

Нет, спасибо. :D

В "Type-Driven Development in Idris" увидел такой интересный шаблон проектирования, заключающийся в программировании не в самом Idris (а-ля в хост-языке), а в множестве eDSL. Таким образом, недопустимые операции (например, удаление файла при работе с REPL) нельзя выполнить + повышается самодокументируемость, в общем, все преимущества мощной типизации.

Описывается это примерно так: определяем тип, возможно бесконечный (см. "codata") с операцией >>= (а ещё лучше - сразу реализовать для него монаду) и исполнителя этого типа. Аппликация операторов >>= (возможно, при помощи do-нотации) - есть eDSL, а исполнитель - есть исполнитель, интерпретатор, этого eDSL:

module Main

%default total

data ReplCommand : Type -> Type where
    PrintMessage : String -> ReplCommand ()
    ReadMessage : ReplCommand String
    (>>=) : ReplCommand a -> (a -> ReplCommand b) -> ReplCommand b

run : (command : ReplCommand resultType) -> IO resultType
run (PrintMessage x) = putStrLn x
run ReadMessage = getLine
run (x >>= f) =
    do
        firstResult <- run x
        secondResult <- run (f firstResult)
        pure secondResult

myRepl : ReplCommand ()
myRepl =
    do
        userInput <- ReadMessage
        PrintMessage userInput

main : IO ()
main = run myRepl

Всё, что может делать _любая_ реализация REPL, описано в ReplCommand. Она не может совершить вредоносных действий, например, удаление БД, выход из программы, и так далее. Единственное, на чём нужно сконцентрировать внимание - это функция run. Но она лишь одна, зато все реализации считаются "правильными" в нашей понятийной системе.

Можно уточнить требования, например, заставить реализации REPL отвечать на каждое считанное сообщение. Я опустил этот момент в угоду простоты изложения.

@MRSMITH4 вот такое говно более-менее сойдет?

точнее

Public много не бывает

первый для типов, второй для мемберов, третий для методов

а че

Как-то одна вода.

> Функции с одинаковым типом входного и выходного значения являются моноидами и имеют специальное название — «эндоморфизмы»

Как-то очень нестрого

Мне понадобилось понять, что не функции A -> A являются моноидами, а множество функций A -> A (Hom(A, A)) в заданной категории образуют моноид с единичным элементом - id, а бинарным оператором - композицией морфизмов

Какое-то дерьмо попсовое

Ничего не понятно. Что за Hom?

Множество всех морфизмов с доменом A и со-доменом A

Где A - объект в категории

В комментариях какая-то дичь творится, непонятно, это они так шутят, или нет