λ> :t Control.Monad.Fix.fix Control.Monad.Fix.fix :: (a -> a) -> a

@l29ah ‰ lambdabot @src fix fix f = let x = f x in x

@l29ah Спасиб, мил человек, а то я не знал!

@l29ah Хм, как-то странно выглядит. Стоп, тут ведь неявно подразумевается «µa.» в начале, не?

@anon10018 Что такое "µa."?

@l29ah Ну, типа, рекурсивный тип, я не знаю… В общем, мне непонятно, что в той формуле означает «a». Некий произвольный тип, что ли?

@anon10018 Да. В х-ле у тебя везде имплицитный forall для типопеременных.

@l29ah И что же, так все просто?

@anon10018 Не понял вопроса.

@l29ah Я думал, там будет какая-нибудь жуткая формула в три этажа с µ-комбинаторами и лямбдами на тайп-левеле, а оно так просто оказалось. Ладно, попробую теперь доказать, что в «f = \x1 → Y (\y → \x → if x > 0 then y (x – 1) else 0) x1» f имеет тип Int → Int.

@anon10018 лень чототам доказывать λ> :t \x1 -> fix (\y -> \x -> if x > 0 then y (x - 1) else 0) x1 \x1 -> fix (\y -> \x -> if x > 0 then y (x - 1) else 0) x1 :: (Num a, Num a1, Ord a) => a -> a1

@l29ah Э, ну я сам хотел!

@l29ah Чот у меня не получается повторить этот результат. Все время или надо делать «let T = …», или хуй знает, как дальше раскрывать. Я просто свой компилятер делаю, и мне нужно навелосипедить вот эту выводилку из Хачкеля.

@anon10018 Чо за T?

@l29ah f = \x1 → Y (\y → \x → if x > 0 then y (x – 1) else 0) x1 Пусть f применяется к z : Int. Тогда: f (z : Int) = = (\x1 → Y (\y → \x → if x > 0 then y (x – 1) else 0) x1)) (z : Int) = = Y (\y → \x → if x > 0 then y (x – 1) else 0) (z : Int) = = |учтем, что Y g = g (Y g)| = = (\y → \x → if x > 0 then y (x – 1) else 0) (Y (\y → \x → if x > 0 then y (x – 1) else 0)) (z : Int) = = |пусть t : T = (Y (\y → \x → if x > 0 then y (x – 1) else 0))| = = (\y → \x → if x > 0 then y (x – 1) else 0) (t : T) (z : Int) = = if (z:Int) > 0 then (t:T) ((z:Int) - 1) else 0 = = |пусть z1 = z - 1| = = if (… : Bool) then (t:T) (z1:Int) else (0:Int) = = а дальше как?

@anon10018 Собственно, если потом раскрывать t и учитывать, что T = (a → a) → a, то это грёбаное T никуда не уходит. В итоге, если считать, что if возвращает тип-сумму, то у меня получается, что f : Int → T|Int.

@anon10018 Уточняю: если принять, что Y:(a→a)→a, то потом получается, что f:Int→a|Int. a, уходи.

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