угу. И не пользоваться чужими библиотеками. И общей рекурсией

Так это ж жизнь хаскелиста, законы доказываем на бумажке, а termination checking на авось.

Только в итоге вроде и норм выходит.

Вот dependent Haskell как раз интереснее, чем от боттомов огораживаться.

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

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

+1

Но, казалось бы, и ничего страшного, ведь bottom и должен все ломать

И живешь дальше, и все хорошо

Меня больше волнует, что в Haskell нет релевантной квантификации, из-за чего нельзя naturality выражать и приходится ее аппроксимировать через parametricity.

И какой-нибудь там type f ~> g = forall a . f a -> g a из-за этого не позволяет выразить любые натруальные трансформации.

Что за naturality?

fmap f . trans == trans . fmap f, где trans :: g ~> h?

Да. Оно следует из parametricity, но не наоборот

Например, у нас в Haskell есть fmap :: forall f a b . Functor f => (a -> b) -> (f a -> f b). Но т.к. a и b введены через forall (имеем parametricity), то из первого закона fmap id = id следует и второй закон fmap (f . g) = fmap f . fmap g.

В теории категорий один закон из другого не следует, поэтому их два.

Т.к. там не parametricity используется, когда говорят "for every object exists ..."

Так. У хаскелля есть параметричность, из которой следует натуральность. Не означает ли это, что у хаскелля есть так же и натуральность?

Ага, и она везде, где параметричность

Но ее нет самой по себе, поэтому мы не можем выражать вещи, которые натуральны, но не параметричны

Точнее, можем, но на case-by-case основе, добавлением всяких там констрейнтов

Например?

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

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 может совершенно разные вещи делать

ERROR: S client not available

Например, для 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 запилили

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