Во. С этого надо было начать. Я с самого начала подозревал некорректное использование редукционизма, но никак не мог вас из этого вытянуть в явном виде. А спорить со своими спорными интерпретациями у меня нет никакого желания: есть немалый печальный опыт подобных споров, и сегодня я тщательно избегаю его повторения.[disclaimer #1. Я накатал стену текста, за что простите, но у меня выдалось тут несколько свободных часов, и я решил предаться своей любимой графомании. За это я приношу извинения, но, написав, я подумал стоит ли постить, и решил, что я ведь никого не обязываю читать всё это. Я свой кайф от написания уже получил. А если вам не доставляет кайфа это читать, то мне, как заядлому графоману, это в общем-то уже и не очень важно. С другой стороны, может вы таки прочитаете, и это окажется полезным.]
[disclaimer #2. Стену я накатал, потом подумал, и решил дополнить неким пояснением, которое может быть будет полезным. Нам недоступна реальность для непосредственного восприятия. Из-за этого, в большинстве случаев мы можем безопасно считать, что никакой реальности нет, и всё что вокруг нас -- это выдумки, иллюзии. В некотором смысле так и есть: ведь если я вижу кружку с чаем, то реально это переживание кружки с чаем возникает потому, что моя психика построила образ кружки с чаем, то есть образ, "программный объект" соответствующий чему-то там в реальности. И я не знаю чему: в лучшем случае я могу описать те ощущения, которые кружка с чаем создаёт на сетчатке, но какова природа этой кружки я не знаю. Я не знаю как она выглядит. Вообще бессмысленно говорить как кружка чая выглядит в реальности, потому что реальный объект выглядеть как-то может исключительно в психике, но не в реальности. Поэтому, даже когда я там в контексте слов о теории категорий, говорю об объектах, то это не объекты реального мира. Их лучше представлять как некие программные объекты, которыми оперирует программа "психика" выполняемая на биологическом компьютере мозге.
Я решил написать об этом, потому что заметил некую предвзятость в отношении архитектуры процессора, то есть заметил идею о том, что архитектура процессора -- это некая догма, это реальность, а всё остальное -- это не реальность, но выдумки всякие. Архитектура процессора -- это такие же выдумки, как и всё остальное. Это тоже абстракции, которые созданы для того, чтобы проще было управлять схемами построенными на логических вентилях. Если условность этой абстракции непонятна, попробуйте спаять процессор на рассыпухе, или хотя бы выясните как это делается -- в интернете есть туева хуча информации, руководства, готовая схематика, даже промышленным образом собранные девайсы можно купить в виде плата полметра на полметра.]
Ваш тезис в том, что раз в системе команд процессора нет понятия тип, значит понятия тип нет вообще. Или может быть, что если мы не можем объяснить высокоуровневое понятие "тип" через логические вентили, на которых построен процессор, значит это бессмысленное понятие. (Ну, да, я очень вольно формулирую, и даже вероятно извращаю ваши слова, каюсь, но простите, сложно удержаться. Да и это не очень важно, я покажу это дальше.) Такого рода аргументы в общем случае строятся посредством редукционного перехода, то есть мы берём какой-то вопрос, какую-то проблему, которая сформулирована в рамках одной области знаний -- например программирования на высокоуровневых языках, -- а затем пытаемся переформулировать эту проблему в рамках более низкоуровневой области знаний, например, в системе команд процессора, или в логических вентилях или ещё в чём-то -- в принципе тут можно спускаться хоть до квантовой механики.
Проблема с такими редукционными переходами, что они могут терять исходную проблему. Если они сохраняют проблему, и спустившись на более низкий уровень мы сохраняем способность видеть исходную проблему, пускай даже она сформулирована в других терминах, то редукционный переход в таком случае -- это очень полезная вещь, которая может помочь выявить высокоуровневые закономерности. Если же сам факт выполнения редукционного перехода привёл к исчезновению проблемы, то это знак того, что редукционный переход некорректен. Как минимум в том смысле некорректен, что он не решает никаких проблем вообще.
Я могу привести пример не из программирования, но очень занятный. Особенно с точки зрения тролля. Если вы поймёте, что я пытаюсь донести, и если вам удастся понять как думают хомячки и в чём их ошибка, то вы сможете до бесконечности вгонять их в когнитивный диссонанс, задавая "каверзные" вопросы. Тема: свобода воли. Общество давным давно ставит проблему свободы воли, задаваясь вопросом что это, и что с ней делать. Почему этот вопрос так волнует людей? Например, потому что наше понимание справедливости подразумевает, что если человек "по доброй воле" сделал гадость, то его надо наказать, а если он сделал это под давлением обстоятельств, если у него не было выбора, то у него есть оправдания, которые как минимум должны снижать размеры наказания. Если человек совершил хороший поступок, то тут то же самое: если он сделал это проявив свободу воли, то это котируется выше, чем если он сделал это случайно, или потому что у него не было выбора. Тут можно копать дальше, выясняя зачем обществу нужно именно такое понимание справедливости, как на всё это влияет свобода воли. Можно задаться целью проектирования идеального общества, а потом искать ответы на вопросы типа "как влияет на структуру общества то или иное понимание свободы воли обществом", или "если поведение X считается проявлением свободы воли, то как должна отличаться реакция общества на это поведение, по сравнению с ситуацией, когда поведение X не считается проявлением свободы воли". Можно придумать и другие задачи или вопросы связанные со свободой воли.
Так вот, очень часто люди начинают спор о существовании свободы воли с редукции в биологию, в физиологию, в химию, в квантовую механику или ещё куда-то. Причём те, кто хотят доказать, что свобода воли есть, любят редуцировать в квантовую механику, а потом рассуждать о том, что квантовая неопределённость и есть свобода воли. Но это серьёзная ошибка методологического уровня. В школе учат рассуждать на примере математики, в математике таких ошибок не существует, поэтому как правило люди даже не замечают ошибки в этих рассуждениях и могут спорить до скончания века. Ошибка в том, что как только мы заявили, что человек -- это сложная химическая реакция в кожаном мешке, так сразу мы "потеряли" свободу воли, потому что в химии нет никакой свободы воли по построению этой химии. Нет свободы воли -- нет проблемы свободы воли, так? "Если мы не видим суслика, значит его нет." Но те исходные социальные вопросы, с которых я начал, остались нерешёнными. То есть исходная проблема осталась проблемой. Умные люди пытались придумать какой-то фреймворк для решения этих проблем, в рамках создания этого фреймворка они запилили понятие свободы воли (впрочем "запилили" -- громко сказано, скорее они сделали кривую демо-версию). Им удалось решить какие-то вопросы и системно описать через это новое понятие какие-то социальные процессы и показать как их фреймворк предлагает решать те или иные социальные проблемы. Какие-то цели остались ещё недостигнутыми, поэтому эти умные люди продолжают дискутировать о том, как лучше пилить дальше понятие свободы воли. И тут приходит редукционист, говорит, что а) человек -- это химическая реакция в кожаном мешке, б) в химии нет никакой свободы воли, из (а) и (б) с очевидностью следует, что у человека нет никакой свободы воли. чтд, а вы все не умные люди, а только щёки с умным видом надуваете, а на самом деле идиоты. Тут умные люди делают facepalm.jpg и молча ретируются. (Вы не подумайте, я не причисляю себя к _этим_ умным людям, о чём свидетельствует хотя бы вот эта стена текста, которую я накатал, вместо ретирады.)
С программными типами то же самое. Если мы возьмём rust и зададимся вопросом зачем разработчики rust создавали ту систему типов, которая есть в rust'е, то мы увидим очевидный ответ: чтобы дать возможность программисту описать как можно больше ограничений на то, что можно делать с теми или иными кусками данных. Дать возможность программисту описать как можно больше правил работы с данными, правил которые затем компилятор сможет проверить. Идеальная система типов с их точки зрения -- эта такая система типов, которая позволяет создавать для любой программы такой набор типов, который будет позволять делать с данными только те вещи, которые осмысленны в рамках задач, решаемых программой. Вот они цели.
Теперь, если мы выполняем редукцию в низлежащую архитектуру процессора, в систему команд этого процессора, то мы начинаем мыслить о программе в иных абстракциях, на которые абстракции раста невозможно отобразить изоморфно. И поэтому многие утверждения о типах из rust'а после отображения на категории программирования в машинных командах, становятся бессмысленными, или двусмысленными/неоднозначными, или ещё каким-нибудь образом начинают вызывать сомнение в их истинности. Но -- вы знакомы с теорией категорий? -- тут надо помнить, что есть разница между утверждением и образом утверждения, полученным в результате применения к исходному утверждению некоего отображения (в нашем случае редукции). На эту разницу можно положить болт, если наше отображение изоморфно, то есть если одна категория (то есть множество объектов и множество всех связей между ними) отображаются взаимно-однозначно на другую категорию. (Множество матриц размера NxN изоморфно множеству однородных систем линейных уравнений с N переменными, поэтому я могу легко рассуждать о матрицах, и переносить выводы на ОСЛУ, и даже в речи взаимозаменяемо употреблять слова "ОСЛУ" и "матрица NxN" -- это не приводит к противоречиям, и даже математики-и-педанты-на-всю-голову снисходительно на это смотрят).
Но если отображение не изоморфно, и если несколько разных объектов (понятий, абстракций) rust'а отображаются в один объект в ассемблере, то тут заранее вообще ничего нельзя сказать о том, что случится с истинностью утверждений, после отображения. Ну, если у нас есть объекты x,y,z, есть утверждение p(x,y,z), и есть отображение f, то зная истинность p(x,y,z) мы ничего не можем сказать об истинности p(f(x),f(y),f(z)) в общем случае.
Я могу привести ещё один пример не из программирования. Пример, где редукция, как отображение между двумя способами представлять реальность, построена, работает и позволяет переносить проблемы из одного представления в другое. Термодинамика газов в том виде, в котором её рассказывали в школе. Там явно произносились слова "макропараметры", под которыми подразумевались такие вещи, как температура, давление и объём газа. Фишка в том, что газ состоит из молекул, и у молекул нет температуры и нет давления. У них есть объём, но он слабо связан с объёмом газа, по-крайней мере сумма объёмов молекул не сойдёт даже за оценочное значение объёма газа, там разница будет во много порядков. Это не вызывает когнитивного диссонанса? Как так: на микроуровне нет макропараметров, а на макроуровне они возникают? Если мы на макроуровне сформулируем какую-нибудь задачу, например, "как зависит давление от температуры?", а потом попробуем выполнить редукционный переход, то мы потеряем задачу. Физики и математики проделали кучу работы, и они построили математическую модель, позволяющую "редуцировать" давление и температуру до микропараметров, и пользуясь их формулами и определениями, мы в общем-то можем переформулировать задачу, заданную в терминах макропараметров, в термины микропараметров. Собственно законы термодинамики, устанавливающие связь между температурой давлением и объёмом, а так же накладывающие ограничения на динамику ещё одного макропараметра -- энтропию -- были доказаны именно через эту редукцию, хотя они и были исходно получены чисто эмпирически. Термодинамика мне нравится как пример тем, что здесь редукция макропараметров возможна, она реально построена и осмысленна.
> Обратите внимание на второй абзац, "изучения систем <ЖИРНО>типов данных</ЖИРНО> в теории
> языков программирования", то есть значения элементов множеств, а сам тип есть
> некие допустимые рамки этих значений, и в информатике этими рамками служит
> размер хранимого значения, ...
Возьмём те же строки. Допустим, что мне хочется в программе работать со строками в разных кодировках, поэтому я к каждой строке буду привязывать информацию о её кодировке. Инкапсулируем всё это как следует под API, и получим в результате, что две строки "привет мир" могут иметь один и тот же тип, и даже быть равными. Тут правильнее наверное употреблять слово "эквивалентными", хотя это зависит от контекста: иногда нам важно различать эквивалентность и равность, иногда нет. В том же lisp'е мы видим, несколько предикатов сравнения на равенство: eq который сравнивая два объекта проверяет два ли это объекта, или один и тот же, и equal, который сравнивая объекты сравнивает их на "равенство". eq на вышеприведённых строчках "привет мир" выдаст nil, т.е. false, потому что это два разных объекта, equal выдаст t, то есть true, потому что строчки состояет из одной и той же последовательности символов (не кодов символов, а именно символов). Но, обратите внимание, ни eq, ни equal даже не посмотрят на совпадение или несовпадение размеров. И мне как программисту пишущему прикладной код, совершенно не важно совпадают ли размеры или нет.
Типы позволяют описывать разные абстракции, и то, какие именно нужно описать, то, какие удобны для написания конкретной программы -- это вопрос, который оставляют программисту, который разрабатывает эту программу. Ну или хотя бы пытаются оставить ему эти вопросы. Иногда его наоборот ограничивают в выборе, и в этом тоже бывает свой смысл.
Если мне каким-то образом удобно делить строки на типы, то это удобство полностью оправдывает моё деление и не требует дальнейших обоснований. Обоснования могут потребоваться только в том случае, если мой коллега усомнится в том, что это удобно и предложит другой способ. Вот только тогда потребуются аргументы.
> Этот абзац меня расмешил, а вы говорите читайте википедию :) (Основная роль
> системы типов заключается в уменьшении числа багов в программах) эт жесть.
А что не нравится? Это именно так. Вы можете почитать комменты на опеннете, как тут люди отзываются о всяких нестрогих системах типов, с автоматическими приведениями типов. Основной посыл: отсутствие строгости у системы типов приводит к появлению множества трудноотлавливаемых багов. И это действительно так: когда я нечаянно могу выполнить приведение строки к числу, это даёт мне простор для того, чтобы строку полученную из внешнего источника сравнить с числом и получить какой-нибудь бред. Причём это может происходить даже не потому, что я не подумал об этом, а потому что я недостаточно хорошо знаю правила приведения типов.
> """
> Если инструкции в теле функции написаны в предположении, что им на обработку
> должно быть передано целое значение, но вызывающий код передал число с
> плавающей точкой, то вызванная функция вычислит неверный результат.
> """
> Вот и всё, когда дело доходит до исполнения, понятие "типа" данных ЯП
> исчезает, включается понятие "типа" как размера, ибо инструкция выполняющая допустим сложение
> двух флоатов требует соответствующего размера регистров, и отсюда вся хренотень с
> db dw dd dq - и собственно для каждого размера свои
> инструкции.
Вы упускаете из виду один нюанс. Если мы говорим о том, что программа написана на высокоуровневом ЯП со строгой типизацией, то на этапе выполнения программы невозможна ситуация, когда в код, работающий с целочисленными значениями переданы флоаты. Это одна из ловушек редукционизма: очень легко потерять инварианты, которые выполняются на высоком уровне. То есть, сами инварианты никуда не деваются из программы, но мы, выполнив редукционный переход, перестаём их видеть. "Видишь суслика? Нет? А он есть."
> Далее по тексту:
> """
> Изучением систем типов занимается теория типов, хотя на практике конкретная система типов
> языка программирования основывается на особенностях архитектуры компьютера, реализации
> компилятора и общем образе языка.
> """
> 3 / "Hello, World" - как это выражение можно написать на ассемблере?
> (3 - 4 байта, "Hello, World" - 12 байтов (без терминирующего
> нуля допустим))
Это зависит от языка программирования. Если мы говорим о C, то тогда на ассемблере это будет выглядеть как строка "Hello, World" в секции .data, и деление 64-х битного значения 3 на адрес этой самой строки. По-крайней мере, компиляторы прошлого тысячелетия тщательно делали вид, что всё происходит именно так. Компиляторы нового тысячелетия могут выкинуть любой фортель в ответ на подобный код, ибо это UB.
Если же мы говорим о javascript, то... эмм... я плохо знаю javascript: он будет как-то приводить строку к целочисленному типу, и я не уверен, что он получит в данном случае. Можно проконсультироваться с документацией, там должно быть описано.
Строка 3/"Hello, World" не имеет какого-то своего собственного значения. Она может иметь значения в рамках той или иной грамматики, значение полностью определяется языком. Ваше представление о типах, как мне кажется, полностью определяется каким-то диалектом ассемблера. И при работе с тем диалектом оно абсолютно корректно. Но меня нисколько не удивит, если при переходе к другому диалекту ассемблера для того же процессора оно окажется некорректным. И уж совершенно нечему удивляться, если оно не будет работать в js.
>>>Зачем программисты используют типы? Чего они достигают?
> Так лучше вообще без них, почему так высока популярность всяких динамически слабо
> типизируемых ЯП ? Что говорят "статисты"? их программы безопасней раз строго
> типизирован ЯП ? Типобезопасность - как критерий чего?
Ну, во-первых, следует развести понятия "динамическая типизация" и "нестрогая типизация". Типизация может быть строгой и в то же время динамической. Типизация может быть нестрогой, но при этом статической. Динамическая типизация отличается от статической тем, что при статической дополнительно к понятию "тип значения" вводится понятие "тип переменной", что позволяет проверять типы не только в рантайме, но и при компиляции. Подчастую при статической типизации компилятор, генерируя машинный код, вырезает информацию о типах, потому что предполагается, что все необходимые проверки типов уже выполнены, и не требуется дополнительных проверок в рантайме, а значит и информация о типах бесполезна на этапе выполнения программы.
Динамическая (но строгая) типизация, по сравнению со статической, допускает кучу багов в программе, но эти баги отчасти контролируемы, потому что эти баги будут приводить к рантайм ошибкам, которые детектируется системой типов, и затем обрабатываются. Даже если обработка сводится к тому, что программа "контролируемо" падает, это лучше, чем если она, перепутав float и int, продолжает работать как будто так и надо. В первом варианте поведения нет ничего хорошего, но второй позволяет не только DoS атаки, но ещё и произвольное выполнение кода. То есть, с этой точки зрения, динамическая типизация лучше, чем отсутствие типизации, но хуже чем статическая. Но у динамической типизации есть свои плюсы: она может сильно упрощать структуру программы. Например, если мне надо много типов строк, то мне не обязательно думать о том, следует ли все эти типы объединить в единую иерархию типов. Я просто использую много типов строк, ищу те ситуации где возникают рантайм ошибки, и в тех ситуациях делаю typecase (с смысле case по типу аргумента). Это может приводить к большим проблемам в будущем с поддержкой программы, это может приводить к тому, что в каких-то экзотических случаях программа будет падать с ошибкой, потому что в typecase не все возможные варианты перечислены, но зато если я не уделил внимания этапу проектирования программы, то я могу реализовать больше функциональности в программе, прежде чем я упрусь в невозможность продолжать писать код и в необходимость вернуться назад и начать проектировать программу с нуля, переписывать или рефакторить код. Такие фишки полезны, например, когда пишешь то, не знаю что. Когда важен не результат написания программы, а сам процесс её написания, который является исследовательским процессом, нацеленным на изучение предметной области.
Нестрогая же типизация -- это, на мой взгляд, результат человеческих лени и глупости. Я тут поработал с rust'ом, где мне приходится явно указывать все нужные мне преобразования между целочисленными типами, и я понял, что хоть это и добавляет возни, но помогает не совершать некоторых глупостей и заставляет более продуманно выбирать конкретные целочисленные типы для тех или иных переменных, аргументов функций, членов структур и тп. Вырабатываются определённые стратегии выбора типов, нацеленные на снижение последующих конфликтов и явных приведений, и эти стратегии положительным образом сказываются на коде.
Но, если я ещё могу худо-бедно согласиться с подходом C, который автоматом преобразует char к int, а double к float, то всякие глупости типа автоматические приведения строки к числу или числа к строке -- это вообще выходит за границы здравого смысла. Но, если пытаться найти объяснение отличное от глупости, то я бы предположил, что идея нестрогой типизации в языке нацелена на то, чтобы найти компромисс между отловом максимума ошибок и простотой написания кода/изучения языка. Понятно, что всё это происходит на фоне какого-то представления о том, какие именно задачи будут решаться на этом языке, какой код будет писаться. И как показывает практика, эти априорные представления очень часто оказываются ошибочными, поэтому компромисс совершенно не попадает в оптимум.
>>>Даже с точки зрения размера это разные типы.
> разные типы для кого? для человека может разные символьные и целочисленный, для
> компилятора С почти по барабану (или целое число в диапазоне 0-255,
> -127-+127), для архитектуре и подавно главное размер регистра.
Это сильно зависит от языка. А абстракции языка зависят от тех задач, и тех методов решения задач, на которые заточен язык. Язык C не различает символьный тип и int8_t, а в паскале -- это принципиально разные типы, и отображение между ними выполняется явным вызовом функций. Потому что Вирт посчитал, что негоже использовать арифметические функции для работы с символами. Что все применения арифметики к ASCII кодам должны быть инкапсулированы в хорошо оттестированной библиотеки, которая предоставляет программисту "safe API". И в этом ведь есть определённый смысл: это позволяет изменить внутреннюю кодировку строк, не запуская процесс аудита всего кода, чтобы убедиться, что вся работа с символами и строками осталась корректной после изменений представления строк.
>>>То есть даже с точки зрения размера -- это разные типы.
> я вот об этом же - кроме как "тип" как размер регистра(ячеек
> памяти) для архитектуры другого нет. Зачем всё усложнять?
Чтобы автоматизировать труд программиста. Чтобы программисту надо было бы тратить меньше времени на поиск багов вида "аргументы для функции сложены на стек не в том порядке". Ну, это например. На самом деле, количество разнообразных граблей, от которых уберегает система типов, очень большое.
> Я был бы
> рад если бы архитектура строго выделяла бы все описанные выше "типы",
> но она этого не делает, и нужность (необходимость) этих "типов" -
> увы не доказана даже в теории.
Ну, во-первых, это не совсем вопрос теории. Это во многом чисто практический вопрос, программисты создают инструменты, которые им удобны. Если мы посмотрим на теорию, то не найдём у неё никаких желаний, в теории нет таких понятий "нужно" или "хочется". Нужность чего-либо начинается с хотелок человека, и обосновывается ими же. И вот тут возникает "во-вторых": хотелки человека, как правило, не в том, что он хочет явно указывать где надо привести u8 к u64, хотелки человека заключаются в чём-то другом. И связь между хотелками человека и необходимостью вычистить язык от явных преобразований типов может устанавливаться, в частности, и формальными доказательствами. Местами это возможно, и местами это делается. Но чтобы найти такие теоретические доказательства, надо взять конкретную фишку языка, подумать о том зачем разработчик её привнёс в язык (не "зачем это надо мне", а именно "зачем это было надо разработчику языка" -- некоторые не умеют различать эти два вопроса, а зря), и вот потом, двигаясь от целей разработчика искать обоснования, и там иногда можно встретить и формальные доказательства.
ЯП -- это инструмент. Такой же как и лопата. Если нам придёт в голову построить теорию лопаты, то мы будем двигаться от тех целей, для которых лопата предназначена. Вряд ли мы будем исследовать, какие свойства лопаты помогают или мешают использовать её для выкручивания винтов с крестовым шлицом из механизма наручных часов. ЯП -- это инструмент, в отношении которого есть какие-то ожидания о том, для каких задач он подходит, а для каких нет. И двигаясь от этих ожиданий можно обосновать те или иные решения принятые разработчиками ЯП. Или обратно: разглядывая решения, принятые разработчиками, можно предположить их ожидания и цели.
> Главный вопрос - зачем ввели эту теорию типов - остаётся открытым.
Я ни на что не претендую, но надеюсь, что здесь мне удалось накидать достаточное количество ниточек, за которые можно потянуть, и в конечном итоге распутать клубок этого открытого вопроса. Я надеюсь, что мне удалось донести мысль о том, что если смотреть на высокоуровневый ЯП с точки зрения ассемблера и любые утверждения об этом языке переводить в термины ассемблера, то можно быть практически уверенным в том, что этот высокоуровный ЯП и все утверждения о нём станут бессмысленными, глупыми и вообще нехорошими. И что такой результат -- это не потому, что утверждения действительно такие, и не потому, что все разработчики высокоуровневых языков идиоты (а среди них есть очень даже умные люди, с огромным опытом программирования), а следствие того, что мы при редукции теряем смысл утверждений, а потом воюем с соломенным чучелом. Ну и блистательно побеждаем.
Вариант для распечатки
(ok) on 15-Окт-17, 14:55 
