These are chat archives for groupoid/exe

3rd
Mar 2016
Zeit Raffer
@zraffer
Mar 03 2016 12:56
имел разговор с жж-юзером pbl, который предлагает строить кодировку на основе параморфизмов, а не катаморфизмов, якобы она будет иметь более эффективные в операциональном плане рекурсоры. я помню @nponeccop высказывался тут уже про неэффективность рекурсоров. надо обдумать.
Zeit Raffer
@zraffer
Mar 03 2016 13:33
Zeit Raffer
@zraffer
Mar 03 2016 14:01
вобщем, надо проверить, что параморфизмы можно выгоднее использовать при паттерн метчинге, по сравнению с катаморфизмами (или нет...).
кстати собеседник продвинутый :)
https://github.com/pbl64k/icfpc2014
Namdak Tonpa
@5HT
Mar 03 2016 14:26
Приглашай Pavel Lepin в команду )
Namdak Tonpa
@5HT
Mar 03 2016 14:39
я сктати не совсем понимаю у нас же есть элиминаторы для head и tail
непонимаю зачем там Fix у него на гисте
Namdak Tonpa
@5HT
Mar 03 2016 14:49
вот же в морте есть head и tail, тоже на Maybe (закомитил только что в Om)
что он хочет показать?
что если добавиьт Fix то термы становятся короче?
это же очевидно
Namdak Tonpa
@5HT
Mar 03 2016 14:57
у меня вот какая идея возникла
хочется чтобы программы на EXE можно было использовать как скрипты для шелла
Т.е. как SQL, чтобы load и compile работали с одним и тем же исходником
но для этого придется вводить слова терминаторы
на которые будет реагировать шелл
в эрланге это точка
или end
типа вот ты пишешь программу в шеле
серией вводов строк
и шеллу нада узнать когда закончился ввод терма
можно типа в begin end
Dmytro Sirenko
@EarlGray
Mar 03 2016 15:00
можна порожній рядок
Namdak Tonpa
@5HT
Mar 03 2016 15:00
это типа скобок ( ) но на уровне exe
  begin record pair: * 
     := (a: *) (b: *) end
