@frp_ru

Страница 386 из 420
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 это такой предикат

? 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
Gadt и в пурсе нет
там это эмулируется через Exists

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

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

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
https://futurice.com/blog/more-gadts-in-purescript
подумал про другого олега, но приемлимая разметка поставила всё по местам

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
а как

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

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

Страница 386 из 420