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

Ы. Мощно ты задвинул, внушаить.

Ну, во-первых. Типы в Haskell представляются, если не отвлекаться на тонкости, как указатели на записи. То есть, вместо

data Tree = Nothing | Node Tree Int Tree

typedef struct Tree_struct *Tree;
struct Tree_struct {
  int tag; // 0 for Nothing, 1 for Node
  Tree left; // or some garbage for Nothing
   int value; // ditto
   Tree right; // ditto
}

Понятное дело, если добавить полиморфизм, то будет сложнее (и система шаблонов C++ вполне может не справиться), если добавить более сложные конструкторы — понадобятся юнионы, и так далее.

Как это связано с бесконечной структурой? Прекрасным образом связано. Если ты посмотришь на эту бесконечную структуру, то ты увидишь, что она примерно так и организована: куча записей, указывающих друг на друга. Да, целиком она, конечно, в память не влезет, но нам и не нужно: нам нужны только некоторые её элементы, которые вот таким образом представляются. Конечно, там есть и очень большие элементы, которые в память не влезают совсем — но большинство практически нужных таки влезают, а если что не влезет — падаем, вякнув про недостаток памяти.

И да, Haskell считает неподвижные точки. Посмотри, опять-таки, на процедуру вычисления неподвижной точки. Ты начинаешь с жопы (т.е., (_|_)), а затем много раз применяешь функцию. Это в точности соответствует тому, что происходит в компе: ты начал с ситуации, в которой НИЧЕГО не известно, а затем начал её уточнять. Естественно, GHC может оптимизировать этот процесс, и, более того, делает это (и очень здорово), но в центре там именно оно.

Да, в таком виде процесс вычисления неподвижной точки никогда не остановится; но нам часто это и не нужно. Грубо говоря, если нам нужно значение f (fix g), где f — какой-то простой тип (Int, например), то мы можем не вычислять точно значение fix g, а остановиться, когда f от очередного значения станет отличным от (_|_). Поскольку функция f монотонна, мы знаем, что f от дальнейших значений может быть только больше текущего — а, так как больше нет, оно будет таким же. И f (fix g) будет, по непрерывности f, супремумом этой последовательности — то есть, мы уже его знаем. Можем дальше не вычислять.

Но какое отношение НТ могут иметь к векторизации?

Вот тут не знаю.

Как всегда, после того, как написал вопрос, стало чуть понятнее, что надо гуглить, и нагуглил я вот это:

http://anton-k.github.io/ru-haskell-book/book/10.html

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

Как это связано с бесконечной структурой? Прекрасным образом связано. Если ты посмотришь на эту бесконечную структуру, то ты увидишь, что она примерно так и организована: куча записей, указывающих друг на друга. Да, целиком она, конечно, в память не влезет, но нам и не нужно: нам нужны только некоторые её элементы, которые вот таким образом представляются. Конечно, там есть и очень большие элементы, которые в память не влезают совсем — но большинство практически нужных таки влезают, а если что не влезет — падаем, вякнув про недостаток памяти.

Хм... Но если я смотрю на эту структуру с формальной точки зрения про семантические домены (которую в Haskell активно пропагандируют), то я должен на это смотреть как на возрастающую цепочку этих самых доменов с инъекциями вверх и проекциями вниз (ещё тот вынос мозга, ну да ладно)... В какой момент происходит переход от этой математике к указателям? Вот что мне совсем не понятно в этом случает. Если смотреть абстрактно, то да, вроде как, понятно, что вот, используя указатели мы можем строить потенциально бесконечные структуры. Но... Каков переход от одного к другому?

А если вообще, смотреть не на Haskell, а на тот же Си, например. Есть структура:

struct tag { struct tag *next };

Получается, по теории, мы должны для неё написать рекурсивное уравнение, примерно такое:

struct tag = struct(pointer(struct tag))

