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

ну так вероятность увеличивается

и понять что пошло не так будет чуток сложнее

на другой базе вообще смысла не вижу тестить

там еще аргумент - "с инмемори базой тесты быстрее идут"

не понятно куда спешим

ну и в кросс-базовыми ORM все плохо, т.к. базу выбираешь обычно ради её уникальных фич, а не общего функционала со всеми остальными

а в подобных решениях специфические фичи не поюзаешь, ради сомнительной поддержки кучи стореджей

а мне ещё не нравится маппинг на объекты автоматом

во всяких орм

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

жаль, с исключениями это не работает

жаль, с исключениями это не работает

C зависимыми типами в экзистенциальной обёртке и Data.Type.Equality проканает. Но как-то это.. ректально даже без термо.

Если экзистенциально обернуть Data.Type.Equality, останется Proxy

А если дважды обернуть, то ()

целый день я ёжика рожу

Лестничные операторы рождения и уничтожения ёжиков

A что мы вообще с экзистенциальным типом можем делать? Мы же не знаем, какой это конкретно тип?

иногда это же только на пользу

мы можем “что-то” о нем знать и поэтому можем то же “что-то” делать

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

например, благодаря этому можно тайпчекать длины фиксированных векторов, которые от входных данных зависят и т.д.

поэтому мы можем использовать бульбоморфизмы, даже не зная больших деталей

Если дан какой-то экзистенциальный тип e, то в контексте может быть некий констрейнт Foo e предоставляющий операции над ним (как @catamorphism говорит). И эти констрейнты могут отличаться в разных ветках кейса если использовать GADT-ы (как @A64m_qb0 упомянул на примере с длиной вектора)

К тому же кому в положительной позиции existential, а кому в отрицательной universal

Если функция f :: forall a. a -> a то она тоже ничего про a не знает

если f :: forall a. Foo a => a -> a то знает Foo

если f :: forall a. a ~ Int => a -> a то уже и конкретный тип знает

экзистенциальность дает возможность неизвестный тип не принять, а вернуть

skolem он и есть skolem (выбрали за нас), вне зависимости от квантификатора

Если функция f :: forall a. a -> a то она тоже ничего про a не знает

f = id

это какой-то параметрический рефлекс?

это какой-то параметрический рефлекс?

Именно, что рефлекс 🤣

жаль Haskell нетотальный и f имеет бесконечно много операционно разных реализаций

(денотационно одинаковых, но это ровно до ближайшего catch)

экзистенциальность дает возможность неизвестный тип не принять, а вернуть

Так. Хорошо. Я плохо это понимаю, и в этом мой интерес. Haskell не имеет синтаксиса exist, верно. Как вернуть неизвестный тип. Как это вообще?

через CPS или обертку

Рассмотри функцию f :: A -> B, ты ее можешь переписать как f :: A -> (B -> r) -> r

жаль Haskell нетотальный и f имеет бесконечно много операционно разных реализаций

тотальный же тоже может иметь бесконечно много операционно разных реализаций

всегда можно еще один id прикомпозить и получить очередную завершающуюся имплементацию id

Рассмотри функцию f :: A -> B, ты ее можешь переписать как f :: A -> (B -> r) -> r

Вот оно. Корень зла. Я такое уже видел, но мне не совсем понятно, почему так :(

Потому что если есть f :: A -> B, то есть f' :: A -> (B -> r) -> r) где f' a cont = cont (f a)

чисто механическое преобразование

всегда можно еще один id прикомпозить и получить очередную завершающуюся имплементацию id

можно зато доказать что любой well-typed терм a -> a можно переписать в id

если с f ты будешь получать результат и биндить его в let типа такого: let x = f a in DoStuffWith(x) то с f' ты будешь передавать continuation как аргумент: f' a $ \x -> DoStuffWith(x)

Потому что если есть f :: A -> B, то есть f' :: A -> (B -> r) -> r) где f' a cont = cont (f a)

Так, хорошо. Это понятно. Но f и f' не эквивалентны, с точки зрения типов. И мне не ясно причем тут exist

можно зато доказать что любой well-typed терм a -> a можно переписать в id

да, можно, но речь была вроде не совсем про это

Так вот, если ты хочешь, чтобы внутри возвращаемый B был неизвестным типом, то в случае с f тебе нужен новый квантификатор (f :: exists e. A -> e), а в случае в f' ты используешь forall — f' :: A -> (forall e. e -> r) -> r

Потому что exists в положительной позиции превращается в forall в отрицательной

Экзистенциальные обертки дают примерно тот же самый эффект. forall при конструировании дает exists при деконструировании

Инуитивно: если функция может вернуть что угодно (exists), то continuation должен уметь принять что угодно (forall). Если в конструктор можем положить что угодно (forall), то при матчинге должны уметь обработать что угодно (exists)

Очень круто. Я не всё понял, но постараюсь. Что почитать, чтоб не разводить флуд? Желательно попроще. Я JS-ер 🤣

мы по юзерпику поняли

мы по юзерпику поняли

Юзерпик?

А, собачка? :)

тотальный же тоже может иметь бесконечно много операционно разных реализаций

Согласен, мое недовольство скорее в том, что мы объявляем одну денотацию (боттом), а на деле можем наблюдать операционные различия (catch позволит отличить разные типы исключений, а non-termination вообще отдельно идёт)

а по моему юзерпику какой язык определяется?

а по моему юзерпику какой язык определяется?

APL

а по моему юзерпику какой язык определяется?

фортран/апл

на увеличенной версии клавиатура под апл не подходит

согласно Лурку

Стереотипный, скорее :)

я в твиттере и похуже видел

Стереотипный, скорее :)

стереотипизированный

типичный программист на Хаскеле - накачанный полубог - техлид

на увеличенной версии клавиатура под апл не подходит

J

типичный программист на Хаскеле - накачанный полубог - техлид

это в пору до mtl так было

типичный программист на Хаскеле - накачанный полубог - техлид

О, это я.

а теперь все скукожились в хикка-гиканов?

да, потому что lift перестали использовать

не liftят, lensами зрение портят

точно

совпадение? не думаю.

до mtl не было ничего

Кстати, что за хайп такой вокруг этих Lens?

Потому что в Haskell забыли человеческие record updates подвезти

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

А потом Kmett решил исправить это так, что решил еще 30 проблем и вылечил рак

получились lens

"- А что, вы и лифтить за меня будите?"

"- А что, вы и лифтить за меня будите?"

🤣 Это сильно.