
Denis
06.02.2018
20:29:50
ты посмотри на описание математических понятий у Тарского

? animufag ?
06.02.2018
20:30:29
прикольная э
не помню как она должна выглядеть но вроде не так

Denis
06.02.2018
20:33:12
https://youtu.be/sb-o1gPFyME?t=865

Google

Дмитрий
06.02.2018
20:33:19
ты посмотри на описание математических понятий у Тарского
Я ток такого тарского нашёл 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

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

? animufag ?
06.02.2018
22:40:39
нуууу

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

? animufag ?
06.02.2018
22:40:53
ааа
да я это и хотел спросить
мол слово экзистенциальный или почему именно здесь

kana
06.02.2018
22:41:54
я просто все пытаюсь понять, как выражается exist через forall через вынос в/за скобки

? animufag ?
06.02.2018
22:41:54
но чёт мне кажется там все из них являются C a

Denis
06.02.2018
22:42:21
ну да) это под собой кванторы и подразумевают

kana
06.02.2018
22:44:03
так
зига

Google

? animufag ?
06.02.2018
22:44:17
короче я сейчас не пойму, так что можешь не тратить время на объяснение
ноо оно кажется и так непонятным

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

? animufag ?
06.02.2018
22:44:25
то есть в принципе
оно должно дать какую-то хорошую интуицию

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

Denis
06.02.2018
22:45:50

? animufag ?
06.02.2018
22:45:56
аааа
ща

kana
06.02.2018
22:46:32
правда, forall a. C a => [a] - тоже, так что чет хз

? animufag ?
06.02.2018
22:46:37
с этой точки зрения стоит посмотреть на случай когда forall глобальный
да
так что хуйня
уже было поверил что вот оно прозрение

kana
06.02.2018
22:47:18
простите
вопрос про перенос exist на систему типов хаскеля

? animufag ?
06.02.2018
22:48:47
так так так
для начала нужно разобраться как работают правила в этой логике
то есть почему от переноса forall возникает exist
это должно иметь соответствие с обычной логикой с предикатами
и вроде там оно не так просто работало

kana
06.02.2018
22:50:24

Google

? animufag ?
06.02.2018
22:51:26
а что здесь квадратные скобки делают?
там короче было отрицание в обычной логике

kana
06.02.2018
22:51:42
давай что-нибудь попроще спроси

? animufag ?
06.02.2018
22:51:44
а тут его особо не используют

kana
06.02.2018
22:51:58
наверное обычные скобки
только квадратные для понтов

? animufag ?
06.02.2018
22:52:18
да это норм догадка

kana
06.02.2018
22:53:03
(forall n, (n + 1 > n)) -> |N| = inf
exist n, (n + 1 > n -> |N| = inf)
нужно в SF главу про логику порешать
мне кажется это что-то очень примитивное

? animufag ?
06.02.2018
22:54:04
инфинитив? это откудато совсем далёкого
ну хотя для этого выражения инфнитив уместен

Denis
06.02.2018
22:56:20
http://www.cyberforum.ru/mathematical-logic-sets/thread1755203.html

kana
06.02.2018
22:56:23
ну я таким образом показал, что если для любого n можно построить на одно больше, то мощность множества - бесконечность
а второе выводится из первого, говорит, что существует такой n, и это чет нонсенс
а я вроде просто правило применил

? animufag ?
06.02.2018
23:00:36
ну как там это с инфинитивами работает я не понял
но суть в том что понятно как forall сводится к exist

kana
06.02.2018
23:01:04
inf - infinity

? animufag ?
06.02.2018
23:01:17
и тогда в хаскеле такой локальный forall подразумевает глобальный exist для a
inf - infinity
да у меня на практике по матану точно говорили инфинитив, а в русском матане слова брались отовсюду и зачастую не из англ

Google

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

? animufag ?
06.02.2018
23:03:03
осталось только словами грамотно произнести по-русски вот эту фразу с экзестенциальным типом

Denis
06.02.2018
23:05:41
я нашел что [] это формула тождественна ложна

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

kana
06.02.2018
23:07:50
ну без тайпклассов это бессмысленно чет
или без gadt
exist типы без тайпклассов или gadt не говорят нам ни о чем вообще, мы же не можем работать со значениями

Дмитрий
06.02.2018
23:08:27
Gadt и в пурсе нет

kana
06.02.2018
23:08:41
в пурсе и exist нет

Denis
06.02.2018
23:08:49

Дмитрий
06.02.2018
23:08:49
Ну так то да

Denis
06.02.2018
23:09:40
Олеговской?
https://futurice.com/blog/more-gadts-in-purescript
ох
newtype Exists f = MkExists { runExists :: forall r. (forall a. f a -> r) -> r }

Дмитрий
06.02.2018
23:11:11

kana
06.02.2018
23:13:16
я уже читал эту статью
в ней по моему ошибка

Google

Дмитрий
06.02.2018
23:13:31
Вот ещё http://code.slipthrough.net/2016/08/10/approximating-gadts-in-purescript/

kana
06.02.2018
23:13:40
в определении Refl-а без гадтов

? animufag ?
06.02.2018
23:13:42

kana
06.02.2018
23:14:45
должно быть
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

SHIPPERING
06.02.2018
23:15:30
Я перепишу бота
Честно
Когда-нибудь это случится
А тут я вывожу замечательную пару текущего дня. Всем любви, котята! @themishkun + @xgrommx = <3

Dmitry
06.02.2018
23:15:42
Ор

Sublime Bot
06.02.2018
23:15:42
Инициирую поиск пидора дня...
Шаманим-шаманим...
Высокий приоритет мобильному юниту.
Кажется, пидор дня - @Adsumus

Denis
06.02.2018
23:16:41
шо за херня? я не давал согласия на участие

Dmitry
06.02.2018
23:16:56
И не надо

kana
06.02.2018
23:16:58
бот видит всю суть

? animufag ?
06.02.2018
23:17:18
а как
почему в прошлый раз кана и гудмайнд
это такой рандом?