И что?... Получаем опять вынос мозга. То есть, я понимаю, конечно, что pointer должен быть в каком-то смысле ленивым. Но больше я ничего не понимаю :( Ну, то есть. Если действовать по рецепту fix, то мы должны написать тут функцию

F(struct tag)(n) = struct(pointer(struct tag))(n)

Где n - это какие-нибудь штуки, вроде: sizeof, fieldoffset и прочее. А struct (как функция) затаскивает эти вещи в свои поля и чего-нибудь там как-нибудь суммирует. И что дальше? Дальше мы должны начать с задницы? Типа:

F(_) = struct(pointer(_)) = struct(pointer-4) = fix(F)

Ок. Замечательно. Эту часть я понимаю. Но как это всё превратить в алгоритмы? Я же не могу автоматом, как в Haskell написать:

typedef struct tag *struct.tag; struct tag { struct.tag **next };

БррРр! Вынос мозга.

И да, Haskell считает неподвижные точки. Посмотри, опять-таки, на процедуру вычисления неподвижной точки. Ты начинаешь с жопы (т.е., (_|_)), а затем много раз применяешь функцию. Это в точности соответствует тому, что происходит в компе: ты начал с ситуации, в которой НИЧЕГО не известно, а затем начал её уточнять. Естественно, GHC может оптимизировать этот процесс, и, более того, делает это (и очень здорово), но в центре там именно оно.

Но у него в ядре, которое STG вообще ничего нет о неподвижных точках. Там есть let, куча и выражения... И никаких f(f(f...(_))) там тоже нет.

Или как? Или они просто берут STG и доказывают: вот тут мы используем подставновки значений из кучи, и это соответствует вычислению неподвижной точки, которая единственна и неповторима, поэтому мы её и найдём?

Эмс. Но... В итоге же, получается, что там нет вычисления собственно самой fix, а есть некий процесс, который к ней сходится, и он существует в виде некоторого состояния некоторого графа, который при каждом шаге вычисления как-то меняется.

ArrRrggGgH! Опять вынос мозга! А где же функциональная чистота тогда!?

я должен на это смотреть как на возрастающую цепочку этих самых доменов с инъекциями вверх и проекциями вниз

Стоп-стоп-стоп. Начнём с того, что «структура» — это ОДИН домен. Другой вопрос, что он СТРОИТСЯ как предел такой цепочки. Но он сам по себе.

В какой момент происходит переход от этой математике к указателям?

А ты посмотри на ту цепочку. В ней ведь каждый следующий домен получается применением функтора к предыдущему. А функтор перегоняет домен X в домен Nothing | Node X Int X. А последнее — и есть структура с тегом, двумя указателями на X, и числом.

struct tag = struct(pointer(struct tag))

Чаво? Там просто data Tag = Tag Tag.

И никаких f(f(f...(_))) там тоже нет.

Есть, конечно. Только STG — это уже ОЧЕНЬ суровая оптимизация. Если хочешь понять, как работает какой-нибудь рэйтрейсинг — не надо смотреть на скомпилированный бинарник, нужно понимать на уровне повыше.

нет вычисления собственно самой fix, а есть некий процесс, который к ней сходится

А в чём разница? Мне так кажется, что процесс, который сходится к ответу — это и есть процесс вычисления ответа. Не?

и он существует в виде некоторого состояния некоторого графа, который при каждом шаге вычисления как-то меняется.

Да забудь ты про эти внутренности. Какие там оптимизации сделаны — это глубоко по барабану.

Не. Я не хочу о внутренностях забывать, потому что мне интересен именно переход от теории, к тому, что реально происходит в ходе вычисления. От деталей и оптимизаций можно и отказаться, но вообще технику хотелось бы представлять. И потом, авторы же говорят, что STG - это ядро Haskell, остальное - сахар.

Стоп-стоп-стоп. Начнём с того, что «структура» — это ОДИН домен. Другой вопрос, что он СТРОИТСЯ как предел такой цепочки. Но он сам по себе.

МххХх... Так вот и вопрос, по каком принципу мы переходим от формулы для домена к структуре, которая является пределом? Почему рекурсия магическим образом заменяется на указатели? И почему в упомянутой мной работе, которая C.Gunter, D.Scott Semantic Domains, о пределах говорится, как о бесконечных штуках. Вот допустим, предел же для функции, которая строить последовательность Фибоначчи, он бесконечный. И предел для функции, которая строит список - тоже. Я имею в виду супремум. А тут формула по структуре, вроде, точно такая же, но предел почему-то конечный.

Может быть, что это не сам предел? А генератор последовательности? В таком случае, вроде, всё понятнее становится. Нет? Те места, куда можно подставить задницу, и должны быть указателями с навешанным на них тэгом (чтобы это была задница текущего домена, а не вообще задница). А когда мы пишем data, то мы пишем генератор? Нет?

А ты посмотри на ту цепочку. В ней ведь каждый следующий домен получается применением функтора к предыдущему. А функтор перегоняет домен X в домен Nothing | Node X Int X. А последнее — и есть структура с тегом, двумя указателями на X, и числом.

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

А в чём разница? Мне так кажется, что процесс, который сходится к ответу — это и есть процесс вычисления ответа. Не?

Ну, вот я об этом и спрашиваю. Только ещё дополнительно спрашиваю: как формулу для типа превратить в предел. И делаю предположение: в предел (или даже не в сам предел, а в проекцию его на нечто конечное) она превращается в ходе выполнения программы. А в ходе компиляции, она превращается в генератор.

Так вот и вопрос, по каком принципу мы переходим от формулы для домена к структуре, которая является пределом

Э... пределом является домен. Как его строить — известно. Или ты про что?

Почему рекурсия магическим образом заменяется на указатели?

Указатели — это просто инструмент. Ну, вспомни, как начинал программить. Как ты от понятия «список» переходил к «связному списку» с указателями и структурами? Тут точно то же самое.

о пределах говорится, как о бесконечных штуках

Ну да, в интересных случаях предел будет бесконечным множеством.

но предел почему-то конечный.

Это почему это? Предел будет (в интересных случаях) бесконечным множеством. И что? Даже тип Integer имеет бесконечно много возможных значений, кого это когда смущало.

Может быть, что это не сам предел?

Что «это»?

А чем функтор отличается от функции (я просто совсем нуб)?

А каким местом ты тогда эти тексты осиливал?

Если ОЧЕНЬ грубо и в применении именно к доменам — функтор действует на типах, функция на значениях. От функции требуется непрерывность, от функтора — определённые взаимоотношения с проекциями.

Если более точно — man теория категорий. Там, правда, говорят не «функция», а «морфизм».

И не является ли этот функтор как раз генератором сходящейся последовательности?

Он определяет последовательность доменов. Слово «сходящейся» лишнее, предел есть у любой последовательности.

А построение самого предела (или точнее, его проекции с текущим входным аргументом) - это как раз выполнение программы?

Нет. Выполнение программы — это построение неподвижных точек определённых функций. А типы в рантайме вообще отсутствуют.

И отдельно про Си.

struct tag = struct(pointer(struct tag))

Чаво? Там просто data Tag = Tag Tag.

Ну мне тут интересно не то, чему она в Haskell соответствует. А самостоятельная внутри-Си-шная семантика. Для которой, вроде как, важно, что это именно указатель. Под struct tag я имел в виду просто некую штуку... Которая предел (должна превратиться в предел?). Надо было так, наверное писать:

struct.tag = struct(pointer(struct.tag))

Если мы на это смотрим, как на генератор, то он получается в виде

F = lam struct.tag -> struct(pointer(struct.tag))

Так? Генерировать он должен последовательность, которая сойдётся к функции, которая должна отвечать на разные запросы, типа, а дай мне размер этого типа. Эта функция будет определяться так:

F(F(F(... F(_)...)))(SIZE)

И чтобы получить ответ, мы должны делать так:

1. Биндим сначала к struct.tag задницу.

2. ??? А вот дальше что? Бесконечно крутить, пока не получим фиксированный результат? Но тогда всякие штуки, вроде:

struct tag { struct tag X};

будут зависать. Или мы мы можем поменять SIZE и задницу местами? Ну, вместо:

F: (SIZE -> N) -> (SIZE -> N)

написать:

F: ((SIZE -> N) -> SIZE) -> N

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

Ne?

А каким местом ты тогда эти тексты осиливал?

Ну, надеюсь, мозгом :) Они там вместо «функтор» пишут «оператор» для доменов. Ок. Понятно.

