не множество. объект категории. в данном случае - тип Хаск.

Про рерайт системы хз. Никогда не думал в этом направлении. Речь о равенстве между объектами в категории?

Равенства между стрелками в (1,1)-категориях. Если мы возьмём классическую категориальную семантику хаскеля, то мы объявляем типы объектами, а типизируемые термы -- стрелками. При этом мы должны наложить нормально реальную аппликацию и композицию со стрелками вида (()-> T). Нормально сделать это можно только в тотальном подмножестве языка

Вообще моноид в математическом определении - это множество с операцией и нулевым элементом.

Вы бы тогда начали с того что такое "в математическом". Используется категориальное основание для математики или математическое основание для ТК?

не множество. объект категории. в данном случае - тип Хаск.

Ну тогда дай определение свободного моноида в терминах теории категорий.

Ну тогда дай определение свободного моноида в терминах теории категорий.

выше выдержка из Awodey

Ну тогда дай определение свободного моноида в терминах теории категорий.

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

Равенства между стрелками в (1,1)-категориях. Если мы возьмём классическую категориальную семантику хаскеля, то мы объявляем типы объектами, а типизируемые термы -- стрелками. При этом мы должны наложить нормально реальную аппликацию и композицию со стрелками вида (()-> T). Нормально сделать это можно только в тотальном подмножестве языка

ну так то да, тут спорить не с чем

Вы тут случайно не в костюмах с бабочками сидите перед мониторами случайно?

откуда Вы узнали?

не знаю как вы, а я в футболке с двумя черепами

В хрустальном шаре рассмотрел.

Про рерайтинг системы кстати отличное замечание. Оно меня навело на мысль о том, что если на подобных размышлениях базировать реальные системы, то это конечно фейл. А если не базировать, то гипотетический Hask меня вполне устраивает.

Про рерайтинг системы кстати отличное замечание. Оно меня навело на мысль о том, что если на подобных размышлениях базировать реальные системы, то это конечно фейл. А если не базировать, то гипотетический Hask меня вполне устраивает.

На самом деле мы не можем только тьюринг-полные системы построить вокруг теор. ката. Если мы будем приближать систему тотальными подсистемами, то все свойства будут сохраняться

Равенства между стрелками в (1,1)-категориях. Если мы возьмём классическую категориальную семантику хаскеля, то мы объявляем типы объектами, а типизируемые термы -- стрелками. При этом мы должны наложить нормально реальную аппликацию и композицию со стрелками вида (()-> T). Нормально сделать это можно только в тотальном подмножестве языка

есть мнение, что самое интересное, сделать это для нетотальной части. чтобы реальные бесконечные списки описывались и вплоть до тьюринг полноты. но это сложнее. а без этого будет не Хаск, а какой-нибудь Идрис.

есть мнение, что самое интересное, сделать это для нетотальной части. чтобы реальные бесконечные списки описывались и вплоть до тьюринг полноты. но это сложнее. а без этого будет не Хаск, а какой-нибудь Идрис.

Можно попробовать рассматривать какие-нибудь (1,2)-категории, в которых порядок на стрелках будет доменом Скотта

Я какое-то время назад пытался решить эту проблему уже, но ни к чему не пришёл

Бывает порой грустно от того, что люди постоянно пытаются абстрагироваться от лямбда исчисления. На самом деле более восхитительного, красиво и самого по себе интересного исчисления люди, наверное, не придумывали. Заходишь порой в чатик по хаскелю и понимаешь, что люди настолько окунулись в категориальную семантику, что забывают о том, что далеко не для всех термов у нас бывает нормализация. Конечно когда мы работаем с каким-нибудь тотальным языком типа агды, мы можем забить на то, что "множество" термов типа на самом деле никакое не множество, подменив его нормальными формами. Но в том же хаскеле этого сделать нельзя. Во многом это связано с тем, что у лямбда исчисления нету внятного математического обобщения. Людям приятно работать со сферическими конями в вакууме, а не задумываться о стратегиях редукции и рерайт-правилах. Так что в рамках свободной игры ума попытался придумать обобщение понятия множества с "лямбда" семантикой. Наверняка кто-нибудь эту фиговину формулировал и возможно она даже очень скучная, потому что я не особо много её придумывал. Будем называть "лямбдоидом" множество L, функцию lambda: L->L, частичную функцию apply: L x L -> L и отношение порядка на нём (>), при чём: 1. Отношение порядка обладает свойством слияния: если множество минимальных элементов может иметь не более одного элемента // в лямбда исчислении у нас термы либо бесконечно редуцируют, либо сходятся в одной точке

