это самый простой NT что не создает никаких эффектов

ну это уже программистское

а T2 -> T вроде категорное

Не, именно в статье по тк я это и видел)

Там было f, не m, не суть

Типа F²(a) -> F(a)

Ну в общем использование верхнего индекса мне понравилось

но самое интересное это функтор с функторной алгеброй

а вот эти 2 1 -> T, T2 -> T` дают возможность функтору стать монадой

Но постой, я не понимаю, при чем тут функтор вообще

где для A есть такой морфизм a :: F(A) -> A

у нас есть простой вид A -> B

и есть F A -> F B

или же h :: A -> B F h :: F A -> F B

где для A есть такой морфизм a :: F(A) -> A

Это какая-то комонада

Да, я знаю, что такое функтор)

и есть a :: F A -> A, b :: F B -> B

Я не у тому. Наличие тех двух морфизмов делают любую категорию монадой, независимо от того, функтор это или нет

теперь можно вывести по коммутативной диаграмме такое h . a = b . F h

f :: F A -> A

это алгебра

f :: A -> F A

это коалгебра

наверное ты знаешь что такое fix

Для поиска неподвижной точки?

ну да это мат понятие где x = f x

как бы на одной точке крутимся

что дает нам писать неявную рекурсию

ну так вот

такая же фигня и для типов возможна

fix f = f(fix f)

Ну я недавно читал про фри-монаду, там было что-то пободное

это стандарт

да

Free монада похожа на Fix просто у Free есть еще доп инфа в виде Pure

но не суть)

продолжим?

Да, давай, я все равно нихуя не понимаю)

наверное ты знаешь что любую структуры можно представить алгебраически

Предполагал, да)

думаю ща ты угадаешь что это

l = 1 + a + a^2 + a^3...

это индуктивный тип

Ну на всякий случай скажу, что я не угадал

Индуктивный в каком плане?

И в смысле тип?

спискок это

индуктивный это рекурсивный

Типа рекурсивный тип?

Да

Вот

есть еще корекурсивный но не об этом ща

думаю знаешь что такое мат индукция?

Да

доказывал что-то через мат индукцию

Да, но мелочь

Доказать для 1, доказать для n+1

ну так вернемся) l = 1 + a + a^2 + a^3 + ... l = 1 + a * (1 + a + a^2 + ...)

дальше надо унифицировать)

это ряд Тейлора)

запиши математически его

Давай лучше ты, потому что я слышу такой термин впервые)

l = 1 + a * l

l = 1 + a * l

теперь видишь почему это индуктивный тип?

Почти

тут что-то скрыто)

ERROR: S client not available

А, не пояти

Я смог

Азахаха

вспомни что я писал про x = f x

давай запишем так l = (\x -> 1 + a * x) l

Стой, прежде чем это делать

Я не очент понимаю связь рекурсии и неподвижной точки

А, вот теперь понял

ну это почитай про комбинатор неподвижной точки Y придуманый Карри

его бетта редукция будет приводить к нему же

f x = 1 + a * x

продолжим?)

не

l = f l

о!

а у нас есть для этого вещица одна

l a = fix(\x -> 1 + a * x)

как можно заметить то \x -> 1 + a * x

давай теперь попробуем записать через тип это

data List a b = Nil | Cons a b

это простой тип суммы/произведения

не индуктивный

теперь fix

для функции мы знаем как это сделать

И b - List a b

чтобы было понятней l a b = fix(\x -> 1 + a * x) b просто тут эта преобразование

Ага

fix f = f (fix f) newtype Fix f = Fix { unFix :: f(Fix f) }

похоже?)

Ну

так

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