Обновить
2
0.9

Специалист по теории типов USB-кабелей

Отправить сообщение

Вроде с детерминизмом в физике разделались сто лет назад.

Кажется, мы заходим на второй круг.

  1. В MWI (и некоторых других интерпретациях) даже квантмех детерминирован.

  2. Квантмех действует на все объекты одинаково. Нет никаких оснований считать, что у человека больше свободы воли на основе отсылок к квантмеху, чем у электрона, у бильярдного шара или у песчинки, выбирающей, как именно ей скатываться с холма.

Хаос предполагает отсутствие детерминированного результата.

Меня этот тред начинает очень сильно печалить :'-(

Хаос — это, если по-человечески, сильная зависимость системы от начальных условий, не более.

Или, если топологически, функция (детерминированная!) f на топологическом пространстве X хаотична, если множество её периодических точек плотно в X и для любых открытых U, V в X. ∃ u ∈ U.∃ n ∈ ℕ. f^n(u) ∈ V (упрощая — функция бесконечно бегает почти по всему пространству).

Простейшая, абсолютно детерминированная функция

f : [0; 1] → [0; 1]
f x | x ≤ ½ = 2x
    | otherwise = 2 - 2x

хаотична.

Свобода воли может это обстоятельство использовать.

Для протокола — этот аргумент не в ту сторону, в которую вы думаете.

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

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

Э, ну, я не знаю, законы физики заставляют?

Вроде, очевидная вещь, что порядок из хаоса получается большим трудом, а хаос из порядка - сам собой.

А связь со свободой воли здесь какая?

Там же все это уже можно в последних стандартах (тайпклассы, Comparable, ...), как там оценивается мощность системы типов?

Там нет тайпклассов, концепты не позволяют universal quantification, концепты не могут быть объектами высшего класса, и тела функций не проверяются согласно концептам.

Зависимых типов тем более нет и никогда не будет.

Короче, в плюсах всё очень плохо что с точки зрения выразительной силы, что с точки зрения эргономики того, что есть (хиндли-милнера тоже не завезли, скажем).

Вот вы все тянете в свою сторону - в сторону того чтобы было что-то НЕЛЬЗЯ.

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

В плюсах я могу написать функцию

template<typename T>
std::vector<T> sort(std::vector<T>, Comparator<T>);

но у меня нет способов композабельно и проверяемо компилятором выразить, что результирующий массив действительно отсортирован. Эта функция так может возвращать исходный массив без какой-либо сортировки, или пустой массив, или сделать partial sort на первых 20 элементах.

В языках с очень развитой системой типов я могу написать

sort : (input : List a)
     → (ord : Order a)
     → (res : List a ** Sorted res ord input)

— функция возвращает и отсортированный список, и доказательство того, что этот список — отсортированная версия входа. И отмечу, что в так часто вспоминаемом в таких тредах хаскеле так нельзя, его система типов для этого недостаточно развита.

А мне надо чтобы было МОЖНО!

А почему б не писать на джаваскрипте? Там вообще всё можно, никаких запретов!

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

Ну пишете

addNumStr : String → Int → String

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

А в языке с очень развитой системой типов можно заодно доказать, скажем, что

s1 + addNumStr s2 n = addNumStr (s1 + s2) n
addNumStr "" n = toString n

и прочие угодные вашей душе вещи.

Получается что у вас обратная парадигма - все ИЗНАЧАЛЬНО можно (пусть и с непонятными результатами)

Нет, не получается.

Если конечно у меня есть право тоже что-то объяснять.

Это право есть у всех, кто сначала разобрался в предмете.

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

Точно так же, кстати, как верующий человек воспринимает горящий куст (или луч света из облаков) как знак.

не вижу механизма детерминированности, а в случае LLM наоборот

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

Собственно, как иллюзия, то есть род непосредственно воспринимаемого чувства, бог есть у очень немногих людей. Большинство верующих его воспринимают как идею, то есть некоторое умозрительное объяснение чувственного опыта (неважно в данном случае, истинное или нет).

А это неважно: можно переформулировать вопрос в терминах чувственного опыта. Или веры во что-то выше/больше/етц нас. Веры в ангелов-хранителей, проклятия, етц.

