(и выполняет monadic laws!)

Заставить их выполнить, к сожалению нечем, у нас тут не Agda

кстати, а агду ктонибудь уже пробовал?

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

Надеюсь, что в тему: наткнулся на список блогов, сравнивающих Х. с другими языками: https://wiki.haskell.org/Blog_articles/Comparisons

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

Haskell для кода, Agda для формализмов

Цель другая: Agda из этой оперы: https://en.m.wikipedia.org/wiki/Proof_assistant Хаскель для.., ну, много чего. Но скорее не для формальных доказательств

ну вы уж меня извените, но цель хаскеля явно не в написании когда

это proof of concept

то что код можно писать это совпадение

а вообще,ч ем круче система типов тем круче язык

.. О, оказывается, Agda написана на Хаскеле

я хочу язык, где можно указать тип "целое число от 1 до 20"

и чтобы тайпчекал выход за границу массива, например

вопрос, если есть комонады значит где то есть и контрмонады?

https://hackage.haskell.org/package/contravariant-1.4.1 контрмонад нет, есть контрафункторы, контр-аппликативы и контр-альтернативы

Warning: Kmett's code ahead

ну там суть в том, что функторы это кофункторы

типа функторы это "могу писать + fmap" а контрфунктор "могу читать + fmap"

в полном соответствии с семантикой ко- и контр- вариантных типов

то что код можно писать это совпадение

пруф какого концепта-то?

пруф какого концепта-то?

существование полностью ленивого тьюринг-полного языка, емнип

хотя это то просто

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

ну нет, во-первых, пруфом этого концепта был LML, во вторых ghc делать стали позже чем хаскель. В 80-е установили что можно сделать практически полезный ленивый ФЯ, хаскель был уже платформой для дальнейшего экспериментирования, можно ли вообще более-менее эффективно компилировать такие ФЯ - такого вопроса уже не было, это не хаскельный эксперимент

значит меня обманули :(

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

пролог как будто не для людей делали

нужен уточняющий смайлик, не могу распарсить ирония это или утверждение :(

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

на слабо от препода

так-то мы на питоне писали, но я вызвался на прологе

и как, эффективно?

я кстати на удивление часто слышу пролог именно в связке с machine learning

оказалось рекурсия и имутабельность вместе с процессом выполнения как достижения целей вполне подходят итеративным процесам достижения вменяемого респонса нейронов нейросети

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

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

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

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

рекомендуешь?

не уверен. это тот язык в котором любой опыт в другом программировании только мешает

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

ну а у экспериментов 80-х с ФЯ результаты были сносные, так что вопрос можно ли вообще такое делать уже потом не стоял | | RT | y | fib | prim | | | | | 20 | 300 | | ------- | --------- | --- | ---- | ---- | | C | | | 0.46 | 0.2 | | LML | G-machine | 84 | 0.92 | 0.5 | | LML | G-machine | 88 | 0.78 | 0.26 | | VAX ML | FAM | 84 | 0.5 | 1.2 | | SML/NJ | cmachine | 88 | 0.4 | 0.38 | | Franz | | | | | | Lisp | | | 1.1 | 1.1 | | SASL | SECD | 84 | 31 | 20 | | LCF ML | Stanford | | | | | | LISP | 84 | 46 | 29 | | Miranda | S-K | 88 | 72 | 12.3 |

вот у ФЯ 70-х производительность была вообще никакая (в этой таблице это LCF ML и SASL)

мирандовый рантайм это тоже изобретение 70-х, сам язык новее

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

советую не использовать нейминг функторов на всем остальном

контр в функторах это скорее исключение, контрмонад нет (насколько я знаю)

именно ко обозначает переворачивание стрелок

а контр в кофункторах показывает не сколько дуальность, сколько контрвариантность

разве разворот стрелки не делает ковариантные штуки контрвариантными?

в этом же вроде бы и суть

моноид ковариантен?

моноид инвариантен по идее

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

это две разные характеристики, которые пересеклись на функторах (по случайности)

а, я понял смысл нотации

это омонимы

это две разные характеристики, которые пересеклись на функторах (по случайности)

но это не факт)

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

типа у них такой Either

Всем привет, как записать Int в файл? Можно даже побайтно

writeFile "./file" $ show 2 ?

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

Нет. Комонады ковариантны.

Контрафункторы это функторы в дуальную категорию, а вот кофункторы это дуал самих функторов. Функторы дуальны самим себе, так что кофункторы = функторы.

ох, вот оно че

Комонады это дуал монад, но они все еще в категории эндофункторов, а не в категории контрафункторов

Я не уверен, что контрафункторы образуют категорию вообще. По крайней мере очевидным образом не образуют.

Поэтому о контравариантных монадах речь вести не приходится.

делает вид, что всё понимает, и кивает с умным видом

Я могу объяснить если меня спрашивать ;)

так, функтор — отображение категории, сохраняющее до некоторой степени структуру, эндофунктор — функтор из категории в неё же. Пока всё верно?

Функтор это отображение одной категории в другую, да. Объекты в объекты, морфизмы в морфизмы, равенства в равенства (сохранение структуры композиции и id)

Эндофунктор из категории в себя, да.

Категория эндофкнуторов — очевидно... А контрафункторы тогда что?

Контрафункторы это отображение категории в обратную категорию

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

Эндофунктор над C это C -> C Контрафунктор над C это C -> Op(C) или Op(C) -> C (не важно)

Для любой категории C, например Hask

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

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

В изоляции ты не определишь, категория обратная или нет, это не её собственное свойство

на примере Hask 1. определим категорию H1 так, что объекты в ней типы в Хаскеле с кайндом *, а стрелки между объектами A B это функции A -> B (с оговорками про bottom) 2. определим категорию H2 так, что объекты в ней типы в Хаскеле с кайндом *, а стрелки между объектами A B это функции B -> A (с оговорками про bottom)

H1 и H2 это обратные (opposite) категории