Вообще, изначально задача была в том, чтобы сделать тривиальным map, который каждый прекрасно понимает и без какого-либо погружения в тк. Но потом я вспомнил, мол, мап можно выразить через байнд и пьюр, а байнд мне тоже может пригодится. Так почему бы не сделать так?

Не знаю уместно это или нет, но я на всякий случай тебе проясню: дело далеко не в том, чтобы у тебя был bind и return и даже того факта, что они удовлятворяют особой магической сигнатуре тоже недостаточно. У них еще должна быть "правильная" семантика, которую математики в лучших своих традициях определяют как набор инвариантов - логических утверждений, которые истины в любом "состоянии" системы. Проверить выполнение этих требований погромистом чаще, реже программистом компилятор не может, поскольку это NP-сложная задача. Как следствие, мало найти что-то, что выражается как return и bind, надо еще чтобы они в этом конкретном случае удовлетворяли этим непреложным законам.

все видели? меня дедушка лайкнул

причем с чисто практической точки зрения в эфшарпе нет возможности дать статическую гарантию в общем виде, то есть система типов вообще никак не помогает с проверкой этих законов.

причем с чисто практической точки зрения в эфшарпе нет возможности дать статическую гарантию в общем виде, то есть система типов вообще никак не помогает с проверкой этих законов.

Обычно для такого используют quickcheck или доказывают руками, но понятно, что это полумеры.

Вообще, изначально задача была в том, чтобы сделать тривиальным map, который каждый прекрасно понимает и без какого-либо погружения в тк. Но потом я вспомнил, мол, мап можно выразить через байнд и пьюр, а байнд мне тоже может пригодится. Так почему бы не сделать так?

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

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

В F# такого особо нет.

Вообще видать - тебе в зависимые типы. Там можно доказать с тем, что компилятор проверит исполнение данных законов

ох ничосе. не знал ничего такого. и как компилятор это сделает? переберет 2^32 значений на каждую конфигурацию int'а? очевидно, нет. докажет по индукции? окей, но тогда отвественность опять будет лежать по погромисте.

Он проверит доказательство, точно так же как он тайпчекает программу

Надо почитать про это все. Для меня пока темный лес.

Idris

+ или Agda