ты посмотри на описание математических понятий у Тарского

прикольная э

не помню как она должна выглядеть но вроде не так

https://youtu.be/sb-o1gPFyME?t=865

ты посмотри на описание математических понятий у Тарского

Я ток такого тарского нашёл https://ru.wikipedia.org/wiki/%D0%A2%D0%B5%D0%BE%D1%80%D0%B5%D0%BC%D0%B0_%D0%A2%D0%B0%D1%80%D1%81%D0%BA%D0%BE%D0%B3%D0%BE_%D0%BE_%D0%BD%D0%B5%D0%B2%D1%8B%D1%80%D0%B0%D0%B7%D0%B8%D0%BC%D0%BE%D1%81%D1%82%D0%B8_%D0%B8%D1%81%D1%82%D0%B8%D0%BD%D1%8B

я понял наконец, почему [C a => a] - эксистенциальный тип

нуууу

forall a. [a] должен работать для любых a, в то время как [forall a. a] будет существовать только если хотя бы один a такой существует

ааа

да я это и хотел спросить

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

я просто все пытаюсь понять, как выражается exist через forall через вынос в/за скобки

но чёт мне кажется там все из них являются C a

ну да) это под собой кванторы и подразумевают

forall a. [a] должен работать для любых a, в то время как [forall a. a] будет существовать только если хотя бы один a такой существует

∀ / forall - для всех ∃ / exists - существует такой (хотя бы один)

так

зига

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

я все это прекрасно знаю, иначе бы не использовал эти термины, зачем, бога ради, ты мне это пишешь?)

то есть в принципе

оно должно дать какую-то хорошую интуицию

[forall a. C a => a] населен только если C имеет инстансы, C это такой предикат

я все это прекрасно знаю, иначе бы не использовал эти термины, зачем, бога ради, ты мне это пишешь?)

простите

аааа

ща

правда, forall a. C a => [a] - тоже, так что чет хз

с этой точки зрения стоит посмотреть на случай когда forall глобальный

да

так что хуйня

уже было поверил что вот оно прозрение

простите

вопрос про перенос exist на систему типов хаскеля

так так так

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

то есть почему от переноса forall возникает exist

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

и вроде там оно не так просто работало

а что здесь квадратные скобки делают?

там короче было отрицание в обычной логике

давай что-нибудь попроще спроси

а тут его особо не используют

наверное обычные скобки

только квадратные для понтов

да это норм догадка

(forall n, (n + 1 > n)) -> |N| = inf exist n, (n + 1 > n -> |N| = inf)

нужно в SF главу про логику порешать

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

инфинитив? это откудато совсем далёкого

ну хотя для этого выражения инфнитив уместен

http://www.cyberforum.ru/mathematical-logic-sets/thread1755203.html

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

а второе выводится из первого, говорит, что существует такой n, и это чет нонсенс

а я вроде просто правило применил

ну как там это с инфинитивами работает я не понял но суть в том что понятно как forall сводится к exist

inf - infinity

и тогда в хаскеле такой локальный forall подразумевает глобальный exist для a

inf - infinity

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

да, но я все еще не понимаю как это работает, тождество выше же ложное (forall a. P a) -> B exist a. P a -> B

осталось только словами грамотно произнести по-русски вот эту фразу с экзестенциальным типом

да, но я все еще не понимаю как это работает, тождество выше же ложное (forall a. P a) -> B exist a. P a -> B

да, согласен. оно как-то неубедительное

я нашел что [] это формула тождественна ложна

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

ну без тайпклассов это бессмысленно чет

или без gadt

exist типы без тайпклассов или gadt не говорят нам ни о чем вообще, мы же не можем работать со значениями

Gadt и в пурсе нет

в пурсе и exist нет

Gadt и в пурсе нет

там это эмулируется через Exists

Ну так то да

там это эмулируется через Exists

Я из статьи про эмуляцию и узнал что их нет)

Олеговской?

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

ох

newtype Exists f = MkExists { runExists :: forall r. (forall a. f a -> r) -> r }

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

Во, точно

я уже читал эту статью

в ней по моему ошибка

Вот ещё http://code.slipthrough.net/2016/08/10/approximating-gadts-in-purescript/

в определении Refl-а без гадтов

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

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

должно быть data a := b = Refl { subst :: forall c. c a -> c b } и такая функция действительно есть - id, но она есть только если a = b, в чем и задумка типа в статье же data a := b = Refl { subst :: forall c. c a -> c a }, тут можно подставлять id для любого b

/pidor@SublimeBot

/shipper@shippering_bot

Я перепишу бота

Честно

Когда-нибудь это случится

А тут я вывожу замечательную пару текущего дня. Всем любви, котята! @themishkun + @xgrommx = <3

Ор

Инициирую поиск пидора дня...

Шаманим-шаманим...

Высокий приоритет мобильному юниту.

Кажется, пидор дня - @Adsumus

шо за херня? я не давал согласия на участие

И не надо

бот видит всю суть

а как

почему в прошлый раз кана и гудмайнд

это такой рандом?