И про чайник Рассела тоже не смогу.

Почему свобода воли ЛЛМ — чайник Рассела, а человека — нет?

А что понимают фанаты ФП под заклинанием "развитая система типов" вы не достанете из них и клещами.

Я, кажется, уже встречал треды, где вам пытались объяснить что-то на тему, но можно попробовать ещё раз.

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

Насколько я помню есть только одно альтернативное определение типа: тип определяется набором операций которые определены для этого типа (над этим типом).

Есть ещё категориальная формулировка, вроде «типы и термы в просто типизированном лямбда-исчислении — это соответственно объекты и морфизмы в декартово замкнутых категориях» или «тип-сумма — это левый сопряжённый к диагональному функтору», но это если хочется прям строгости-строгости.

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

Я не могу сказать про «любой», но если достаточно долго смотреть, скажем, на boost.spirit, то может привидеться какой-нибудь из parsec'ов, например.

Футурамы-Бендера.

Тут ключевой вопрос в другом:

Но вы правда считаете, что это всё интуитивнее, чем делать через bind?

Так это вы описали вообще естественный процесс абстрагирования:

Я хотел сказать, что когда всё иммутабельное и рекурсивное, то через некоторое время в коде появляется большое количество функций, отличающихся совсем чуть-чуть.

То же самое, когда в коде всё мутабельное и императивное. Появляются алгоритмы в std::, появляются ООП и паттерны всякие там, и так далее.

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

В плюсах нет дешёвого и неболезненного способа выразить интерфейс монады.

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

Но стоит ли автор осуждения на основании этой подстройки?

Да, по определению.

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

Я имел ввиду что в целом ряде случаев, отторжение по поверхностному анализу личности просто лишит ваш 100% полезной информации.

Всегда есть альтернативные издержки. Выбор не сводится к «потратить 18 минут на чтение статьи или слить их в бездну небытия». Вместо 18 минут на чтение статьи человек мог бы сделать что-то, что ему лично было бы куда полезнее.

Подстройка этого порога («оценка вероятности истины меньше X ⇒ не читаем») как раз максимизирует профит человека.

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

Я видел, и, если упрощать, не считаю, что анализ более поверхностный, чем оно того заслуживает.

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

А это зависит от модели мира. В модели исходного комментатора лейбл «инфоцыган» достаточен для того, чтобы говорить, что с вероятностью сильно больше нуля (и среднего по больнице) автор статьи врёт. В вашей — нет.

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

Только такие ситуации и бывают. И потом ещё итеративно уточнять репутацию авторов высказываний, чтобы оно к чему-то сошлось.

Графовые модели так и работают.

Лично мне всегда казалось, что проще всего объяснить, какой тип можно считать монадой, через join: например, можно же схлопнуть список списков в плоский список, значит монада

Парсер — это монада. Какова операционная семантика схлопывания… парсера парсеров? Парсера, возвращающего парсер? Блин, да это даже не выговоришь.

State s — это монада. Какова операционная семантика схлопывания State s (State s a)?

Вероятности — это монада. Какова операционная семантика схлопывания MonadDistribution m ⇒ m (m a)?

Есть, в конце концов, свободные монады поверх произвольных функторов, data Free f a = Pure a | Roll (f (Free f a)). Схлопнете тут?

Про Cont я и говорить не хочу, это исчадие ада.

Понятно, что это всё можно описать (и кое-что — даже весьма просто, если у вас есть достаточный опыт — скажем, я второй десяток лет развлекаюсь ФП и когда-то занимался статами, поэтому представить себе вероятностное распределение на распределениях и их маргинализацию я вполне могу). Но вы правда считаете, что это всё интуитивнее, чем делать через bind?

join, конечно, является основой, если вы начнёте заниматься теоркатом (потому что там это естественное преобразование T² ⇒ T). Но если вы всё-таки пишете код, то bind ИМХО проще.

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

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

Не понял, зачем? Если у вас всё пока что иммутабельное, то не нужно ничего никуда добавлять. Замыкания, все дела:

addEach :: Int -> [Int] -> [Int]
addEach n = go
  where
  go [] = []
  go (x:xs) = x + n : go xs

Через какое-то время вас достанет писать однообразные рекурсивные перекладывания из списка в список, и вы придумаете fmap.

