https://twitter.com/kmett/status/736182981145026561

но я не осилил

Я только общую постановку проблемы понял пока что.

То бишь, он утверждает, что есть в Hask вещи параметричные, но ненатуральные?

Такого не бывает

А, наоборрт

parametricity implies naturality

Он утверджает, что в Хаскеле неудобно теорию категорий моделировать, потому что там где в теоркатегорном языке говорят "for every" нельзя в Хаскельной версии просто воткнуть "forall".

И кидает ссылку, которая рассказывает о разнице формально.

Это уже совсем тонкие темы пошли. Надо читать.

Но суть в том, что если взять relevant квантификацию, т.е. pi из DependentHaskell вместо forall, то будет норм. Потому что pi не требует ни параметричности, ни натуральности

И натуральные трансформации можно будет выразить таким образом примерно: type f ~> g = pi a. f a -> g a Только он "больше", чем натуральные трансформации, т.к. не требует натуральности. Надо еще в комменте закон написать будет.

А чем вообще pi отличается от forall?

(Или не в комменте, если Agda)

Если Agda - то в глубоком юникоде.

по переменным, введенным через forall, паттерн-матчить нельзя. Вот если ты на Agda пишешь, то у тебя есть параметричность, если кайнд Set, и ее нет, если любой другой кайнд.

А в Dependent Haskell это квантификатором регулируется

А, то бишь, совсем deptypes

Паттерн-матчить в type-expr или в теле объявления?

т.е. такое невозможно id :: forall a. a -> a id x = case a of String -> "ha ha" _ -> x а с pi вместо forall возможно

в type-expr можно всегда через type families

речь про тело объявления

А в Агде, вроде, можно

в Агде можно, если введенная переменная не в Set

т.е. если ты натуральное число примешь, то можно, конечно

а если тип какой-то населенный, то нельзя

Но это странно, что от типа зависит параметричность

И McBride про это выступал и жаловался много, так что в DependentHaskell решили сделать "как надо".

А, то есть пример выше тоже не будет компилироваться?

Ага, такой хитрый id в Agda написать нельзя

потому что нельзя будет матчить по типу

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

Ее отобрали в т.ч. потому что Set особенный тем, что открытый

Ты можешь новые объявления делать и у него будут добавляться новые конструкторы

И подогнать под это нормальную теорию для паттерн-матчинга весьма нетривиально

Такие id обладают недоступной снаружи структурой и вообще. Как теоретики смотрят на то, что с pi у нас более чем бесконечное кол-во функций вида pi a . a -> a?

А Set1 тоже нельзя матчить?

Ну так рассмотри что-то вроде f :: pi (n :: Nat). forall (a :: Type). Vec n a -> Vec n a

Тебя же не смущает, что ты не параметричен по n :: Nat

И в зависимости от длины эта f может совершенно разные вещи делать

Например, для n как простых чисел делать reverse, а для остальных делать id

А Set1 тоже нельзя матчить?

Да, никакой Set lvl нельзя

>>> False == False in [False] True

Это ещё пол-беды! Вот где "интересное": >>> (False == False) in [False] False >>> False == (False in [False]) False

>>> False == False in [False] True

https://docs.python.org/3/reference/expressions.html#comparisons Comparisons can be chained arbitrarily, e.g., x < y <= z is equivalent to x < y and y <= z, except that y is evaluated only once (but in both cases z is not evaluated at all when x < y is found to be false).

там получается (False == False) and (False in [False])

>>> dis.dis(lambda: False == False in [False]) 1 0 LOAD_CONST 1 (False) 2 LOAD_CONST 1 (False) 4 DUP_TOP 6 ROT_THREE 8 COMPARE_OP 2 (==) 10 JUMP_IF_FALSE_OR_POP 18 12 LOAD_CONST 2 ((False,)) 14 COMPARE_OP 6 (in) 16 RETURN_VALUE >> 18 ROT_TWO 20 POP_TOP 22 RETURN_VALUE >>> dis.dis(lambda: (False == False) in [False]) 1 0 LOAD_CONST 1 (False) 2 LOAD_CONST 1 (False) 4 COMPARE_OP 2 (==) 6 LOAD_CONST 2 ((False,)) 8 COMPARE_OP 6 (in) 10 RETURN_VALUE >>> dis.dis(lambda: False == (False in [False])) 1 0 LOAD_CONST 1 (False) 2 LOAD_CONST 1 (False) 4 LOAD_CONST 2 ((False,)) 6 COMPARE_OP 6 (in) 8 COMPARE_OP 2 (==) 10 RETURN_VALUE

False == False iff False in [False]

Понятно, что сцепочили сравнение, непонятно, почему in, тоже "сравнение"

а вот фиг знает, но я ради интереса сейчас спрошу в IRC'е Python'истов) интересно, что ответят

Гвидо странный, поэтому такое

В той же доке >>> nan = float('NaN') >>> nan is nan True >>> nan == nan False <-- the defined non-reflexive behavior of NaN >>> [nan] == [nan] True <-- list enforces reflexivity and tests identity first

Так что всё плохо со здравым смыслом

И даже понятно, почему так сделали - is быстрее, чем == - но в целом то адище получается!

Да что про Гвидо говорить, он в районе 2007 хотел выпилить map, filter и reduce и заменить их на циклы и свой ужасный list comprehension.

Из него же: "И я их добавил, только потому что они были нужны 1 лисп-хакеру, который прислал работающие патчи"

Насчёт map(f, y) возвращающего объект, из которого при чтении удаляются элементы не хейтили ещё?

Гвидо - известный ФП-ниосилятор :)

Насчёт map(f, y) возвращающего объект, из которого при чтении удаляются элементы не хейтили ещё?

map итератор же возвращает - однопроходный

>>> i = map((1).__add__, [1,2,3]) >>> list(i) [2, 3, 4] >>> list(i) []

"раньше такого не было"

У меня полчаса бомбило, когда я это выяснил.

Интересно, что назначение монад я ещё более менее понимаю, а вот про аппликаторы не понимаю ничего. Нет, я знаю их интерфейс, я знаю, где они применяются, но совсем не понимаю концепции

Интересно, что назначение монад я ещё более менее понимаю, а вот про аппликаторы не понимаю ничего. Нет, я знаю их интерфейс, я знаю, где они применяются, но совсем не понимаю концепции

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

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

оборачивание чистой функции ничего не даст

pure не добавляет никакой информации

Интересно, что назначение монад я ещё более менее понимаю, а вот про аппликаторы не понимаю ничего. Нет, я знаю их интерфейс, я знаю, где они применяются, но совсем не понимаю концепции

на степике во 2 курсе по хаскелю хорошо про них рассказывается

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

И это как-то очень костыльно все

Мне кажется что до меня дошло после доклада Simon Marlow про haxl и зачем они applicative do запилили

всё так, выполняет команду, вызывает колбэки

на степике во 2 курсе по хаскелю хорошо про них рассказывается

Москвин? Смотрел его лекции в каком-то универе, до курсов не дошел

мне стало более понятно, когда я про free почитал

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

у любого контейнерного типа есть эффект

Объясни пожалуйста

ну вот Identity, например... :D

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

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

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

почему все всегда скатывается к "контейнеру типу"? нет никакого контейнера в общем случае

у любого контейнерного типа есть эффект

Не эффект, а контекст