Э... пределом является домен. Как его строить — известно. Или ты про что?

Ну вот я как раз про это: как его строить? Пока что, у меня такое представление:

1. Есть у нас формула, допустим data List = Nothing | Int List.

2. Мы строим из этой штуки функтор (!?), который генерирует. Нам же нужен предел, а предел без функции (функтора?) не бывает: F = lambda List -> Nothing | Int List

3. А вот дальше что?

3.1. По идее, я могу предположить. Мы смотрим, ага List - это переменная, и вместо List мы будем подставлять задницу, а потом к полученному применять снова нашу F и так далее. И кто-то где-то доказал, что если теперь этот List заменить на List *, то мы получаем искомый предел? Но, вроде, для такой F этот самый предел должен быть бесконечным. Как он превращается в конечную структуру... БррРрр!? То есть, я понимаю, интуитивно, что это те же самые связные списки из далёкого детства. Но я формальный переход не понимаю от одного к другому. (А есть что-нибудь про то, как Haskell рассахаривается в STG?)

3.2. Или мы просто говорим, что не будем мы никаких пределов считать, а просто вернём саму F, и если она там будет сама к себе применятся в процессе конструирования списков, то всё будет ОК, потому что она непрерываная и будет у неё предел в итоге вычисления.

3.3. Или ...?

Ну вот я как раз про это: как его строить?