и пошла компиляция сразу
если в шелле эти две строки ввел
типа как begin transaction
ну или можешь ставить begin end в начале и в конце файла
тогда будет пофайловая компиляция
Zeit Raffer
@zraffer
Mar 03 2016 15:03
все мы договорились - параморфизмы нужны для компиляции паттернметчинга вида list@(x:xs), что дает нам тождественную функцию (например) за константное время. ура!
Dmytro Sirenko
@EarlGray
Mar 03 2016 15:03
begin Module
end
Namdak Tonpa
@5HT
Mar 03 2016 15:03
вот без Module пожалуйста
имя файла это модуль
Zeit Raffer
@zraffer
Mar 03 2016 15:04
объясняю зачем - чтобы тождественная функция (и подобные случаи) быстро считались
Namdak Tonpa
@5HT
Mar 03 2016 15:04
хотя нет не так
имя типа это модуль эрланга
а в exe никаких модулей не нужно
есть система типов
@zraffer так мы же уже упражнялись в паттерн мачинге
и умножали наш тип на список деконструктуров.
я еще тогда сказал что нас ничего не оставит
что, таки пришли параморфизмы и остановили?
@EarlGray record это и есть модуль
то что напридумывали с namespases и modules,которые существуют отдельно от рекордов
это все ересь имхо
вот в эрланге офигенно нет никаких неймспейсов
делай в имени типа неймспейсы
через _
Dmytro Sirenko
@EarlGray
Mar 03 2016 15:08
а module:func() це що? Це все не один же атом?
Zeit Raffer
@zraffer
Mar 03 2016 15:09
параморфизмы ничего не остановят. они просто оптимизируют ПМ.
Namdak Tonpa
@5HT
Mar 03 2016 15:09
module:func — це record.field
як в ООП мовах
Zeit Raffer
@zraffer
Mar 03 2016 15:10
хотя ценой, конечно, усложнения кодировки. надо будет решить. стоит ли оно того.
Namdak Tonpa
@5HT
Mar 03 2016 15:10
надо будем мерять
пока не отвлекамся
делаем как договорились, будут немного конские элиминаторы для ПМ потом поправим, померяем, сменим кодировку если шо
нет других модулей кроме рекорда, и он основа всех слагаемых индуктивных типов!
Zeit Raffer
@zraffer
Mar 03 2016 15:12
да нормально все, оно более-менее ложится в общую картину, как я представляю все эти инициальные алгебры. напишем прототип, тогда будем тестировать.
Namdak Tonpa
@5HT
Mar 03 2016 15:16
після його компіляції будуть створені {sum,unit,prod,empty,sigma}.beam
а з ім’ям cartesian не буде створено нічого взагалі
тільки атрибут такий буде в beam файлі і все
Namdak Tonpa
@5HT
Mar 03 2016 15:27
так шо как вам идея такого шелла
типа begin end только для шелла
а в файлах это можно не использовать
так как файл по умолчанию при загрузке будет обрамлятся в begin end
и даваться на вход репл-компилятору
Zeit Raffer
@zraffer
Mar 03 2016 15:28
а почему не точку? как в Эрланге. не ложится на синтаксис?
Namdak Tonpa
@5HT
Mar 03 2016 15:28
ну да, нет у нас нигде точки
a begin end кстати тоже в эрланг стиле
это его ключевые слова
Zeit Raffer
@zraffer
Mar 03 2016 15:28
ну точка была бы короче
Namdak Tonpa
@5HT
Mar 03 2016 15:29
точка это только вконце монады эрланговой
Zeit Raffer
@zraffer
Mar 03 2016 15:29
о это для инженеров описание. "а в конце монады у нас точка" )))
Namdak Tonpa
@5HT
Mar 03 2016 15:30
ну типа просто если точку встретил то все что до этого было не скомпилиным — скомпилировать?
Zeit Raffer
@zraffer
Mar 03 2016 15:30
ну да
Namdak Tonpa
@5HT
Mar 03 2016 15:30
придется тогда различать точки в record.field
Zeit Raffer
@zraffer
Mar 03 2016 15:31
нехорошо
Namdak Tonpa
@5HT
Mar 03 2016 15:31
прими begin end
прими дух паскаля и ады
:-)
Zeit Raffer
@zraffer
Mar 03 2016 15:31
дух си призывает фигурные скобочки
Namdak Tonpa
@5HT
Mar 03 2016 15:36
я вообще подумал что нам надо атомы как в elixir и clojure
:atom
возможно do end для монад
в этом ключе begin end как операторные скобки выглядит логичным
главное что хочется, чтобы поток команд в шеле был неотличим от лоада файла
чтобы файлы не обладали никакими уникальными свойствами, чего нельзя сделать в репле языка
там в Эликсире просто неплохие биндинги на низкоуровневый эрланг написали
это все можно просто ихние классы на наши рекорды поменять и все
так шо тут тоже есть обширное пространство для плагиата
nponeccop
@nponeccop
Mar 03 2016 16:39
@zraffer ну, для параморфизмов нужнен набор программ чтобы посмотрет как что выражается. Я подозреваю просто, что некоторые штуки плохо выражаются через катаморфизмы. А параморфизмы шире применимы. Т.е. катаморфизм тривиальный частный случай параморфизма. А если параморфизм выражать через катаморфизм получится много мороки.
Zeit Raffer
@zraffer
Mar 03 2016 16:40
ну да, вот id или tail для списков выражаются просто на бумаге, но с линейной вычислительной сложностью
параморфизмы эту ситуацию спасают
Namdak Tonpa
@5HT
Mar 03 2016 16:42
так а что для этого нада у нас изменить?
кодировку?
Zeit Raffer
@zraffer
Mar 03 2016 16:42
ага
чуток усложнить
Namdak Tonpa
@5HT
Mar 03 2016 16:42
увесистее станет? это типа Скотта кодировка получится с зав типами?
Zeit Raffer
@zraffer
Mar 03 2016 16:42
ага
Namdak Tonpa
@5HT
Mar 03 2016 16:42
ясно
ну в хаскеле вроде скотта
Zeit Raffer
@zraffer
Mar 03 2016 16:43
ну оригинальный Скотт же безтиповый
Namdak Tonpa
@5HT
Mar 03 2016 16:43
ну черч тоже оригинальный безтиповой
nponeccop
@nponeccop
Mar 03 2016 16:43
а Fix на уровне типов парадоксален?
Namdak Tonpa
@5HT
Mar 03 2016 16:43
бесконечный ризонинг аксиом
Zeit Raffer
@zraffer
Mar 03 2016 16:43
вместо Fix у нас инициальная алгебра
Namdak Tonpa
@5HT
Mar 03 2016 16:43
типа чтобы применить аксиому нужно бесконечную дедукцию совершить
если такое допустить то не парадоксален )
Zeit Raffer
@zraffer
Mar 03 2016 16:44
которая является неподвижной точкой согласно лемме Ламбека
Namdak Tonpa
@5HT
Mar 03 2016 16:44
у нас такого нельзя
Zeit Raffer
@zraffer
Mar 03 2016 16:44
у нас и без этого хорошо
Namdak Tonpa
@5HT
Mar 03 2016 16:44
в духе конструктивизма у нас идет все
nponeccop
@nponeccop
Mar 03 2016 18:21

