Это полностью совместимо со спекой reactivex.io?

Там вроде просто обертка, не все операторы похоже

вообще их две)

В пурсы очень простой интероп

ну в пурсе нет смысла в rxjs, там свои стримы есть

И полуколец

Соответственно для них определена операция сложения

Числа входят в категорию колец

Я просто в прелюдии Integer не нашел)

Встроенны

Как и Bool

А Int как раз вроде один из немногих определённых в языке

числа это даже поле уже

И массив

Ну там и Field есть

Числа входят в категорию колец

не все сеты чисел создают кольцо, да?

числа это даже поле уже

В данном контексте важно именно то что они — кольцо

не все сеты чисел создают кольцо, да?

Ну я вкратце, да

то есть чтобы было кольцо нужно чтобы каждому числу из сета a было число -a?

Да, поэтому натуральные числа — полукольцо, а целые — кольцо

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

В хаскелле Num тупой

В плане?

Ну про кольца эти в прелюдии

В хаскелле этого нет

Линейная логика (Введение) (полная Markdown-версия поста: http://bit.ly/2ydfn1w) Если классическая логика оперирует утверждениями, то линейную логику удобно описывать через доступность неких ресурсов. Представим следующее логическое утверждение: если есть кружка кофе, её можно выпить. Чуть более формально это можно записать следующим образом: P = have coffee Q = drink coffee P ⊢ Q Из P ⊢ Q можно вывести, что P, P ⊢ P & Q. В рамках классической логики мы можем применить закон сокращения к левой части и получить: P ⊢ Q ⇒ P, P ⊢ P & Q ⇒ P ⊢ P & Q Получается, что выпивать кофе из кружки можно сколько угодно раз, она останется наполненной. По правилам же линейной логики мы не можем сократить P, P до P, так что P, P в нашем примере (P, P ⊢ P & Q) можно трактовать как наличие двух кружек кофе.

Линейная логика (Определение) (полная Markdown-версия поста: http://bit.ly/2ydfn1w) Линейная логика, как правило, определяется в терминах секвенциального исчисления (http://bit.ly/2xyEgBS) с ограничением структурных законов ослабления и сокращения. При этом мы получаем по две версии (аддитивную и мультипликативную) для операций (&, |) и логических констант (1, 0). Итак, рассмотрим линейную логику LL(V), где V — изначальный набор логических переменных. Обозначения: 1. Каждая логическая переменная является утверждением. 2. Для каждого утверждения A существует утверждение ¬A — отрицание A. 3. Для каждой пары утверждений P, Q можно построить ещё четыре утверждения: * A & B — аддитивная конъюнкция; * A ⨁ B — аддитивная дизъюнкция; * A ⨂ B — мультипликативная конъюнкция; * A | B — мультипликативная дизъюнкция. 4. Также заданы четыре константы, используемые в вышеперечисленных операциях: * ⊤ — аддитивная истина; * 0 — аддитивная ложь; * 1 — мультипликативная истина; * ⊥ — мультипликативная ложь. 5. Для каждого утверждения A существует существует также два дополнительных утверждения: * !A — экспоненциальная конъюнкция; * ?A — экспоненциальная дизъюнкция. 6. Линейная импликация определяется как ¬A | B (обозначение: A ⊸ B). 7. Утверждения A и B называются эквивалентными, если A ⊢ B и B ⊢ A; иными словами, ⊢ Γ, A истинно тогда и только тогда, когда истинно ⊢ Γ, B (обозначение: A ≡ B). Прилагательные "мультипликативный", " аддитивный", "экспоненциальный" объясняются дистрибутивностью операций. Мультипликативные операции дистрибутивны относительно аддитивных, если одна из операций — конъюнкция, другая — дизъюнкция (другими словами, произведение суммы есть сумма произведений, где под произведением понимается применение мультипликативной операции, а под суммой — применение аддитивной): A ⨂ (B ⨁ C) ≡ (A ⨂ B) ⨁ (A ⨂ C) A | (B & C) ≡ (A | B) & (A | C) Экспоненциальные операции превращают аддитивы в мультипликативы (экпоненциал суммы — произведение экспоненциалов): !(A | B) ≡ !A ⨂ !B !(A ⨁ B) ≡ !A & !B !⊤ ≡ 1 !0 ≡ ⊥ Также операции можно сгруппировать по полярности: ⨂, ⨁, 1, 0, ! имеют позитивную полярность, а |, &, ⊥, ⊤, ? — негативную. Теперь начнём строить законы вывода доказательств для линейной логики. Для начала, отметим, что если последовательность истинна, то истинны все её перестановки: если ⊢ Γ, то ⊢ Γ', где Γ' — перестановка Γ. Далее, запишем правила для операции отрицания: ¬(¬A) ≡ A ¬(A ⨂ B) ≡ ¬A | ¬B ¬(A ⨁ B) ≡ ¬A & ¬B ¬(A | B) ≡ ¬A ⨂ ¬B ¬(A & B) ≡ ¬A ⨁ ¬B ¬(1) ≡ ⊥ ¬(⊥) ≡ 1 ¬(0) ≡ ⊤ ¬(⊤) ≡ 0 ¬(!A) ≡ ?(¬A) ¬(?A) ≡ !(¬A) Обратите внимание на то, что отрицание меняет полярность констант и операций. Логические правила Логические правила, в которых встречаются операции конъюнкции и дизъюнкции мы переопределим, так как теперь у нас по две версии конъюнкции и дизъюнкции. Законы же для отрицания и кванторов остаются такими же как в классической логике. Мультипликативы 1. Если ⊢ Γ, Α и ⊢ Δ, Β, то ⊢ Γ, Δ, Α ⨂ Β. 2. Если ⊢ Γ, Α, Β, то ⊢ Γ, Α | Β. 3. Всегда истинно: ⊢ Γ, 1. 4. Если ⊢ Γ, то ⊢ Γ, ⊥. Аддитивы 1. Если Γ ⊢ Α и Γ ⊢ Β, то Γ ⊢ Α & Β. 2. Если Γ ⊢ Α, то Γ ⊢ Α ⨁ Β и Γ ⊢ Β ⨁ Α 3. Всегда истинно: ⊢ Γ, ⊤. Экспоненциалы 1. Если ⊢ Γ, то ⊢ Γ, ?Α. 2. Если ⊢ Γ, ?Α, то ⊢ !Γ, ?Α. 3. Если ⊢ Γ, Α, то ⊢ Γ, ?Α. Структурные правила Ослабление (ограниченное) Γ ⊢ Δ ⇒ Γ, !A ⊢ Δ Γ ⊢ Δ ⇒ Γ ⊢ ?A, Δ Сокращение (ограниченное) Γ, !A, !A ⊢ Δ ⇒ Γ, !A ⊢ Δ Γ ⊢ ?A, ?A, Δ ⇒ Γ ⊢ ?A, Δ Перестановка ⊢ Γ ⇒ ⊢ Γ' (Γ' — перестановка Γ)

Примеры Упражнение 1 Докажем, что эквивалентность утверждений является *отношением эквивалентности*. Рефлексивность: A ≡ A. Рефлексивность следует из аксиомы индентичности Симметричность: Α ≡ Β ⇒ Β ≡ Α. Симметричность очевидна из определения эквивалентности утверждений. Транзитивность: (A ≡ B) & (B ≡ C) ⇒ Α ≡ C. Распишем (A ≡ B) & (B ≡ C) ⇒ Α ≡ C в виде секвенций, перенося все утверждения на правую сторону: (⊢ ¬A, Β) & (⊢ Α, ¬B) & (⊢ ¬B, C) & (⊢ B, ¬C) ⇒ (⊢ ¬A, C) & (⊢ A, ¬C) Воспользуемся правилом сечения для левой части условия транзитивности: 1. (⊢ ¬A, B) & (⊢ ¬B, C) ⇒ ⊢ ¬A, C ⇒ A ⊢ C. 2. (⊢ A, ¬B) & (⊢ B, ¬C) ⇒ ⊢ A, ¬C ⇒ C ⊢ A. Транзитивность доказана. Итак, все три условия выполнены, значит эквивалентность утверждений является отношением эквивалентности и образует классы эквивалентности. Упражнение 2 Докажем, что A ⨂ 0 ≡ 0. Распишем в виде секвенций: 1. A ⨂ 0 ⊢ 0 ⇒ ⊢ ¬A ⨁ ⊤, 0. 2. 0 ⊢ A ⨂ 0 ⇒ ⊢ A ⨂ 0, ⊤. Начнём с первой секвенции. Согласно второму логическому закону для аддитивов, секвенция ⊢ ¬A ⨁ ⊤, 0 истинна если истинна секвенция ⊢ ⊤, 0. Истинность этой секвенции следует из третьего логического закона для аддитивов (⊤ справа). Вторая секвенция истинна согласно третьему логическому закону для аддитивов (⊤ справа). Эквивалентность доказана. Упражнение 3 Доказать, что (A ⨁ B) ⊸ C ≡ (A ⊸ C) & (B ⊸ C). Раскроем импликацию и распишем в виде секвенций: ⊢ ¬(A ⨁ B) | C ⇔ ⊢ (¬A | C) & (¬B | C) Раскрываем отрицание слева: ⊢ (¬A & ¬B) | C ⇔ ⊢ (¬A | C) & (¬B | C) Несложно заметить, что для доказательства этой эквивалентности достаточно доказать следующее: ⊢ (A & B) | C ⇔ ⊢ (A | C) & (B | C) Из правил для аддитивных и мультипликативных операций получаем: ⊢ A & B, C ⇔ (⊢ A, C) & (⊢ B, C) Теперь рассмотрим два случая. Для начала предположим, что утверждение справа от знака ⇔ (⊢ A, C и ⊢ B, C) истинно. Тогда истинность левой части следует из первого логического правила для аддитивов. Рассмотрим теперь ситуацию когда хотя бы одна из секвенций ⊢ A, C, ⊢ B, C не является истинной. Кроме первого правила для аддитивов нет правил, которые позволяют доказать выводимость аддитивной конъюнкции в правой части секвенции, значит в этом случае секвенция ⊢ A & B, C не является истинной. Эквивалентность доказана. --- Предлагаю самостоятельно доказать следующие эквивалентности для закрепления материала: 1. A | ⊤ ≡ ⊤ 2. A ⊸ B ≡ ¬B ⊸ ¬A 3. A ⊸ (B ⊸ C) ≡ (A ⨂ B) ⊸ C 4. A ⊸ ∀ y. B ≡ ∀ y. (A ⊸ B) (Переменная y не должна встречаться в свободном виде в утверждении A)

Скоро и про линейные типы будет, полагаю, спасибо @KolesnichenkoDS

а какие еще есть примеры кольц и семикольц кроме чисел?

ну мб вектора матрицы

оо точно

кроме как на первом курсе в матане их больше нигде не встречал

а что-то не связанное с числами напрямую?

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

а какие еще есть примеры кольц и семикольц кроме чисел?

почитай в вики

https://en.wikipedia.org/wiki/Ring_(mathematics)#Basic_examples

ага

хмм а почему Char в хаскеле не моноид?

А как его конкатить?

хмм а почему Char в хаскеле не моноид?

а как их складыать?

Коды складывать?

Кольца вместе с гомоморфизмами колец образуют категорию, обычно обозначаемую **Ring** (иногда так обозначают категорию колец с единицей, а категорию обычных колец обозначают **Rng** ). Топ нейминг

concat x y = toEnum (fromEnum x + fromEnum y)

concat x y = toEnum (fromEnum x + fromEnum y)

а единицей что будет?)

да и не заработает это

ну \0

0/

Это не слишком очевидное поведение

\0/

Лучше какой CharCodе ньютайп сделать, если это нужно

Меня больше всего обозначения радуют, уже перебрали все символы, все символы с двойным контуром и уже принялись за готический шрифт))