Предел определён при помощи универсального свойства. С точностью до изоморфизма. Явная конструкция даёт ОДИН из вариантов.

Ты б сказал раньше, что явной конструкции не видел. Я ж не знаю.

Конструкция примитивная. Есть последовательность X_0, X_1, X_2,... доменов, для каждого i зафиксирована проекция p_i : X_{i+1}->X_i. Предел строится так: это множество всех последовательностей (x_0, x_1, x_2,..), где x_i принадлежит X_i и p_i(x_{i+1}) = x_i. Проекции из предела на отдельные X_i — это просто взятие одного элемента из последовательности. Доказать, что это — именно предел, проще простого.

Но, вроде, для такой F этот самый предел должен быть бесконечным.

Что это вообще значит?

потому что она непрерываная

Кто непрерывный? Ты понимаешь разницу между типом и значением?

Конструкция примитивная. Есть последовательность X_0, X_1, X_2,... доменов, для каждого i зафиксирована проекция p_i : X_{i+1}->X_i. Предел строится так: это множество всех последовательностей (x_0, x_1, x_2,..), где x_i принадлежит X_i и p_i(x_{i+1}) = x_i. Проекции из предела на отдельные X_i — это просто взятие одного элемента из последовательности. Доказать, что это — именно предел, проще простого.

А p_i откуда берётся? Я так понимаю, именно для её реализации и нужен указатель? Но как мы понимаем, что p_i надо вот именно в это место вставить по описанию типа? Вот конкретно для списка как это всё будет построено?

Кто непрерывный? Ты понимаешь разницу между типом и значением?

Видимо, пока не очень. Но Haskell же работает с типами как-то. Значит, в какой-то момент типы являются значениями? Нет? Ну и ещё вопрос тогда: а разве домены нельзя считать каким-нибудь чупом, чтобы на них тоже строить непрерывные функции?

А p_i откуда берётся?

Так это, прости, не конструкция предела, а конструкция самой последовательности. Если по-разному задать эти p_i, то будут разные пределы.

Для случая, когда строится именно неподвижная точка функтора F, берётся X_0 = {(_|_)} (т.е., множество из одного элемента), X_{i+1} = F(X_i). Соответственно, проекция p_0 : X_1 -> X_0 строится единственно возможным образом, а p_{i+1} : F(X_{i+1}) -> F(X_i) берётся равной F(p_i).

Я так понимаю, именно для её реализации и нужен указатель?

Не нужно это реализовывать. ТИПОВ В СКОМПИЛИРОВАННОМ БИНАРНИКЕ УЖЕ НЕТ!

Значит, в какой-то момент типы являются значениями?

С точки зрения компилятора — естественно, там даже модули будут значениями. Только он от них избавится.

С точки зрения программы — нет, конечно.

Ну и ещё вопрос тогда: а разве домены нельзя считать каким-нибудь чупом, чтобы на них тоже строить непрерывные функции?

Нельзя. Хотя бы потому, что их слишком много. Парадокс Рассела будет, во все края. Ну и с упорядочением непонятки — как их упорядочивать-то?

Так это, прости, не конструкция предела, а конструкция самой последовательности. Если по-разному задать эти p_i, то будут разные пределы.

Ок. Это понятно.

Для случая, когда строится именно неподвижная точка функтора F, берётся X_0 = {(_|_)} (т.е., множество из одного элемента), X_{i+1} = F(X_i). Соответственно, проекция p_0 : X_1 -> X_0 строится единственно возможным образом, а p_{i+1} : F(X_{i+1}) -> F(X_i) берётся равной F(p_i).

Всё равно, не ясно. Точнее так. Саму конструкцию предела я понимаю. Я не понимаю, как она представляется в самом компиляторе. И как он из этого получает запись из нескольких полей с указателями.

Вообще, по идее, указатели они же соответствуют взятию какого-нибудь значения из текущего окружения, ну, иными словами - подстановку. И раз в итоге из типа получается нечто с указателем, значит, получается нечто, куда можно подставлять значения. Значит, это нечто, является... Эмс? Чем? lambda-абстракцией. То есть, получается, эмс... Чем, получается? Не понятно. Это описание проекции что-ли такое? Или самой F? Вроде, не похоже на описание проекции, потому что проекции в разных местах последовательности устроены по-разному. Значит, вот получаемая структура - это описание функтора?

Не нужно это реализовывать. ТИПОВ В СКОМПИЛИРОВАННОМ БИНАРНИКЕ УЖЕ НЕТ!

Меня же как раз и интересует то, чего компилятор с типами делает. Как-то не похоже, что он от них совсем избавляется, потому что в STG data тоже есть.

