kir
18.02.2018
14:55:26
Оно делает именно то, что ты хотел
Vyacheslav
18.02.2018
14:56:27
нет
я говорил, что если ты на типе определил просто >>=, то автоматом юзаешь do-syntax, так это тоже можно делать, но это не очень понятно имхо потом
еще и семантику меняешь
Google
Alexander
18.02.2018
15:05:31
нельзя определить просто >>=
этим хаскель и хорош, кстати
Vyacheslav
18.02.2018
15:07:43
Правда?
kir
18.02.2018
15:07:46
Другого не завели.
Кстати, никогда не пытайтесть выполнить throw $ fix SomeException. По Ctrl-C ghci не прибивается
Vyacheslav
18.02.2018
15:07:57
Почему это хорошо?
Alexander
18.02.2018
15:08:51
потому что такие вещи пакуются в неймспейсы
kir
18.02.2018
15:09:23
Можно определить >>=, в локальном контексте. Но do-нотация всё равно рассахаривается в Prelude.>>=
Alexander
18.02.2018
15:09:39
в целом можно рассахаривать и в >>=
через RebindableSyntax
Например, если не любишь прелюдию
kir
18.02.2018
15:10:07
Мы его только что поминали)
Alexander
18.02.2018
15:10:12
вот да
суть в другом, что если у тебя есть >>= то ты описываешь контракт на этот метод через тайпкласс
Google
Alexander
18.02.2018
15:10:48
собственно, внезапно, все что имеет >>= и return это монада
kir
18.02.2018
15:11:08
(и выполняет monadic laws!)
Заставить их выполнить, к сожалению нечем, у нас тут не Agda
Alexander
18.02.2018
15:16:52
кстати, а агду ктонибудь уже пробовал?
есть смысл переключится с хаскеля на нее и попробовать разорбаться?
Imants
18.02.2018
15:23:28
Надеюсь, что в тему:
наткнулся на список блогов, сравнивающих Х. с другими языками:
https://wiki.haskell.org/Blog_articles/Comparisons
Pig
18.02.2018
15:45:49
Rushan
18.02.2018
15:48:38
извините, что не гугля спрашиваю
а в чём суть Agda и отличие от Haskell?
Imants
18.02.2018
15:59:26
Цель другая:
Agda из этой оперы:
https://en.m.wikipedia.org/wiki/Proof_assistant
Хаскель для.., ну, много чего. Но скорее не для формальных доказательств
Alexander
18.02.2018
16:00:25
ну вы уж меня извените, но цель хаскеля явно не в написании когда
это proof of concept
то что код можно писать это совпадение
а вообще,ч ем круче система типов тем круче язык
Imants
18.02.2018
16:01:50
.. О, оказывается, Agda написана на Хаскеле
Alexander
18.02.2018
16:02:04
я хочу язык, где можно указать тип "целое число от 1 до 20"
и чтобы тайпчекал выход за границу массива, например
вопрос, если есть комонады значит где то есть и контрмонады?
kir
18.02.2018
16:10:50
https://hackage.haskell.org/package/contravariant-1.4.1 контрмонад нет, есть контрафункторы, контр-аппликативы и контр-альтернативы
Warning: Kmett's code ahead
Alexander
18.02.2018
16:16:50
ну там суть в том, что функторы это кофункторы
Google
Alexander
18.02.2018
16:17:45
типа функторы это "могу писать + fmap" а контрфунктор "могу читать + fmap"
в полном соответствии с семантикой ко- и контр- вариантных типов
A64m
18.02.2018
16:18:17
Alexander
18.02.2018
16:18:49
хотя это то просто
ну в общем, в хаскеле изначально компилятор был интереснее самого языка
A64m
18.02.2018
16:22:18
ну нет, во-первых, пруфом этого концепта был LML, во вторых ghc делать стали позже чем хаскель. В 80-е установили что можно сделать практически полезный ленивый ФЯ, хаскель был уже платформой для дальнейшего экспериментирования, можно ли вообще более-менее эффективно компилировать такие ФЯ - такого вопроса уже не было, это не хаскельный эксперимент
Alexander
18.02.2018
16:23:08
значит меня обманули :(
но вообще там была аналогия с тем, что пролог тоже сделали но эксперимент не удался и получилось говно лютое
Alister
18.02.2018
16:24:59
пролог как будто не для людей делали
Alexander
18.02.2018
16:25:28
нужен уточняющий смайлик, не могу распарсить ирония это или утверждение :(
Alister
18.02.2018
16:26:32
ну я на нем в свое время писал нейросети простенькие
на слабо от препода
так-то мы на питоне писали, но я вызвался на прологе
Alexander
18.02.2018
16:26:57
и как, эффективно?
я кстати на удивление часто слышу пролог именно в связке с machine learning
Alister
18.02.2018
16:28:08
оказалось рекурсия и имутабельность вместе с процессом выполнения как достижения целей вполне подходят итеративным процесам достижения вменяемого респонса нейронов нейросети
Alexander
18.02.2018
16:28:40
я короче разобрался, комонадами называются контрмонады
Alister
18.02.2018
16:28:44
плюс мутабельность там раз и обчелся и вполне может быть описана гармоническим рядом
Alexander
18.02.2018
16:28:57
так как контрафункторы раньше назывались кофункторами, думаю дело тут нечисто
Google
Alexander
18.02.2018
16:29:21
Alister
18.02.2018
16:31:03
не уверен. это тот язык в котором любой опыт в другом программировании только мешает
A64m
18.02.2018
16:33:27
но вообще там была аналогия с тем, что пролог тоже сделали но эксперимент не удался и получилось говно лютое
ну а у экспериментов 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-х, сам язык новее
kana
18.02.2018
17:48:37
контр в функторах это скорее исключение, контрмонад нет (насколько я знаю)
именно ко обозначает переворачивание стрелок
а контр в кофункторах показывает не сколько дуальность, сколько контрвариантность
Alexander
18.02.2018
17:50:22
разве разворот стрелки не делает ковариантные штуки контрвариантными?
в этом же вроде бы и суть
kana
18.02.2018
17:50:57
моноид ковариантен?
Alexander
18.02.2018
17:51:21
моноид инвариантен по идее
kana
18.02.2018
17:52:07
ну собственно я к тому, что не думаю, что на все, что дуально, можно отнести к ко и контрвариантному
это две разные характеристики, которые пересеклись на функторах (по случайности)
Alexander
18.02.2018
17:53:00
а, я понял смысл нотации
это омонимы
kana
18.02.2018
17:53:25
Alexander
18.02.2018
17:54:05
ну, технически, математики все дуальное любят называть ковариантом и контрвариантом
типа у них такой Either
Google
Sergey
18.02.2018
18:04:46
Всем привет, как записать Int в файл? Можно даже побайтно
kana
18.02.2018
18:06:57
writeFile "./file" $ show 2
?
Index
18.02.2018
18:07:36
Контрафункторы это функторы в дуальную категорию, а вот кофункторы это дуал самих функторов. Функторы дуальны самим себе, так что кофункторы = функторы.
kana
18.02.2018
18:10:02
ох, вот оно че
Index
18.02.2018
18:10:08
Комонады это дуал монад, но они все еще в категории эндофункторов, а не в категории контрафункторов
Я не уверен, что контрафункторы образуют категорию вообще. По крайней мере очевидным образом не образуют.
Поэтому о контравариантных монадах речь вести не приходится.
Антон
18.02.2018
18:13:31
делает вид, что всё понимает, и кивает с умным видом
Index
18.02.2018
18:14:26
Я могу объяснить если меня спрашивать ;)
Антон
18.02.2018
18:17:38
так, функтор — отображение категории, сохраняющее до некоторой степени структуру, эндофунктор — функтор из категории в неё же. Пока всё верно?
Index
18.02.2018
18:19:35
Функтор это отображение одной категории в другую, да. Объекты в объекты, морфизмы в морфизмы, равенства в равенства (сохранение структуры композиции и id)
Эндофунктор из категории в себя, да.
Антон
18.02.2018
18:21:19
Категория эндофкнуторов — очевидно... А контрафункторы тогда что?
Index
18.02.2018
18:22:40
Контрафункторы это отображение категории в обратную категорию
kana
18.02.2018
18:22:46
хм, мы же можем сказать про некую любую категорию, обратна она или нет, получается контрафунктор всегда отображает в обратную этой же категории?
Index
18.02.2018
18:23:16
Эндофунктор над 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)