These are chat archives for groupoid/exe

14th
Feb 2016
Zeit Raffer
@zraffer
Feb 14 2016 06:42
это значит надо перекомпилировать Cat (в последней версии эта функция берет 6 универсумов, а тут я вижу 4)
  • возьми новую версию, я переименовал одну функцию в Setoid
Zeit Raffer
@zraffer
Feb 14 2016 08:39
TypeEqu пока заброшен, его вообще можно удалить
Namdak Tonpa
@5HT
Feb 14 2016 08:47
или как его нужно компилировать?
Zeit Raffer
@zraffer
Feb 14 2016 08:53
в нем просто были эксперименты, сейчас он нигде не используется
но в перспективе это все будет нужно, когда дойду до равенства в универсуме
Namdak Tonpa
@5HT
Feb 14 2016 09:20
     E := ∅ | E data L : A := F
            | E record L : A [ extend P ] := F
            | E let F in O
            | E case O [ | I O -> O ]
            | E receive O [ | I O -> O ]
            | E spawn O O raise L := O
            | E send O to O
перенес SetoidLim и TypeEqu в другой каталог все собирается!
Namdak Tonpa
@5HT
Feb 14 2016 09:26
вприниципе этого синтаксиса достаточно чтобы моделировать эффекты привязанные к процессам, и у процессов три аксиомы send, receive (которая точностью повторяет case, только блокирующая) и spawn (где указывается список эффектов которые может райзить или наборот всасывать процесс), сами эффекты прдеставлены просто как хендлер с двумя функциями — которая бросает в среду что-то и которая всасывает со среды что-то (как random).
  record Eff: * := (in: exe) (out: exe)
  record Process: (Sigma: sum) → (X: record) → * :=
         (effect: list Eff)
         (action: Sigma → X → X)
