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

ДАА ?

видел где-то определение множества как пары функции принадлежности и равенства но зачем равенство, если (forall a in A. a in B) and |A| = |B| <=> A = B

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

Что проявляется уже в ряде принципов идриса, например. Да на всех на самом деле проявляется

Все хотят тьюринг-полную систему типов (зануда-мод: не все конечно), но как только ты получишь её, ты просто обнаружишь себя с ещё одним типичным слоем в логике приложения с типичными проблемами

Поэтому вся вот эта абстракция не так легко даётся авторам языков, потому что шаг влево шаг вправо и у тебя проблема останова

видел где-то определение множества как пары функции принадлежности и равенства но зачем равенство, если (forall a in A. a in B) and |A| = |B| <=> A = B

А ты уверен, что у тебя здесь не выводятся те же самые утверждения?

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

Да и вообще говоря могут совместно существовать системы на разных постулатах

как лучше назвать типы для Арных функций ?

Arity0<R>

Arity1<T1, R>

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

у рамды тайпинги совсем не вменяемые

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

толи я не догоняю в 3 ночи, толи хз) но зачем это в пурсе?) http://try.purescript.org/?gist=1304cf5bdc3af1cefa5f0a9e263d5d49&session=0548d95f-ace6-0132-6b53-a4c79b686f4a

Ого, мощная штука

Оочень мощная по ходу

Я всегда задавался вопросом, почему есть ∀ но нет ∃

Вот это ∃ и есть

(то что в Data.Exists чепушня какая-то, стримы какие-то, чзнх)

с этим есть вопросы такая фигня называется экзистентиональная (exist, ∃) квантификация, но я знаком, как в пурсе происходит работа с тайпклассами, там инстансы из иплиситной передачи в пурсе-коде начинаются передаваться эксплиситно в js-коде как аргумент

и как это будет работать с exist, где мы не знаем, что за инстанс

Через замыкание

Там тащемта есть кнопка Show JS

у хаскелл есть такой Forall https://hackage.haskell.org/package/constraints-0.9.1/docs/Data-Constraint-Forall.html

Интересно, насколько можно высушить такой код, если пройтись по нему Uglify с кложур компилером (благо пурса из коробки CC-Friendly)

а, лол, это не existentially quantified types и это не работает

https://gist.github.com/CMCDragonkai/b203769c588caddf8cb051529339635c

ну это же самый обыкновенный Черч newtype Forall f = Forall (forall r. f r) runForAll :: forall f r o. (f r -> o) -> Forall f -> o runForAll f (Forall l) = f l newtype Maybe' a r = Maybe' {runMaybe :: r -> (a -> r) -> r} type MMaybe a = Forall (Maybe' a) nothing :: forall a. MMaybe a nothing = Forall (Maybe' const) just :: forall a. a -> MMaybe a just x = Forall (Maybe' $ \_ j -> j x) maybe :: forall a r. r -> (a -> r) -> MMaybe a -> r maybe n j = runForAll $ \(Maybe' f) -> f n j

а оно и не будет

но я, кстати, не понимаю, почему это называется exist

если это вполне себе forall

те есть вот некоторые говорят, что правильно было бы записывать тип MyShow1 как MyShow1 :: (exist a. Show a => a) -> MyShow1 но это же вполне себе MyShow1 :: forall a. Show a => a -> MyShow1 что хаскель и показывает

или это внесение forall за скобки превращает его в exist?

forall n in Nat. n + 1 > n -> Prop (exist n in Nat. n + 1 > n) -> Prop че

аааа, хм, да, это имеет смысл

типа специализированная версия

или это внесение forall за скобки превращает его в exist?

++ Set(∫^x p x x, c) ≅ ∫_x Set(p x x, c) Функция, берущая экзистенциальный тип должна быть готова для того, чтобы она могла взять любой тип

так

это че за интегралы

я тут шарагу закончил

К примеру функция, которая берёт сумму в типе, имплементируется как кейс для каждого типа, представленного в сумме

∀ a ∋ A. a ∋ B → A ⊃ B (∃ a ∋ A. a ∋ B) → A ⊃ B вот так можно судить?

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

∀ a ∋ A. a ∋ B → A ⊃ B (∃ a ∋ A. a ∋ B) → A ⊃ B вот так можно судить?

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

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

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

чет я это не понял...

ой, мемес с дуальностью

пойду на html писать

http://comonad.com/reader/2008/kan-extension-iii/ Ещё где-то видел хороший пример на доказательстве ниндзя леммы йонеды, там весь этот мусор с теоркатом

А вообще тут речь уже идёт не о функциях, а об отношениях

символ интеграла это как и есть (сумма) тут?

символ интеграла это как и есть (сумма) тут?

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

^x <- top _x <- bottom ?

я в теоркат глубоко еще не погружался

^x <- top _x <- bottom ?

$$\int_{∀}^{∃}$$ Так читабельнее?

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

а где про это прочитать? и почему Риман? его геометрия?

а где про это прочитать? и почему Риман? его геометрия?

Бе-решит(книга Бытия) IV том, Ветхий Завет

Бе-решит(книга Бытия) IV том, Ветхий Завет

шутим?

(forall a. P a) -> Void - exist forall a. P a -> Void - forall это то же самое not (exist a. P(a)) = forall a. not (P a)

ERROR: S client not available

это верно?

так лол, в пурсе нет gadt

как код тогда писать?

так лол, в пурсе нет gadt

а зачем и сужать типы?) они пишут себе на реакте что обернут в пурсу)

http://code.slipthrough.net/2016/08/10/approximating-gadts-in-purescript/

https://futurice.com/blog/more-gadts-in-purescript

ты просто кидаешь первые результаты гугла

Leibniz...

во второй статье пример Refl типа

который не работает

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

algebraic effects :D https://gist.github.com/sebmarkbage/2c7acb6210266045050632ea611aebee

http://blog.ezyang.com/2010/10/existential-type-curry/

по мотивам Стефена Диля https://github.com/mjepronk/wiwinwl-purescript

Всем привет. В js где могут использоваться бифункторы или нечто подобное? Сначала подумал про работу с промисами, где в then указываем resolve и reject, но обработаная ошибка не считается ошибка - то, что прошло через reject дальше по цепочке попадет в resolve. Есть в js что-нибудь нативное, что ведет себя как здесь https://github.com/fantasyland/fantasy-land#bifunctor ?

either, tuple

Всем привет. В js где могут использоваться бифункторы или нечто подобное? Сначала подумал про работу с промисами, где в then указываем resolve и reject, но обработаная ошибка не считается ошибка - то, что прошло через reject дальше по цепочке попадет в resolve. Есть в js что-нибудь нативное, что ведет себя как здесь https://github.com/fantasyland/fantasy-land#bifunctor ?

у fluture тоже

а

нативное нет конечно

Всем привет. В js где могут использоваться бифункторы или нечто подобное? Сначала подумал про работу с промисами, где в then указываем resolve и reject, но обработаная ошибка не считается ошибка - то, что прошло через reject дальше по цепочке попадет в resolve. Есть в js что-нибудь нативное, что ведет себя как здесь https://github.com/fantasyland/fantasy-land#bifunctor ?

.catch(e => Promise.reject(f(e)))

А ну да, если ошибку в reject-е каждый раз пробрасывать, то будет как бифунктор. Просто осмыслить не мог, где это может пригодится

?

Я не один, кто увидел в этом нечто экозитическое)

Что именно?

promap всесто dimap?