These are chat archives for groupoid/exe

5th
Aug 2016
Namdak Tonpa
@5HT
Aug 05 2016 08:31
сделал вброс на реддит, знаю что рано но все же https://www.reddit.com/r/dependent_types/
Zeit Raffer
@zraffer
Aug 05 2016 08:44
Все куда-то спешат )
This message was deleted
Namdak Tonpa
@5HT
Aug 05 2016 10:46
надо было в https://www.reddit.com/r/types постить, рядом с андромедой
Zeit Raffer
@zraffer
Aug 05 2016 10:47
андромеда моя андромеда (пару минут на перезагрузку)
Namdak Tonpa
@5HT
Aug 05 2016 10:47
первый камент положительный :-)
это хорошо
Zeit Raffer
@zraffer
Aug 05 2016 10:58
а на андромеду за 7 дней ни одного коммента
ты выбрал правильный топик
Namdak Tonpa
@5HT
Aug 05 2016 10:58
в четверг я шлю Хенку письмо :-) в четверг благоприятный день
говорю что мы не верим в Британскую школу и т.д. что мы хотим быть ближе к истокам и AUTOMATH ..
Zeit Raffer
@zraffer
Aug 05 2016 10:59
в один из четвергов) не спеши) я напишу транслятор на агде или леан
а шо за британская школа??
Namdak Tonpa
@5HT
Aug 05 2016 11:00
ну все эти Сейнт Эндрю и т.п.
Агда, Идрис и т.д.
Zeit Raffer
@zraffer
Aug 05 2016 11:00
может не надо гнать все время? а то уже привык )
Namdak Tonpa
@5HT
Aug 05 2016 11:01
с другой стороны та статья про "not derivable" это ж из того института где Хенк
Неймиген
Zeit Raffer
@zraffer
Aug 05 2016 11:01
на статьюнадо написать контрстатью. во как!
Namdak Tonpa
@5HT
Aug 05 2016 11:01
ну я действительно не верю в Агду
Zeit Raffer
@zraffer
Aug 05 2016 11:01
разобрать их доказательство
Namdak Tonpa
@5HT
Aug 05 2016 11:01
шо тут гнать )
Zeit Raffer
@zraffer
Aug 05 2016 11:01
а что значит не верю?
надо покупать SSD а то 10 мин перезагружаться это как-то слишком
Namdak Tonpa
@5HT
Aug 05 2016 11:03
незнаю что-то иррациональное
Zeit Raffer
@zraffer
Aug 05 2016 11:03
отторжение агды )
а как тебе скобочки? оставляем? или попытаемся упростить синтаксис?
Namdak Tonpa
@5HT
Aug 05 2016 11:04
оставляем
Zeit Raffer
@zraffer
Aug 05 2016 11:04
гы
Namdak Tonpa
@5HT
Aug 05 2016 11:04
а что ты уростить хочешь?
Zeit Raffer
@zraffer
Aug 05 2016 11:05
не ну просто, такой стиль, что много скобочек. мы заговорили про агду, там скобочек почти нет, как в хаскелле
Namdak Tonpa
@5HT
Aug 05 2016 11:06
ну у нас же стилистика Lean которая к LISP восходит
Zeit Raffer
@zraffer
Aug 05 2016 11:06
я кстати не знаю, кто начал такую безскобочную моду, через отступы, не подскажешь?
питон там
Namdak Tonpa
@5HT
Aug 05 2016 11:07
Британская школа
Zeit Raffer
@zraffer
Aug 05 2016 11:07
блин ))
Namdak Tonpa
@5HT
Aug 05 2016 11:07
британские ученые
:-)
это ж HOPE и Miranda
оттуда пошел Хаскель а дальше Агда и Идрис
Zeit Raffer
@zraffer
Aug 05 2016 11:08
я помню был эксперименальный древний язык OCCAM с параллельными каналами, там вроде уже были эти отступы
Namdak Tonpa
@5HT
Aug 05 2016 11:08
HOPE 1970, OCCAM 1983
Zeit Raffer
@zraffer
Aug 05 2016 11:08
о!
Namdak Tonpa
@5HT
Aug 05 2016 11:09
LISP -> AUTOMATH -> Lean -> EXE/OM такая приемственность
ОМ кстати больше на ЛИСП похож
Zeit Raffer
@zraffer
Aug 05 2016 11:10
ОМ похож на лямбда-выражения ) которыми он и является ))
Namdak Tonpa
@5HT
Aug 05 2016 11:10
ну есть разные виды лямбд
Zeit Raffer
@zraffer
Aug 05 2016 11:10
шо, есть без скобочек?
Namdak Tonpa
@5HT
Aug 05 2016 11:10
\ x. x, \ x -> x, \ (x) -> x
Zeit Raffer
@zraffer
Aug 05 2016 11:10
ну это да
Namdak Tonpa
@5HT
Aug 05 2016 11:10
у нас со скобочками, чтобы подчеркнуть приемственность от лиспа
Zeit Raffer
@zraffer
Aug 05 2016 11:11
надо написать в реадми
Namdak Tonpa
@5HT
Aug 05 2016 11:11
ну это все натянутая философия, но я опишу если хочешь
но это тогда будет четкое разграничение между британской школой )
надо оставить пути отступления
Zeit Raffer
@zraffer
Aug 05 2016 11:12
moar parenthesis! moar!
Namdak Tonpa
@5HT
Aug 05 2016 11:12
если Хенк не возьмет покровительство я думаю к МакБрайду идти :-)
Zeit Raffer
@zraffer
Aug 05 2016 11:12
он говорит неразборчиво)
я ничего не разбираю
увидел на реддите статью Байера http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/
я ее помню
это ужас какой-то
полный пиздец операционной семантике
каким-то образом эти программы завершаются
я пробовал на Скале это переписать
работает
но как?
effectfully
@effectfully
Aug 05 2016 11:27
у него есть продолжение: http://math.andrej.com/2014/05/08/seemingly-impossible-proofs/
Zeit Raffer
@zraffer
Aug 05 2016 11:29
интересно! я пропустил
спасибо
effectfully
@effectfully
Aug 05 2016 11:30
пожалуйста
Zeit Raffer
@zraffer
Aug 05 2016 11:30
а вы разобрались, почему оно работает?
я не читал подробно этого Мартина Эскардо статьи, вроде бы он намекает, что причиной всему компактность
effectfully
@effectfully
Aug 05 2016 11:32
не, я не разбирался
подумал "скорее всего просто ленивость" (как в https://stackoverflow.com/questions/32988409/minimum-height-in-tree) и поленился
сейчас пробежал глазами и похоже, что там больше, чем просто ленивость
Zeit Raffer
@zraffer
Aug 05 2016 11:34
еще бы как-то использовать этот фокус на практике :)
не очень хорошее ) Шульман говорит I'm confused
у нас так не должно быть )
Zeit Raffer
@zraffer
Aug 05 2016 11:46
ну вот )) слон с китом разборки устроили )))))
Шульман с Байером
он кстати Байер или Бауер? Как фамилиё читаетсо?
я так понимаю, что последние недели во всех тематических блогах обсуждают андромеду ) нам бы так )))
Namdak Tonpa
@5HT
Aug 05 2016 14:31
Работаем над этим
Namdak Tonpa
@5HT
Aug 05 2016 15:33
добавлю в semantics.htm правила для HIT :-)
для затравочки
Zeit Raffer
@zraffer
Aug 05 2016 16:03
Нуну
Namdak Tonpa
@5HT
Aug 05 2016 16:03
ну я думаю там пусть будет Equ, W и HIT в EXE секции
равенство, индуктивные и высшие индуктивные
Zeit Raffer
@zraffer
Aug 05 2016 16:04
Ага. Только это ж типы, не семантика
Namdak Tonpa
@5HT
Aug 05 2016 16:04
ну у нас только типы
другого ничего нет
по 4 правила на тип
Universe, Pi, Equ, W и HIT
вроде все
больше ничего нет
Zeit Raffer
@zraffer
Aug 05 2016 16:07
Так скажут что в групоиде не знают, что такое семантика
Namdak Tonpa
@5HT
Aug 05 2016 16:07
ну я тогда переименую страницу
Zeit Raffer
@zraffer
Aug 05 2016 16:07
О!
Namdak Tonpa
@5HT
Aug 05 2016 16:07
ну это все равно семантика
во всех документах что я вижу в инете — это называется семантикой
то что ты хочешь record data и codata туда повписывать — это как бы другой уровень
надо это разделять а не мешать как остальные
как назвать этих ребят "Universe, Pi, Equ, W и HIT" ?
Zeit Raffer
@zraffer
Aug 05 2016 16:10
Примитивные типы
Namdak Tonpa
@5HT
Aug 05 2016 16:10
Fundamental Deduction Rules?
Zeit Raffer
@zraffer
Aug 05 2016 16:11
Typing
Namdak Tonpa
@5HT
Aug 05 2016 16:11
ну для record и data я так быстро не выпишу
Zeit Raffer
@zraffer
Aug 05 2016 16:12
Type judgement inference rules
Namdak Tonpa
@5HT
Aug 05 2016 16:43
ладно с HIT я конечно погорячился в общем случае но для транкейшина могу выписать и для сферы
:-)