сам процесс -- это полугруппа активностей (сигнатура action).
т.е. это функция, которая реагирует на какой-то протокол сумму и крутит стейт моноидальный, который должен быть рекордом с полями аксессорами
Т.е. эффект State как бы явно в сигнатуре присутствует, поэтому хедлера отдельного не нужно
стандартные хендлеры эффектов — это Random, IO, Exception, Comm (send, receive).
Namdak Tonpa
@5HT
Feb 14 2016 09:31
типа у процесса есть список эффект хендлеров на которые он реагирует, и функция с сигнатурой полугруппы
Zeit Raffer
@zraffer
Feb 14 2016 09:32
угу
Namdak Tonpa
@5HT
Feb 14 2016 09:32
только надо чтобы эффекты хендлеры наследовались от Eff а не как Data Record или Case Receive
типа record IO extend Eff := (), record Random extend Eff := ()
ну и там дополнительное что-то могут таскать если хотят, тогда они сразу в стейт эффекты превращаются
Zeit Raffer
@zraffer
Feb 14 2016 09:34
а реализация встроенных эффектов непосредственно в бекенде, или как-то в прелюдию на ЕХЕ засунем?
Namdak Tonpa
@5HT
Feb 14 2016 09:34
а так это чистее чистоты и без богомерзких монадных трансформеров
в бекенде
эффекты только в бекенде уже подставляются
у нас же язык чистее чистоты :-) низя )
ну как, шо скажут благородные доны о такой архитектуре?
Zeit Raffer
@zraffer
Feb 14 2016 09:36
а шо скажут. если не всплывет препятствий, то все прекрасно. ты с эффеками что-то писал? я лично еще нет, только монадами пользовался.
но красиво, конечно
эффекты это отдельные категории
Namdak Tonpa
@5HT
Feb 14 2016 09:38
монада будет для эффектов, но одна на весь язык и систему эффектов!
Zeit Raffer
@zraffer
Feb 14 2016 09:38
пора начинать писать тьюториал по ЕХЕ )
ну ты как бы начал
синтаксис
Namdak Tonpa
@5HT
Feb 14 2016 09:39
я хочу написать описание каждого типа
по три предложения
типа как документацию по системе типов начать
и чтобы оно все выглядело в стиле рассказа
как делать Do It Youself Type Theory
с мотивацией
почему мы именно так сделали по каждому конкретному типу
и ссылки на плечи титанов
хотелось бы максимально академически
и проникающе :-)
Zeit Raffer
@zraffer
Feb 14 2016 09:40
да, у нас такая "теория типов, созданная в гараже" )
Namdak Tonpa
@5HT
Feb 14 2016 09:40
и в тоже время просто чтобы было
чтобы когда чувак который пишет на Elixir смог понять что написано :-)
хотя это опционально
Zeit Raffer
@zraffer
Feb 14 2016 09:41
ага, вон Леан периодически не может понять, что я пишу ))
Namdak Tonpa
@5HT
Feb 14 2016 09:41
у нас тут групоиды, так шо, сорри, придется в космический куб выходить _
Zeit Raffer
@zraffer
Feb 14 2016 09:41
ну зачем пугать людей страшными словами ))
Namdak Tonpa
@5HT
Feb 14 2016 09:41
вот как в Агде, он в своем дисере на каждый тип отдельную главу сделал
вот я бы так хотел, как у меня List полностью до потрохов расписан
хочу чтобы все типы на этой странице так были расписаны ))
в самом главном TeX документе )
Zeit Raffer
@zraffer
Feb 14 2016 09:42
ну диссер пишут несколько лет и очень основтельно (кто как, впрочем)
Namdak Tonpa
@5HT
Feb 14 2016 09:42
а на сайтике просто типа реклама
буклет брошюра
cheat sheat
так я поэтому и на сайтик и переключился
что в документе можно утонуть
Zeit Raffer
@zraffer
Feb 14 2016 09:43
"заходите к нам, у нас бесконечность группоидов и космо-куб!"
Namdak Tonpa
@5HT
Feb 14 2016 09:48
ну а шо, если люди хотят типов
мы их завалим типами )
но надо чтобы просто выглядело
Namdak Tonpa
@5HT
Feb 14 2016 09:54
вот надо три простых предложения про группоид и сетоид написать :-)
в секции Logic
чтобы с намеком на космо-куб и HoTT
типа "вот это рекорд используется для ризонинга по гладким многообразиям..."
является частью геометрической логики
читайте космо-куб и просвещайтесь :-)
Моноиды -- у нас это KVS цепочки
Полугруппы -- это Эрланг процессы
А моноиды и Категории это ж одно и тоже с точки зрения ризонинга?
рекорды же одни и теже
Namdak Tonpa
@5HT
Feb 14 2016 10:00
язык кстати у нас супергибкий, я думаю макросистему любую можно написать
можно написать и Lisp и ML и Scala на этом O
благодаря этому правилу O O
наше E это и есть Macro наверно которое в Lean
Zeit Raffer
@zraffer
Feb 14 2016 10:50
"моноиды и Категории это ж одно и тоже с точки зрения ризонинга?" - с категориями нужен вывод типа объектов для операций (либо постоянное их явное указание), так что ризонинг чуточку сложнее
"три простых предложения про группоид и сетоид" - сюда или сразу в какой файл?
Zeit Raffer
@zraffer
Feb 14 2016 12:46
СЕТОИД - это тип вместе с равенством. Теория типов имеет свой тип равенства, который можно рассматривать как простейший нетривиальный зависимый тип, однако поведение этого вида равенства зависит от дополнительных аксиом, которых в минимальной теории типов может и не быть. Чтобы иметь точно определенное равенство, с которым мы, к тому же, можем делать все, что нам захочется, используют СЕТОИДЫ. Очень удобно, что категорные конструкции на сетоидах выдают нам готовое равенство на всех (ко)индуктивных типах, не зависящее от свойств подлежащей теории типов.
Zeit Raffer
@zraffer
Feb 14 2016 12:51
ГРУППОИД - многомерное обобщение сетоидов, в котором есть равенства между равенствами и операции между ними. Понятие ГРУППОИДА введено в алгебраической топологии для нужд теории гомотопий и в идеале может заменять понятие топологического пространства, поскольку охватывает все существенные с точки зрения гомотопий его свойства. В рамках гомотопической теории типов HoTT было описано (в некотором смысле максимальное) равенство на универсуме всех типов, при одновременном усложнении внутреннего устройства отдельных типов, которые стали похожи на ГРУППОИДЫ, в результате чего теория типов оказалась применима к выражению утверждений о гомотопиях.
Namdak Tonpa
@5HT
Feb 14 2016 12:51
отлично, на английский сам попытаюсь )
Namdak Tonpa
@5HT
Feb 14 2016 13:05
Setoid in essence is a type within an equality. Type theory has its own equality type,
which could be treated as simplest non-trivial dependent type, however the behavior of
this kind of equality is defined with additional axioms, that may be optional in minimal type theory. The neat thing about Setoid is that categorical constructions on setoids give us equality on all (Co)inductive types, which is not dependent on properties of underlying type theory.
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:07
*within -> with
the/a simplest
просто реально якби я не прочитав на днях, що таке сетоїд, то подумав би, що є якась equality, всередині якої знаходиться тип
Namdak Tonpa
@5HT
Feb 14 2016 13:10
ну є і тип Eq, він же використовується в сетоїді
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:11
а тут виходить навпаки, ніби тип всередині Eq
може, просто не так зрозумів (вікіпедійне означення, що equipped with an equality operation, приблизно)
Namdak Tonpa
@5HT
Feb 14 2016 13:12
ну на сторінці exe.htm все дуже конкретно
і конкретний тип Eq і Setoid досить формально визначені
якшо є питання то їх тут можно прояснити
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:14
Ох, та і голі визначення виглядають чисто, але страшно
Якби був якийсь пояснювальний текст
Namdak Tonpa
@5HT
Feb 14 2016 13:15
ну от ти його тільки шо на двох мовах прочитав )
раз нічо ніпанятна то тра міняти текст )
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:16
А, так це якраз пояснення означень? Тоді норм
Namdak Tonpa
@5HT
Feb 14 2016 13:16
так
просто List можно пояснити на формулах в трьох реченнях
але щоб Setoid пояснювати то треба всю прелюдію категорну пояснювати
тому тут дещо спрощено, без формулювання теорем навіть
Namdak Tonpa
@5HT
Feb 14 2016 13:21
може більш формально в термінах ініціального об’єкту категорії пучків F,G-діалгебр? )
це треба Якобса перелистати і виписати просто
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:22
Ой, не лякайте категорну дєрєвєнщіну
мені уже страшно
Взагалі, чи є смисл вчити абстрактну алгебру перед теоркатом?
Namdak Tonpa
@5HT
Feb 14 2016 13:24
ну абстрактну алгебру звичайно краще вже проходити в інституті, там же все просто
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:24
А то якось теоркат зразу це повний хардкор, та і почуватись неграмотним у гратках-полях-кільцях не хочеться
Namdak Tonpa
@5HT
Feb 14 2016 13:25
тебе ж ніхто не заставляє шукати ізоморфізми у вищих топологіях
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:25
на магістра піти довчитись, чи що
Namdak Tonpa
@5HT
Feb 14 2016 13:25
теоркат нам дає змогу довести коректність кодування нашого яке ми будем робити для індуктивних типів
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:26
а то так багато всякого смачного
Що таке «індуктивний тип»?
Namdak Tonpa
@5HT
Feb 14 2016 13:27
з синтаксичної точки зору це
  record Data: * :=
         (name: string)
         (base: Om)
         (body: list (prod string Om))
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:27
Мені вони синтаксично схожі на GADT
Namdak Tonpa
@5HT
Feb 14 2016 13:27
це генералізація GADT
ADT -> GADT -> Inductive Constructions
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:28
name/base/body — це конструктори? Чи поля?
Namdak Tonpa
@5HT
Feb 14 2016 13:28
це частини синтаксичної конструкціі
    data vector: (A:*) → nat → * :=
         (nil: ()vector A zero)
         (cons: (n: nat) → Avector A n → vector A (succ n))
