Ну да. Можно реализовать частный случай. Но написать обобщенную функцию для произвольной монады, как в hakell, уже не получится. Например, не получится написать функцию типа

filterM :: Monad m => (a -> m Bool) -> [a] -> m [a]

Мне кажется, проблема в системе типов. Система типов обычных языков, типа C#, просто не позволяет делать такие выкрутасы, которые позволяет система типов Haskell.
Допустим, есть класс типов Monoid

class Monoid a where
   mempty :: a
   mappend :: a -> a -> a

Я могу «эмулировать» его в C# с помощью интерфейса

interface Monoid<A>
{
	A mempty();
	A mappend(A a1, A a2);
}

Затем я могу сделать instanse моноида для конкретного типа с помощью наследования

class IntMonoidInstance: Monoid<int>
{
	int mempty(){ .. }
	int mappend(int a1, int a2) { .. }
}

Но этот фокус не сработает для монады.
Класс типов монады объявлен как

class Monad m where
   return :: a -> m a
   (>>=) :: forall a b . m a -> (a -> m b) -> m b

Здесь m является не просто типом, как в случае с моноидом. Она является типом, параметризированным другим типом. Другими словами: * -> *.
Интерфейс для монады в C# должен выглядеть примерно так

interface Monad<M> where M: * -> *
{
	M<A> return<A>();
	M<B> bind<A, B>(M<A> a1, Func<A, M<B>> a2);
}

Но C# со своей мощной системой типов не позволяет делать такие штуки. Я не могу объявить интерфейс, параметризированный типом, который параметризирован другим типом.
Любые реализации монады в C# все равно останутся недо-монадой.

Я с вами категорически не согласен. Я утверждаю, что новичок нуждается в «магии». Если перегружать новичка деталями, то это его еще больше запутает. Я сознательно упустил математическую строгость в пользу понятности.
Поэтому моя статья написана именно в таких терминах и именно на новичков она и рассчитана.

Я думал об этом. Coq я люблю. Только эта тема не очень востребована.

По-моему, верификация hardware — это вообще не про математику и не про доказательства.
Мне интересны именно «софтварные вакансии».

Я смотрел в сторону VHDL, Verilog. Но у меня сложилось впечатление, что это к «формальной верификации» вообще не имеет никакого отношения. Это больше похоже на написание тестов для микросхем. А мне бы хотелось что-нибудь связанное именно с математическим доказательством корректности программ. Зависимые типы, все такое.

Покажите мне вакансию, связанную с формальной верификациейс, и я вам заплачу! Серьезно.
Формальная верификация — это очень круто и интересно. Мне бы очень хотелось работать в данной области. Но факт в том, что это никому не нужно. И вряд ли это станет мейнстримом в ближайшем будущем. Грусный смайлик.

В принципе, да, все честно.

Есть такая программа для инди/студентов.
https://www.gamesparks.com/indie-student-programme-faq/
Вы не платите ничего, пока MAU(Monthly Active User) не превышает 100 000.

Но у них свои критерии инди, и каждый запрос они рассматривают отдельно. По их мнению, наша студия JetDogs не является инди (что, в общем-то, не далеко от истины).

Я правильно понял, что чувак пишет правой рукой в правую сторону? А вы потом отзеркалили видео, чтобы надпись выглядела нормально для зрителя. Получается, что у чувака со второй картинки специально отзеркаленная футболка?

Музыкальная нотация — худшая из всех систем обозначения или жаргонов, с которыми я когда-либо сталкивалась.

Полностью согласен с автором. В музыкальной нотации есть масса вещей, которые вызывают у меня WTF-реакцию. Такое ощущение, что её придумывал какой-то наркоман.

Не знаю, возможно, меня закидают тапками, но вообще-то в России, как и вообще в континентальной Европе (кроме Нидерландов) принято использовать для обозначения ноты Си букву H, а буква B обозначает си бемоль.

Это, как раз, ярчайший пример нелогичности музыкальной нотации. Казалось бы, что может быть проще, буковками «A», «B», «C» будем обозначать ноты ЛЯ, СИ, ДО, соответственно. Бемолем будем обозначать ноту на пол-тона выше, «Ab», «Bb». Какому гению пришло в голову сделать замену?
B <-> Bb
H <-> B
Вот зачем это нужно было делать? Чтобы всех запутать?
Я вот часто ищу в интернете аккорды разных песен. Когда встречается аккорд «B», никогда не знаешь — это СИ или СИ-бемоль.

Я занимаюсь программированием достаточно долго, пробовал разные языки программирования, разные системы типов, парадигмы. Попутно еще пытаюсь изучать математику: абстрактную алгебру, топологию, теорию категорий и т.п.
Моё субъективное ощущение в том, что математика ГОРАЗДО сложнее любого языка программирования.

Когда-то давно написал 4-мерного пакмана. Игровое пространство представляло из себя несколько 3-мерных лабиринтов, которые существовали как бы в параллельных измерениях. Между такими лабиринтами существовали «коридоры». На самом деле пространство было абсолютно изотропным и не было никаких выделенных направлений, но объяснить людям, что это и есть 4-мерное пространство было очень сложно. Самой частой фразой, которую я слышал, было «4-ое измерение — это же время!?»

Правильно ли я понимаю, что в логике первого порядка есть фиксированное число предикатов и я могу их произвольно комбинировать с помощью кванторов и логических операций. Но в логике первого порядка нельзя сформулировать утверждение «для любого предиката P(x) верно ...»

А можно вопрос в тему? Под логикой предикатов подразумевается логика первого порядка? Я не совсем понимаю, что это такое. Где граница между логикой первого парядка и логикой высшего порядка?

Спасибо тебе, добрый человек :). А почему все-таки его нет в стандартной библиотеке?

А ещё не хватает объяснения вот таких простых вещей, как выход из вложенного цикла, например.

По поводу приведенной выше статьи, кто-нибудь может мне объяснить, где лежит монада EitherT? Я уже весь интернет излазил — где-то пишут, что он лежит в Control.Monad.Either, кто-то пишет, что в Control.Monad.Trans.Either. В моей версии хаскеля (Haskell Platform 2013.2.0.0) его нет нигде. Его выкинули из стандартной библиотеки? Если да, то зачем? Что мне делать, если я хочу EitherT вместо дибильного ErrorT?

Зачем программировать вообще? Есть же давным давно написанный ИИ, который может сам программы писать. Главное, никому не показывать. Межпрограммерский заговор ведь :)

Про Гомера Симпсона и JPG тоже не очень верное сравнение.
В случае с Гомером имеем функцию
t -> (x, y)
к которой применяем ПФ.

А в случае JPG имеется функция (от двух переменных !!!)
(x, y) -> color
к которой применяется ФП, при чем дважды, по обеим переменным

Да ничто не мешает. Теоретически могло быть и то, и то.