а что с ней не так? Бисимуляция для равенства?

сам факт обмена инпутом-аутпутом через ченнелы и general concurrency?

Ну да. Вот эти вот каналы — это некрасиво и излишне.
Нормальной категории не подобрать, всё громоздко получается.
Ну вот для всяких там типизированных лябмд, у нас есть всевозможные CCС.
А для пи-исчисления что у нас есть? ;-)
Ну и если его типизировать, то тем более нифига проще не получается, чем там же линейщина.
А ещё, пи-исчисление записывается внутри линейщины.
И зачем тогда?...

Подскажите хороший задачник для начинающих по теме

в Lawvere, Schanuel, "Conceptual Mathematics" по моему были задачки

Спасибо, нашёл, выглядит интересно

Ребята поясните пожалуйста за f-алгебры и катаморфизмы

foldl`/`foldr - это катаморфизм для [] - как это понять?
что здесь f?
что здесь Fix f? наверное []
что здесь алгебра? f a -> a

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

cata :: Functor f => (f a -> a) -> Fix f -> a
cata f = go where
  go = f . fmap go . unFix

data ListF b = NilF | ConsF a b
  deriving (Functor)

type List a = Fix (ListF a)

lengthAlg :: ListF a Int -> Int
lengthAlg NilF = 0
lengthAlg (ConsF _ l) = l + 1

length :: List a -> Int
length = cata lengthAlg

чет типа такого полагаю

т.е. грубо говоря, как найти функтор для рекурсивного АДТ:

абстрагироваться по всем рекурсивным типам АДТ
применить комбинатор неподвижной точки на этом АДТ
для списка:

data List a = Nil | Cons a (List a) превращается в
data List t r = Nil | Cons t r

для дерева:

data Tree a = Leaf a | Node (Tree a) (Tree a) -- превращается в
data Tree a t = Leaf a | Node t t

список:

data L t r = Nil | Cons t r
type List t = Fix (L t)

абстрагируемся по t (говорим, что t это рекурсивный тип данных – такой же список)

дерево:

data T a t = Leaf a | Node t t
type Tree a = Fix (T a)

опять тоже самое – абстрагируемся по t (говорим, что t это рекурсивный тип данных, т.е. тоже самое дерево)

это видел, да

а что по списку из стандартной библиотеки [] ?

это fixed point какого-то функтора?

ну вот же для списка я скинул

data ListF b = NilF | ConsF a b
  deriving (Functor)

type List a = Fix (ListF a)

nil :: List a
nil = Fix NilF

cons :: a -> List a -> List a
cons a b = Fix (ConsF a b)

чтобы работать с [] через все это, его нужно в ListF преобразовать

по сути массив это data [] a = [] | a : [a]

это уже fixed point

можно ли найти его unFix?

каждый раз находишь, когда паттерн-матчишь списки