на zurihac Никлас эту страшную историю расскаывал

а с плагином для рекордов кто-нибудь экспериментировал уже?

lens - лучший плагин для рекордов

у lens же СООБЩЕНИЯ ОБ ОШИБКАХ плохие, поставьте звездочку Гендри

да кто на них смотрит

учишься есть кактус и игнорируешь

Строчку пишут? Уже довольно

хотя-бы из жалости поставьте

описываешь квадратичный рост тут, но может он и был квадратичный?

Это алгоритм поиска квадратичный, то есть мы получаем квадратичное кол-во coercion-ов. А размер каждого coercion-а тоже растет с кол-вом полей, то есть мы получаем coercionSize^coercionAmount, где coercionSize растет тоже квадратично, в итоге (n^2)^(n^2) или вроде того

Наверное

В общем там точно экспоненциальный бардак какой-то был

Жаль не зарепортили пока свежо в памяти было

я не уверен что ты тут имеешь в виду под coercionSIze

то что транзитивно через пару инстансов скоэрситься надо?

синтаксический размер, coercion имеет тип слева и тип справа, эти типы получались очень большие

в обсуждаемых суперрекордах же вроде не квадратичная сортировка и поиск были

да, они и есть

очень похоже на описываемое

там при конструировании тайплевел merge sort вроде

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

ну может и сильно, без этого вообще бы больше 6 элементов в рекорде не тянула или еще что

да не, до этого так же было

я просто автору про эту фигню еще полгода назад рассказал, он на мердж-сорт переписал, но не помогло

это проблема в том, как GHC специализирует, у нас получалась нормальная производительность компиляции с -fno-specialize

Но ес-сно без специализации жизнь грустна

c -O0 жизни нет

самое главное что получался еще code bloat никому не нужный, потому что GHC специализировал эти инстансы

так что не факт, что в рантайме лучше получалось

я для всяких тайпклассов хотел бы специализацию вконце

надо посмотреть на каких рекордах generic-lens будет тормозить

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

и куча методов хотящих MonadBlah

а их в коде всего 3-шт, но опредеяющихся совсем вконце

было бы круто для таких методов делать late specialization

там вообще куча проходов и так

ну вот не делать специализаций вообще

сначала

чтобы .hi в каждом модуле не раздувало

Я не уверен что дело именно в .hi

GHC в памяти тоже все эти преобразования делает

пусть он их дампать не будет — проблема останется

дело не в .hi скорее всего

49272 S.02-levels-added 5976 S.03-float-out 42720 S.04-simplifier 41784 S.05-simplifier

вот эти шаги в основном блоатятся

в симплифаере

при этом там 13 проходов

но плагин-то по идее может же это избежать?

forall x. P(x) => exists x. P(x) forall x. P(x) <=> not exists x. not P(x) Верно?

Не

Вот не пойму, чего нет. Если для всех х P(x) - true, то логично, что существует такой x, что P(x) - true?

Второе не верно, потому что у нас интуиционизм

> Если для всех х P(x) - true, то логично, что существует такой x, что P(x) - true? Не логично

Первое нужно думать. Дело в том, что в интуиционизме следствие это не наличие преобразования

Допустим для всех x из пустого множества P(x)=true

это не значит, что существует такой x, для которого P(x)=true

Хорошо. Если задано непустое множество?

Допустим для всех x из пустого множества P(x)=true

Пустого? Это же свободная квантификация, какие множества?

forall (x :: Void)

Я не про Хаскел, а в общем.

Пока что

Зависимые типы какие-то

Я не про Хаскел, а в общем.

"В общем" это что? Классическая математика?

Если у тебя есть классическая теория предикатов первого порядка, то в ней оба утверждения верны

Если логика интуиционистская, то первое верно, а второе не доказуемо

Как с вами сложно. 😁

Каким образом первое верно? Если forall x. P(x), то это вообще не значит существование хоть одного x

forall x. P(x) это функция, exists x. P(x) это тьюпл

x может принадлежать к ненаселённому кайнду

Каким образом первое верно? Если forall x. P(x), то это вообще не значит существование хоть одного x

Выводимость forall x. P(x) "значит", что для любого терма логики t, P(t) выводимо

правильно

а exists x. P(x) в интуиционизме означает, что P(x) выводимо для какого-то конкретного x и по пруфрелевантности ты должен мочь предоставить этот x

если у тебя есть forall x. P(x), это не значит, что ты можешь взять и предоставить некий x

а потому вывести exists

а exists x. P(x) в интуиционизме означает, что P(x) выводимо для какого-то конкретного x и по пруфрелевантности ты должен мочь предоставить этот x

Что значит не можешь? Возьми любой терм логики и подставь

ну напиши функцию из пи в сигму в агде

Эм????

откуда ты этот терм возьмешь?

Пи и сигма предикативные

А forall импредикативный

что мне дает это утверждение?