типа того

на идрисе я что-то подобное изобразил, а здесь не могу

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

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

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

но может и так можно

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

"паттерн матчинг" в кавычках конечно

Vasiliy понимаешь такое решение? или сделать пример

пока не понимаю, пробую

тут плохо что смотри, есть Map a ts и Map b ts компилятор не знает что они '[] одновременно

поэтому даже fs HNil = HNil ты просто так написать не можешь, вроде

да, это я понял...

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

да, скомпилировалось

через классы типов?

vinyl-решение

на самом vinyl или сам написал?

просто вот в vinyl у тебя есть этот удобный type level list по которому ты матчить можешь

ну вот твоё определение скопировал, подправил, где надо

а операции над типами идут над первым аргументом

итого у нас меньше информации теряется из-за неинъективных функций

я уверен что с твоим подходом это бы заработало, но это hard way

отличненько, и в другом месте скомпилилось

спасибо!

Dmitry кстати на мои диалоги опасно смотреть со стороны, т.к. я стараюсь не решать XY проблемы правильно, т.к. мне часто интересно сделать то, о чем спрашивает человек, так что я обычно упоминают решение и стараюсь решить то что просят

норм, мне тож нравятся головоломки

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

или не откидывать

но если читать диалог со стороны то может выглядеть как борьба с ветряными мельницами

вообще да, тот фрагмент кода выглядел совсем нетривиально

увы, но такого рожна полно и в нормальных либах...

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

по сравнению с вычислениями на типах в idris в haskell type families выглядит печально

yesod это достаточно интересный экземпляр кода

Снойман вообще интересный человек совсем необычный haskell-лист

или тот же servant — весьма, весьма своеобразный код

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

сервант - это воще жесть

при этом у него (не знаю как сейчас) но раньше очень страдало образование

я не знаю, как люди пишут что-то без него

conduit - экземпляр того что бывает если пытаться не читать статьи и решения и переизобретать

😃

так вот есод это очень огромный овериженеренный кусок кода написанный в своём совсем стиле

т.к. в нём писать неудобно то ещё и с кучей генерации кода

conduit - экземпляр того что бывает если пытаться не читать статьи и решения и переизобретать

вот когда с conduit ковырялся, тоже казалось, что авторы болели синдромом NIH

на TH который сильно рушит бонусы от систем типов

потом полез читать про pipes, там габриэль расписал всякие категории, законы итд, всё стало как-то просто и понятно

ты посмотри на первые версии

там где все на IORef

там реально он прошёл по всей истории streaming библиотек

удивительнее всего, что самой популярной библиотекой для iteratee были enumeratee Сноймана

хотя если бы он действительно прочитал и понял статьи, то минимум бы понимал то, что понял написал conduit-0.4 или 0.5

у него там внутренний дизайн каждую версию менялся

наверное на conduit-1.1 он догнал прогресс

опять же удивительно но эта либа была и есть популярнее pipes и до этого

вот yesod это продукт из той же серии

большой непотопляемый источник хтонического ужаса

есть кондуиты есть пайпы) вот чот я больше Гонзалезу доверяю

ну, популярность, наверное, засчёт огромного количества постов в блогах и всякого такого

too big too sink как выразились fp комплитовцы когда обсуджали всякую фигню после zurihac

да вот хз

в общем он делает очень много и очень шумно

и оно работает

в большинстве случаев

а те, кто попадают в меньшинство обычно достаточно умные чтобы справиться сами

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

https://twitter.com/TheWizardTower/status/910399586950189056

но кому как

есть люди которые дракон хотят

везде

а вот это бесит: • Couldn't match type ‘StM m ()’ with ‘()’ Expected type: IO (StM m ()) Actual type: IO ()

хотя с другой стороны когда не это то: Also: java.lang.NullPointerException at org.csanchez.jenkins.plugins.kubernetes.pipeline.ContainerExecDecorator.close(ContainerExecDecorator.java:275) at org.csanchez.jenkins.plugins.kubernetes.pipeline.Resources.closeQuietly(Resources.java:33) причем второе в рантайме готового проекта..

а вот это бесит: • Couldn't match type ‘StM m ()’ with ‘()’ Expected type: IO (StM m ()) Actual type: IO ()

но ведь здесь может быть и не ()

ты в курсе такого класса проблем?

если у тебя есть какая-то ошибка любая, то компилятор не может вывести m

как следствие он не может ресолвить StM m ()

дык функция StM в одну сторону определена

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

т.е. ошибка совершенно в другом месте