(A:*) → nat → * — це база, [nil, cons] — це конструктори, тобто тіло
vector — це назва типу
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:30
про data і схожі конструкції у мене є уявлення, але record уже мало зрозумілий, чи це просто структура із полями, чи в цьому є якийсь типовий смисл
наприклад, якщо б це був псевдохаскельний record, то name : Data -> string
чи це синтаксичний цукор такий, щоб не писати Data перед кожним типом?
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:36
Взагалі, я голосую за Concise Introduction to Exe for mere haskellers
Dmytro Sirenko
@EarlGray
Feb 14 2016 13:43
І ще в мене одне нескромне запитання: у файлів із кодом на Exe буде розширення .exe ? :)
так
рекорд - так, структура з полями; с категорної точки зору операціі проекції (де(кон)структори) на поля дуальні до конструкторів.
Namdak Tonpa
@5HT
Feb 14 2016 13:54
синтаксично Data та Record у нас співпадаюсь майже.
технічно
     record case: * := (cond: bool) (false: om) (true: om)
     data case: * := (intro: bool → om → om → case)
рекорд -- це то саме шо індуктивний тип з одним доданком
ці два визначення співпадають з точністю до лямбда асемблера
рекорди (коіндуктивні) -- це рекурсвні добутки, індуктивні -- це рекурсивні залежні суми
разом вони формують клас поліноміальних функторів
теорія яка описана в математичній моделі Exe, бере ліміти в категоріях таких функторів
тобто кожен індуктивний або коіндуктивний тип (Coq, Agda, Exe, F*, Idris, Lean) -- це ініціальний або термінальний об’єкт в категорії пучків F,G-діалгебр (для залежного варіанту) або F-(ко)алгебр (без залежних типів).
Namdak Tonpa
@5HT
Feb 14 2016 14:15
Groupoid is an multidimensional generalization of Setoid type, which has equalities on equalities and operations between them. Gropoid was introduced in algebraїс topology for the purposes of homotopy theory and has potential to replace the notion of topological space, since groupoid covers all the properties of topological space from the homotopy perspective. The ultimate equality on universum of all types was shown in HoTT setting, thus type theory became successful for reasoning about homotopies.
Zeit Raffer
@zraffer
Feb 14 2016 14:21
пиши в файл!
Namdak Tonpa
@5HT
Feb 14 2016 14:28
текст на странице уже в вебе
Namdak Tonpa
@5HT
Feb 14 2016 15:59
в FPGA странице я опишу просто что мы что-то смотрели что-то нет, если у вас есть идеи или варианты сотрудничества по организации работы FPGA компиляции пишите нам
а во втором параграфе про Erlang опишу что мол нас устраивает бекенд на эрланге поэтому мы его делаем, если вас интересуют бекенды в другие нетипизированные лямбды (или даже типизированные, почему нет) тоже пишите.
или написать что у нас приоритетное FPGA ?
надо писать как есть :-)
но так чтобы оно не прогнило когда у нас все будет :-)
Zeit Raffer
@zraffer
Feb 14 2016 16:11
ну так и писать как есть: ФПЖА планируется сделать
там есть про минимализм? что вот, если мы убираем ОС и получаем более компактную систему с Эрлангом; а если мы выкинем CISC процессор - гипервизор - и даже Эрланг, то вообще полная Нирвана будет.
Namdak Tonpa
@5HT
Feb 14 2016 16:13
да не групоид сайт я подразумеваю что его читают боги
там этого всего очевидно писать не надо, только суть
хотите полность читайте документ на украинском или английском
Zeit Raffer
@zraffer
Feb 14 2016 16:13
ну или документ
Namdak Tonpa
@5HT
Feb 14 2016 16:13
там будет история развития юникернелов
и наше видение
Zeit Raffer
@zraffer
Feb 14 2016 16:14
кстати, я написал пост про потенциального брадобрея, завтра на свежую голову надо будет реализовать
Namdak Tonpa
@5HT
Feb 14 2016 16:16
я думаю будет решение, если найдутся брадобреи
Zeit Raffer
@zraffer
Feb 14 2016 16:16
или будет решение, или выкинем непредикативный универсум
заодно логотипчик сайнерси обновил )
теперь надо набросать крупными мазками что в INTRO для богов написать :-)
Zeit Raffer
@zraffer
Feb 14 2016 16:26
кто такие боги? )
Namdak Tonpa
@5HT
Feb 14 2016 16:27
ну например сам Лямбдагарбха чтобы если открыл страницу то не стыдно были читать ему )
т.е. без этого технарьства а что-то про язык пространства задвинуть
шизоидную какую-то составляющую добавить )
Zeit Raffer
@zraffer
Feb 14 2016 16:28
"понимается как зародыш состояния Будды в каждом живом существе" - ясТно
Namdak Tonpa
@5HT
Feb 14 2016 16:29
это Димон придумал http://thedeemon.livejournal.com/67223.html
грабха да — это семя бодхичитты
просветленная лямбда типа переводится :-)
может заменить "Provable Erlang Applications" на что-то более броское
Namdak Tonpa
@5HT
Feb 14 2016 16:34
типа "Natural Encoding of the Inner Space" ?
Zeit Raffer
@zraffer
Feb 14 2016 16:35
тебе для богов или все-таки для программеров? ) чтобы техдиректор приватбанка тоже что-то понял, а не только Хенк Барендреггт
Namdak Tonpa
@5HT
Feb 14 2016 16:35
нет, Только Хенка!
Zeit Raffer
@zraffer
Feb 14 2016 16:35
кстати "2016 © Groupoid Infinity, Inc." что уже есть корпорация? ;)
Namdak Tonpa
@5HT
Feb 14 2016 16:35
к директору Приватбанка у меня другие презентации
это к @doxtop он у нас регистрирует корпорации
Доктор в какой стране мы в этом году открываем корпорации?
ну вообще в INTRO я думаю надо упор на Natural Encoding сделать
а это только ты хорошо и смачно можешь описать )
надо просто отпустить мысли
Zeit Raffer
@zraffer
Feb 14 2016 16:38
ах, мы это назвали "Natural Encoding" я не сразу вспомнил
давай я разберусь со свеженайденным брадобреем, потому что возможно придется что-то модифицировать
еще скажут что мы за сексизм ))) мол все вокруг пидарасы, а у нас одних натурал инкодинг )
Namdak Tonpa
@5HT
Feb 14 2016 16:41
все нормально, нас крышует Лямбдагарбха
ну тогда сразу Categorical Encoding
или вот так "Natural Encoding with proved categorical semantic"
Zeit Raffer
@zraffer
Feb 14 2016 16:42
надо подумать, Натурал мне на самом деле нравится, можно еще Limit Encoding
предельная кодировка )
или вот есть лемма Ламбека - про то, что инициальная алгебра является неподвижной точкой функтора. можно криптографически назвать кодировка Ламбека, чтобы никто не догадался (так принято)
Namdak Tonpa
@5HT
Feb 14 2016 16:44
как скажешь!
Lambek Encoding ок
Zeit Raffer
@zraffer
Feb 14 2016 16:44
я сейчас думаю только про брадобрея
Namdak Tonpa
@5HT
Feb 14 2016 16:44
ок удаляюсь
Andrii Zadorozhnii
@doxtop
Feb 14 2016 23:39
ох вы тут пишете буквы гг :) корпорации наверное в юсе нужно делать, надо скатать посмотреть. ну или у фашистов гезельшафт какой-то, тоже нужно скатать посмотреть :)