Я почитал тред http://ivan-gandhi.livejournal.com/3512090.html?thread=57664794#t57664794 про параморфизмы. Суть такова, что там ещё копать и копать, никаких очевидных улучшений я не вижу. Улучшения будут в call by name, т.е. в ленивом случае. А у нас строгий. И представление типов в виде параморфизмов проблематично, т.к. требует рекурсии уровня типов. Т.е. это тема отдельного исследования.

Короче, headMaybe :: [a] -> Maybe a вы напишете только O(N), что с ката- что с параморфизмами.

Zeit Raffer
@zraffer
Mar 03 2016 18:24
Спокойно! Рекурсия уровня типов не надо, есть неподвижная точка функтора, которая считается как инициальная алгебра, это у нас основной инструмент. Это дает эквивалент Fix без ужасов общерекурсивности. Ленивость реализуется локально заворачиванием ()->T тех аргументов, где это надо. Все реализуемо. Единственно, сколько это усложнение будет стоить.
nponeccop
@nponeccop
Mar 03 2016 18:29
Ну это надо реализовать хотя бы на Lean. В общем случае реализация CBN на CBV даёт ужасы CPS.
Если все согласны, я напишу ишшуй что надо proof of concept headMaybe чтобы увидеть, насколько много надо писать для реалистичного control flow.
Zeit Raffer
@zraffer
Mar 03 2016 18:35
хм. а пример ужасов? на Скале все заворачивают (()=>T) аргумент в лямбду и оно прекрасно работает, даже "невозможная монада" http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/comment-page-1/
nponeccop
@nponeccop
Mar 03 2016 18:43

на скале никто в здравом уме не заворачивает, и на ML тоже. Как раз потому что получается каша. А в качестве интеллектуального упражнения - да.

Но у нас хуже: само понятие катаморфизма не предусматривает механизма останова. Т.е. не понадобится ли нам отдельный ленивый катаморфизм, который всё поломает?

Т.е. позволяет ли кодировка Берардуччи выразить O(1) headMaybe?
Namdak Tonpa
@5HT
Mar 03 2016 18:44
нет
> om:a("#List/head").
и длинная колбаса на экран
Maybe присутсвует
nponeccop
@nponeccop
Mar 03 2016 18:47
Pечь же не о невыразимости как таковой, а о невыразимости варианта с O(1).
Заворачивания в () там нет, короче.
Namdak Tonpa
@5HT
Mar 03 2016 18:48
ну так а если прямо в сигнатуры конструкторов писать () -> T
то что не будет ленивости?
оно же скомпилирует
nponeccop
@nponeccop
Mar 03 2016 18:49
напишите и убедитесь в отсутствии каши
если авторы не могут написать headMaybe из-за того, что это требует огромной работы, что говорить о хипсторах :)
не говоря уже о детях и милиционерах
хотя бы на Lean
Namdak Tonpa
@5HT
Mar 03 2016 18:50
{{"λ",{a,0}},
 {{star,1},
  {{"λ",{xs,0}},
   {{app,{{{"λ",{a,0}},
           {{star,1},
            {{"∀",{'List',0}},
             {{star,1},
              {{"∀",{'Cons',0}},
               {{{"∀",{head,0}},
                 {{var,{a,0}},
                  {{"∀",{tail,0}},{{var,{'List',0}},{var,{'List',0}}}}}},
                {{"∀",{'Nil',0}},{{var,{'List',0}},{var,{'List',0}}}}}}}}}},
          {var,{a,0}}}},
    {app,{{app,{{app,{{var,{xs,0}},
                      {app,{{{"λ",{a,0}},
                             {{star,1},
                              {{"∀",{'Maybe',0}},
                               {{star,1},
                                {{"∀",{'Just',0}},
                                 {{{"∀",{'_Just',0}},{{var,{a,0}},{var,{'Maybe',0}}}},
                                  {{"∀",{'Nothing',0}},
                                   {{var,{'Maybe',0}},{var,{'Maybe',0}}}}}}}}}},
                            {var,{a,0}}}}}},
                {{"λ",{x,0}},
                 {{var,{a,0}},
                  {{"λ",{'P',0}},
                   {{app,{{{"λ",{a,0}},
                           {{star,1},
                            {{"∀",{'Maybe',0}},
                             {{star,1},
                              {{"∀",{'Just',0}},
                               {{{"∀",{'_Just',0}},{{var,{a,0}},{var,{'Maybe',0}}}},
                                {{"∀",{'Nothing',0}},
                                 {{var,{'Maybe',0}},{var,{'Maybe',0}}}}}}}}}},
                          {var,{a,0}}}},
                    {app,{{app,{{{"λ",{a,0}},
                                 {{star,1},
                                  {{"λ",{'_Just',0}},
                                   {{var,{a,0}},
                                    {{"λ",{'Maybe',0}},
                                     {{star,1},
                                      {{"λ",{'Just',0}},
                                       {{{"∀",{'_Just',0}},{{var,{a,0}},{var,{'Maybe',0}}}},
                                        {{"λ",{'Nothing',0}},
                                         {{var,{'Maybe',0}},
                                          {app,{{var,{'Just',0}},{var,{'_Just',0}}}}}}}}}}}}}},
                                {var,{a,0}}}},
                          {var,{x,0}}}}}}}}}},
          {app,{{{"λ",{a,0}},
                 {{star,1},
                  {{"λ",{'Maybe',0}},
                   {{star,1},
                    {{"λ",{'Just',0}},
                     {{{"∀",{'_Just',0}},{{var,{a,0}},{var,{'Maybe',0}}}},
                      {{"λ",{'Nothing',0}},
                       {{var,{'Maybe',0}},{var,{'Nothing',0}}}}}}}}}},
                {var,{a,0}}}}}}}}}}