fmap работает на произвольных функторах, а вот конкретно на списках map был ещё в лиспе в бородатых 60-х, когда хаскеля и в проекте не было (и лисп не то чтобы славится иммутабельностью).

Интересно, зачем в C++ придумали std::transform или std::for_each? Наверное, тоже иммутабельность виновата?

Аналогично с монадами: очень утомляет делать цепочки действий и на каждом шаге выполнять одни и те же вспомогательные операции, научились их прятать.

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

И почему в те же плюсы добавили монадические операции для std::optional и std::expected? Хаскелисты покусали плюсистов?

Кантри какое-то. Впрочем, это же мне по статусу положено слушать кантри!

У меня форточка принципиально не открывается.

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

Максимизация «ожидаемого удовольствия» (свёртка вашей текущей оценки вашей личной функции полезности состояния в момент времени t с вероятностью этого состояния, по всем состояниям и времени жизни).

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

и каким инструментарием оптимизации обладаем?

В парадигме наличия свободы воли — возможностью выбирать действия. Получить образование/профессию. Заняться физкультурой. Есть нормальную еду. Работать над своим интересом для других людей.

Но свободы воли нет. Но лучше думать, что она есть.

Изнутри личности, если ты сидишь в "комфортной зоне комфорта" (то есть тебе привычен комфорт, который ты уже имеешь), то зачем тебе еще морковка сзади? Все правильно делаешь, и никому не обязан тройные сальто учиться делать.

Потому что жизнь не статичная.

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

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

И если в первом случае морковка может быть спереди, то во втором… ну, по крайней мере, для себя я морковку спереди разместить так и не осилил. Ну не могу я полюбить тренажерку, хоть годами туда ходи — всё равно такая же тупая локально трата времени и ресурсов.

Есть теория, что у древних греков времён «Илиады» не было самосознания (я не подразумеваю критического отношения к этому утверждению, так как ещё не прочитала книгу).

О, не знал, что про неё на хабре было.

Я её как раз почти дочитал. Скажем так, интерпретация сознания героев (и рассказчиков) «Илиады» у Джейнса консистентна что с интерпретациями «Илиады» других философов, с которыми я встречался, что с его интерпретациями других первичных источников (разные эпосы и мифы прочих народов в разные периоды), что с тем, что я отрывочно знаю об этом хз откуда.

У Джейнса есть ИМХО ряд других слабых мест (например, ИМХО он внутренне противоречив по таймлайну замены бикамеральности на сознание: одни части подразумевают резкую смену, масштаба пары поколений, другие — масштаба 5-10 веков), но как концепт он, конечно, интересен.

Другое дело, что Джейнс — это 70-ые, и с тех пор нейронаука шагнула несколько вперёд, поэтому актуальнее, скажем, Метцингер с «Being no one», но его читать — хардкор.

Аргумент сказанный, пусть даже МиккиМаусом, все еще аргумент.

Аргумент — это логическое высказывание в духе «A ⇒ B» (вернее, дерево его вывода, но это не столь важно). Почти аргументом будет также просто B (скажем, B ≔ «вам стоит чистить зубы два раза в день»), если A является достаточно общепринятым для того, чтобы подразумеваться (скажем, A ≔ «если вы не фанат зубной боли и искусственных зубов ∧ чистка зубов уменьшает риск проблем с ними»). Для аргументов действительно неважно, говорит ли их Микки Маус, или же этим мальчиком был Альберт Эйнштейн.

Проблема в том, что в статье очень мало аргументов и очень много постулатов о том, как работает наш конкретный мир. Это уже не строгие логические построения, а утверждения, которые могут быть истинны или ложны с какой-то вероятностью. И для оценки вероятности истинности этих утверждений необходимо учитывать априорные данные о говорящем (его род занятий, надёжность в других высказываниях, и так далее). Ну, тупо по Байесу, как условная вероятность по тому, что говорящий врёт.

Или, короче, фраза «американцы никогда не были на Луне» на сайте secreti-zapada.narod.ru и из уст Джеймса Вебба будет иметь несколько разный вес, и это вполне естественно.

1
23 ...

Информация

В рейтинге
1 840-й
Зарегистрирован
Активность