K
Size: a a a
2020 July 02
AT
А помимо этого
Так это, стат анализ же держится на этом. Индуктивные типы. Наименьшая неподвижная точка рулит
w
Так это, стат анализ же держится на этом. Индуктивные типы. Наименьшая неподвижная точка рулит
R
Так это, стат анализ же держится на этом. Индуктивные типы. Наименьшая неподвижная точка рулит
AG
индукция это тип рекурсия на завтипах
AG
Так это, стат анализ же держится на этом. Индуктивные типы. Наименьшая неподвижная точка рулит
а как же наибольшая?
AG
в понедельник кстати на LFMTP был доклад примерно на ту же тему, про которую я лампропулоса спрашивал :)
AG
PBT для коиндуктивных данных
λ
Никто не замечал насколько сильно течёт зио?
λ
Никто не замечал насколько сильно течёт зио?
Ты уверен что зио течет?
λ
А не анбаунд тред пул какой-нибудь
λ
Точно не пул
λ
Кароч за сутки у меня 30гб утекло куда-то :/
λ
Но конечно же я не делал дампов
w
Но конечно же я не делал дампов
R
индукция это тип рекурсия на завтипах
Звучит сложно в реализации, это типа рекурсивное дерево типов?
AG
не, например для натов рекурсор будет
rec : {a : Type} -> a -> ( Nat -> a -> a ) -> Nat -> a
а индуктор ind : {p : Nat -> Type} -> p Z -> ((k : Nat) -> p k -> p (S k)) -> (n : Nat) -> p n