Ring Power \0 \0 \0

По моему я видел и другие шрифты, готический не предел

Ну да, куча всего

ComicSans

concat x y = toEnum (fromEnum x + fromEnum y)

смысл от этого

Удивительно, но мне уже даже нравится решение оберток моноидов в ньютайпе, это мб даже лучше, чем именные инстансы, и гибче

а что с именными инстансами?

Более неявно. Не, не гибче, я вспомнил, что инстансы можно на констрейты весить)

В пурсе есть именные инстансы?

Или это про хаскелл было?

Я сравнил хаскель с идрисом, наверное. Я в голове никаких языков не держал, когда писал это, сравнил решения)

А)

concat x y = toEnum (fromEnum x + fromEnum y)

concat = toEnum ... (+) `on` fromEnum

concat = toEnum ... (+) `on` fromEnum

понты

ERROR: S client not available

понты

ок

лол

ComicSans

https://twitter.com/christopherdone/status/913517638097219585

Идеально же

Идеально же

отступы бы только чуть больше

отступы бы только чуть больше

Зачем

Шрифт не моно, какая разница. Или моно... Там по скобке сложно понять

concat = toEnum ... (+) `on` fromEnum

что за три точки?

Не, это вообще жесть

как эту бодягу читать?

(...) = (.).(.)

