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

но эти значения можно признать равными

эти признать можно, да. но ведь это не всегда сработает

можно разрешить бесконечный граф для Stream

можно наверное придумать два элемента в типе, оба в WHNF, доказательство равенства которых будет сложной теоремой или вообще недоказумым:)

по-крайней мере кажется, что так

возникает вопрос, а сколько реально элементов в типе

и корректен ли вообще такой вопрос?

возникает вопрос, а сколько реально элементов в типе

*не "сколько", а просто описать множество попарно неравных значений типа

#(Stream a) = #a ^ א0

это понятно

можно наверное придумать два элемента в типе, оба в WHNF, доказательство равенства которых будет сложной теоремой или вообще недоказумым:)

мне кажется, нельзя. любой дочерний узел будет дном или снова WHNF

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

мне кажется, нельзя. любой дочерний узел будет дном или снова WHNF

я сейчас не про дно. интересуют именно WHNF

конструкторы либо совпадают, либо нет

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

#t = {все "различные" WHNF этого t, где "различные" — ???}

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

кстати, значок решетки - это мощность множества значений ты так обозначил или само множество?

#t = {все "различные" WHNF этого t, где "различные" — ???}

представлены разными конструкторами или ссылаются на различные поля (рекурсия, возможно, бесконечная)

кстати, значок решетки - это мощность множества значений ты так обозначил или само множество?

мощность

я не уверен, что в контексте типов вообще стоит упоминать множества

> Pavel Gilyov: вообще очень сложно говорить о том, настоящий ли человек, наверное Да, часто целая повесть нужна.

> 🌯 animufag 🍺:да скорей всего можно сделать, но набирать сложно Зачем? Есть JuiceSSH. Я так иногда запускаю компиляцию например, или быстро в транспорте что-нибудь подхачиваю.

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

хорошо, что гугл никогда не спит

вот такое нашёл

мы можем сказать, что два некоторых стрима равны экстенсионально, если для них будут равны функции take n и прочее?

как раз то, что ты говоришь - про WHNF

ладно, пойду дальше читать учебник:)

это вообще про равенство функций. хотя функции тоже тип

если я правильно понимаю

про то, что функции (succ . pred) и (pred . succ) не равны интенсионально, но равны экстенсионально

ну вообще они не равны экстенсионально (т.к. minBound), но я понял, что ты имел в виду =)

а вот тут недавно спрашивали, равны ли [1..] и [1..] ++ [2]

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

хотя тут снова фунции, ок

inf + 1 = inf

inf + 1 = inf

Вообще говоря, нет.

Это равенство бессмысленно без уточнения inf и +

а вот 1 + inf = inf скорее всего будет верно в любом случае 🤔

а вот тут недавно спрашивали, равны ли [1..] и [1..] ++ [2]

до редактирования тут было ++ [1], но интереснее конечно с ++ [2]

до редактирования тут было ++ [1], но интереснее конечно с ++ [2]

А какая разница если [1..] НЕ список единиц?

Нет, [1,2,3,...]

[1,1..] - список единиц

я что-то интересное пропустил?

народ интересуется, что есть значение в Хаскелле и что есть равенство значений

ну чё, ребзя, с 9го обратно на гиттер?

прокси!

тор!

за тор, кстати, Богатову продлили домашний арест. Он кстатаи за хаскель в дебианах отвечал

ну чё, ребзя, с 9го обратно на гиттер?

Freenode наше все.

ну чё, ребзя, с 9го обратно на гиттер?

надо запилить клиент нормальный

ну чё, ребзя, с 9го обратно на гиттер?

чего?

в россии вроде собрались телеграм блочить

опять?

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

т.е этот чатик можно просто оставить как есть

в россии вроде собрались телеграм блочить

На основании чего?

на основании того, что дебилы

там в видео про телеграм

и потому, что могут

На основании чего?

мопед не мой, я вообще белорус из вильнюса

Удобно

на основании того, что дебилы

Да глупости какие, буржуазное государство работает не так. Наше государство пока не засветилось в нарушении собственных законов. Законы, конечно, весёлые, но они везде весёлые. Если они решились заблочить, то нашли лазейку в законах, вот интересно чо за лазейка

телега не предоставила ФСБ какие-то там ключи для расшифровки трафика

фейсбук с гуглом банить ссут. линкедин забанили

Фейсбук с гуглом сотрудничают с российской властью

Гугл даже с Китайцами сотрудничает, чо уж там

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

РФ до Китая как сколково до кремниевой долины.

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

Конечно, у гугла дата-центр в москве

РФ до Китая как сколково до кремниевой долины.

У китая в 10 раз более зверские законы в этом плане

Россия же с китая пример и берёт

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

большая ошибка, конечно, недоучёт ментальных особенностей народа

гугл кстати не знает про свой дата-центр в москве

большая ошибка, конечно, недоучёт ментальных особенностей народа

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

ну чё, ребзя, с 9го обратно на гиттер?

ну уж по сравнению с х-лем настройка прокси/тора не такое сложное дело =) думаю, тут все грамотные

большевики в своё время обошлись без твиторов, и их тоже было немного