Потому что не надо много уметь, чтобы критиковать, достаточно много знать... А вот умений чтобы что-то придумать крутое мне не хватает

Потому что не надо много уметь, чтобы критиковать, достаточно много знать... А вот умений чтобы что-то придумать крутое мне не хватает

я опять же извиняюсь, но не является ли данное сообщение именно попыткой покритиковать?

я опять же извиняюсь, но не является ли данное сообщение именно попыткой покритиковать?

Самого себя :)

а! круто!

Вы вот зря противопоставляете рерайт правила и категории. В классической работе Хагино вполне есть и правила перепиывани и даже абстрактная машина для вычисления термов из некоторой категории. Одно другому не мешает.

Вы вот зря противопоставляете рерайт правила и категории. В классической работе Хагино вполне есть и правила перепиывани и даже абстрактная машина для вычисления термов из некоторой категории. Одно другому не мешает.

Но там небось строгая нормализация на термах есть, а у нас же нету

да

Dmitry а когда у вас заседание комитета по докладам?

Крч, neil не сработал для документации. Stack не умеет загружать доки на hackage. В итоге нашел скрипт, который используя stack генерил архив доки и загружал ее.

я генерю доки и гружу скриптом после аплоада

на работе тут ворчат что доки немодные получаются, нелинкованые, но так они хотя бы есть

я это нейлом делаю

тогда линкованые

Neil не сработал, тк он использует cabal. А у меня в зависимостях есть пакет с гитхаба(пулл реквест)

https://hackage.haskell.org/package/inline-r

ну это проблемы индейцев

cabal sandbox init cabal get -s cabal install package

https://github.com/typeable/schematic/blob/master/release s/stack/cabal/g

и заработает

тьфу

`cabal get -s package

точнее s/cabal/stack/g

впрочем и без этого заработает, ведь cabal sdist/upload и так пашет

там с линками проблемы есть

если самому генерить, а у нейла этих проблем обычно нет

с линками нет проблем, т.к. нет линков

ссылки на типы из других пакетов работают нормально?

просто у меня раньше криво работали

не знаю, сейчас проверю

неа, кривые

🙁

в neil норм?

Я этот использовал

https://github.com/ekmett/lens/blob/master/scripts/hackage-docs.sh

@catamorphism вроде норм

вон я ссылку на inline-r дал

я вчера там нейлом генерил

нейл что-то хитрое делает, но я не разбирался подробно

хм, кликается

надо попробовать

а ни у кого в проекте с кучей пакетов стеку не стало голову сносить

меняешь что-нить в зависимости и он нифига пересобрать не может ругаясь на интерфейсы

stack clean не помогает?

помогает

это-то понятно

но это немного бесит

о да

про shadowed dependencies ругаться начал

активно

задолбал уже

во-во

пнул слоана в чятике если их ещё тикетами не завалили

я там отписывался кстати в тикет

но с тех пор это случилось еще 9000 раз

у меня сегодня это раз 15 было

Надо запомнить что можно слоана через тебя пинать.

да мы с ним пересекаемся в одном проекте

16 раз

Будешь вести лайв-трансляцию фейлов?

ну да, а то по флуду уже конкуренты появляются

а я наверное уже спрашивал, если у меня есть код всякие численные методы над Linear, то есть ли у меня шанс сделать кодогенерилку нахаляву

А что за Linear?

linear который

Так там всё на Traversable & friends