вот тебе
я ж говорю нажми в шеле om:
nponeccop
@nponeccop
Mar 03 2016 18:51
(но разумеется с нашей кодировкой)
Namdak Tonpa
@5HT
Mar 03 2016 18:51
 > om:a("#List/head").
это наша кодировка
nponeccop
@nponeccop
Mar 03 2016 18:52
ты мне headMaybe останавливающийся покажи, с кодировкой
"ваша кодировка" просматривает весь список, не?
Namdak Tonpa
@5HT
Mar 03 2016 18:53
нет, только для tail
Zeit Raffer
@zraffer
Mar 03 2016 18:53
что, есть сомнения в head? это мне начинает нравиться
Namdak Tonpa
@5HT
Mar 03 2016 18:54
да head работает, вы че )
nponeccop
@nponeccop
Mar 03 2016 18:54
@zraffer есть сомнения даже в isEmpty :: [a] -> Bool
@5HT он работает, но за O(N)
Zeit Raffer
@zraffer
Mar 03 2016 18:55
это прекрасно. я завтра на свежую голову проверю.
Namdak Tonpa
@5HT
Mar 03 2016 18:56
так у нас же есть для паттер мачинга штуки которые экстрактят константы
я думал они же могу заэкстрактить первый параметр конса
 io:format("Head of [2,1]: ~p~n", 
              [ap(ap(cons(),[2,ap(cons(),[1,nil()])]),
              [fun (H) -> fun (T) -> {head,H} end end, nil])]),
nponeccop
@nponeccop
Mar 03 2016 18:59
@zraffer я тут придумал минимальный пример - Bool напиши правильный. У которого элиминатор обе ветки не считает
Namdak Tonpa
@5HT
Mar 03 2016 18:59
> ch:main().
Head of [2,1]: {head,2}
Zeit Raffer
@zraffer
Mar 03 2016 18:59
@5HT оно считает, вопрос в том, какая сложность, т.е. сколько редукций происходит
Namdak Tonpa
@5HT
Mar 03 2016 19:00
ну счас посчитаю
nponeccop
@nponeccop
Mar 03 2016 19:00
хотя тут можно ленивость сверху элиминатора накрутить
не годится
Namdak Tonpa
@5HT
Mar 03 2016 19:01
но это не настоящий хед это по сути модифицированный экстрактор для ПМ
для [] он будет выдавать nil — имя конутркутора пустого списка
можно там ему Maybe подсунуть
и будет headMaybe как ты хочешь
Nothing в nil ветке возвращать
а в cons ветке Just
и выбросить нахуй этот List/head
:-)
счас я дам трейс инструкций
This message was deleted
This message was deleted
This message was deleted
Namdak Tonpa
@5HT
Mar 03 2016 19:08
io:format("Head of ~p: ~p~n", [unlist(L12),
  ap(L12,[fun (H) -> io:format("H~n"),fun (T) -> io:format("T~n"), {head,H} end end, nil])]),
H
H
H
H
H
H
H
T
T
T
T
T
T
T
Head of [10,2,3,4,5,6,7]: {head,10}
так и есть 7 раз
но моя имплементация в разы короче, наверно из-за того что полностью нетипизированная