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

Никак, это дуальные понятия, их вместе не используют. Оперируют либо за отдельно замкнутыми множествами, либо отдельно открытыми

Какую ты проблему решаешь изначально? Чувствую XY

хочу нормальный маркер для вот этого всего вместо Bool

Множеству не обязательно вообще быть открытым или замкнутым.

И не обязательно быть исключительно либо открытым, либо замкнутым. Можно быть и тем, и другим.

хочу нормальный маркер для вот этого всего вместо Bool

Нет, явно изначально ты решаешь не эту проблему. Задачу-то какую решаешь, откуда ты замкнутые и открытые множества взял

Потому что, опять же, никто не оперирует этими понятиями одновременно

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

И не обязательно быть исключительно либо открытым, либо замкнутым. Можно быть и тем, и другим.

Ну так он и ввел 4 конструктора

Both и т.д.

Пропустил код.

хочу нормальный маркер для вот этого всего вместо Bool

(Bool, Bool) твой маркер

Только нафига это нужно, и правда непонятно

(Bool, Bool) твой маркер

Так я от булов и хочу уйти

Понял, тебе надо закрытость и открытость в одно слово смэшить

Чтобы тип назвать

Так?

Чтобы тип назвать

Тип о 4 конструкторах

не помню, чтобы эту классификацию как-то называли

"по открытости"

или "по замкнутости"

Да заведи просто два типа изоморфных Bool, и запихни их в тип, изоморфный паре

а как его назвать?)

тип, изоморфный паре

Вот для этого и пара

Чтоб не называть, но он так не хочет

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

Clopen :)

f :: (Openess, Closeness) -> IO ()

Норм читается

а как его назвать?)

👆

на хаскеле?

^

А по-русски можно?

А по-русски можно?

пофиг. лишь бы на хаскеле можно было

ну тип для конструкторов Foo и Bar всегда можно назвать FooBar, и сэкономить время на придумывание чего-то получше

data COBN

всё, обошёлся изобретением темплейтов 😩

то есть почему при выборе инстанса не учитываются ограничения?

да, про это вот всё

не пруфассистант. все эти потуги в сторону "тотальности" в хаскеле - это как ФП на C++

с одной стороны, уровень безнадежности примерно тот же. с другой стороны, лямбды в C++ всё же завезли

в Haskell totality checker нужен для оптимизации, чтобы Refl в рантайме не конструировать

доказывать так ничего не возьмешься, разумеется

ну, в смысле, возьмешься, но всё будет с оговоркой, что никто нигде bottom не сотворил, то есть это не доказательство, а скорее sanity check кода

А вот когда доделают левити полиморфизм

смотря что подразумевается под доделанным

Unlifted types разве есть сейчас в GHC? Могу я попросить на вход функции анлифтнутый тип?

ну я имел в виду не Levity polymorphic data types а пменно анлифтнутые типы

в какой нибудь форме

массивы разве что

ну т.е. нет

unboxed sum есть

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

unlifted типы тоже

так анбокснутые суммы они не только анлифтнутые

ну пихнуть туда Array#

а еще и анбокснутые ..

анлифтнутые это когда не надо за ленивость платить

он вроде unlifted boxed

но это тот ещё ад

оно вообще интересно заработает?

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

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

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

но бекпаком вообще можно левити полиморфный код писать, с 8.4

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

вот собственно и все

планов не очень много, так что и доделывать особо нечего

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

если бы обычные типы незаметно дешугарились в ньютайпы и паттерн-синонимы, можно было закоэрсить data T = A | B и data X = M | N не знаю, хорошо это или плохо

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

но вот коэрсить списки и индексированные длиной списки было бы точно прикольно

при условии, что там equality proof каким-то образом анбокснулся и на рантайм-представлении не отразился

вроде я видел пример где дерайвинг виа делается для эквивалентных с точки зрения структуры типов (на дженериках)

это же фактически коерс

так соль коерса в том, что он id

а на генериках там по воле оптимизатора

не, речь не про преобразование на дженериках, это сто лет возможно

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

да ладно

не представляю себе как это работает

в пейпере по DerivingVia это есть?

я тоже Ж((