что за три точки?

Сам же был в недавнем здесь треде насчёт того комбинатора

Зачем

отступ в один символ .... ну как-то совсем необычно

(...) = (.).(.)

ааа

а почему не просто $

отступ в один символ .... ну как-то совсем необычно

их же два

Поинтфри же, какой $

а

блин коры

я пока читал про ката

мне выдало вот как житьваще надо

Завтра ищешь в интернете книжку Categories for the Working Mathematician. Похуй если ничего не поймешь. Затем идешь на haskell.org и изучаешь стандартную библиотеку от корки до корки. Потом зубришь, именно, сука, вызубриваешь определения языка и стандартных библиотек - The Haskell 2010 Report, чтобы от зубов отскакивало. Когда напишешь свой первый катаморфизм, по пути изучив теорию типов на уровне TaPL-а, скачиваешь и изучаешь любую хаскеллевскую библиотеку с первоклассными функторами и морфизмами, рекомендую category-extras или recursion-schemes. Как переделаешь стандартную прелюдию, чтобы по крайней мере все рекурсивные схемы были выражены через комонады, можешь идти дальше - тебя ждет увлекательный мир теории категорий. Катаморфизмы, параморфизмы, зигоморфизмы, хистоморфизмы, препроморфизмы, анаморфизмы, апоморфизмы, футуморфизмы, постпроморфизмы, хиломорфизмы, крономорфизмы, синкрономорфизмы, экзоморфизмы, метаморфизмы, динаморфизмы алгебра и коалгебра Калвина Элгота наконец. Успех хиккующих выблядков / просто быдлокодеров типа рейфага или сисярп/джава-девелоперов, которые работают в Люксофте не будет тебя волновать и уже через пол года ты будешь получать такие гранты, что любой профессор будет теч при одном упоминании списка твоих публикаций.

я пока читал про ката

ката?

фолд

Ну да, я с утреца попросил же что почитать После Изучай хаскель во имя добра

ты мне кстати посоветовал про катаморфизмы

и я заебался искать по ним инфу

а зачем тебе ща рекурсивные схемы?

но нашел какой то смешной тьред зато

а kata слева или справа работает?