Нельзя. Хотя бы потому, что их слишком много. Парадокс Рассела будет, во все края. Ну и с упорядочением непонятки — как их упорядочивать-то?

Но компилятор же их как-то обрабатывает!? А раз обрабатывает, значит, работает с ними как со значениями, которые должны подчиняться всяким «законам вычислимости» и прочим непрерывным радостям. Разве нет? Не магически же он работает, в конце-то концов.

И как он из этого получает запись из нескольких полей с указателями.

Посмотри на функтор. X -> Nothing | Node X Int X. Это именно что запись с тегом, числом и двумя указателями на X.

Но компилятор же их как-то обрабатывает!?

И что? А если программа солнечные пятна будет обсчитывать, думаешь, внутри неё целое солнце будет?

В продакшн функциональном программировании задротские штучки не используются никогда.

И что? А если программа солнечные пятна будет обсчитывать, думаешь, внутри неё целое солнце будет?

Ну. Модель-то пятен там точно будет. Интересно, какая модель у Haskell.

Посмотри на функтор. X -> Nothing | Node X Int X. Это именно что запись с тегом, числом и двумя указателями на X.

То есть, структурой он моделирует этот самый функтор?

Кстати, дурацкий вопрос (дурацкий, потому что, наверняка, это где-то описано, но гуглить я уже устал, поэтому спрошу, как дурак тут), а в Haskell можно как-нибудь понаблюдать за тем, что реально происходит в памяти?

Пользуясь случаем хотел уточнить мысль, которая меня давно беспокоит. В Хаскеле, насколько я знаю, все функции уже по определению каррированные т.е. /xy.xy это /x/y.xy. Получается что каррирования как такогого и нет, любая запись - это сахар для записи одноаргументных функций. Тогда почему все говорят, что в Хаскеле есть каррирование?

Кто тебе такую глупость сказал? В Хаскеле есть тип-произведение, есть тип функций из него, и т.п.

Другой вопрос, что в стандартной библиотеке почти всё каррированное, да.

Интересно, какая модель у Haskell.

У Haskell никакой. У GHC — скорее всего, просто символы, обозначающие типы. И правила игры с ними.

То есть, структурой он моделирует этот самый функтор?

Ну, опять-таки, если добавить какие-то более сложные конструкторы — потребуются union-ы. Это в таком простом случае можно обойтись одной структурой.

Ну, опять-таки, если добавить какие-то более сложные конструкторы — потребуются union-ы. Это в таком простом случае можно обойтись одной структурой.

Про union-ы, в общем-то понятно. Главное непонятка у меня была с рекурсиями в определениях доменов. Большое спасибо за разъяснения. Где тут яростно плюсовать можно? :)

А вот ещё один глупый вопрос о применении теории к практике. Меня всё интересует, как она работает для языков, которые существенно от Haskell отличаются. Вот, допустим, есть у меня C (ну, или любая имеративщина, где можно определять структуры). Когда я пишу для структуры:

record.field

С точки зрения теории доменов — ничего общего.

Ну, посмотри определение проекции.

Так определение понятно. Что это вот такая непрерывная функция p, что p p меньше id и образ у неё домен. Но... Эмс. А в не-Haskell что таким проекциям соответствует?

Да ничего. Если ленивости нет, от всей этой опупеи с доменами остаётся с гулькин нос. Не совсем ничего, но почти.

И да, для проекции нужны две функции, p и i. p i = id, i p < id.

И да, для проекции нужны две функции, p и i. p i = id, i p < id.

Ну там в статье было про финитарную проекцию. И да, там есть и нормальное определение. С двумя функциями. Embedding (видим, i - это injection) projection pair. Да?

Но почему обращение к полю структуры не подходит под эту роль?

Если мы скажем, что (i x) - это создание структуры, в которой всё, кроме field, инициализировано тем, что мы считаем задницей (нулями, например), а field инициализировано x. Тогда (i x).field будет обратной функцией. И, вроде, свойства сохранятся: x = (i x).field и (i s.field) будет меньше s (если мы возьмём стандартный индуцированный порядок для декартовых произведений, которым является структура).

Есть ли в этом ошибка?

Да ничего. Если ленивости нет, от всей этой опупеи с доменами остаётся с гулькин нос. Не совсем ничего, но почти.

А как именно ленивость даёт возможность всему этому заиграть всеми красками?

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

Тогда почему все говорят, что в Хаскеле есть каррирование?

потому что то, что ты описал, и каррирование - это одно и то же

Не распарсил поэтические эпитеты и метафоры