Comments 39
Чертовски нудное вступление, теряющее смысл там, где программирование приходит к операциями над указателями (pointer, **).
За ссылку в стиле "Lisp жив" спасибо,- но я как-то и не сомневался, что lisp в той или иной степени до сих пор работопригоден.
PS Защита сегментов в ОП компьютера (сегмент данных, сегмент кода,...) чем-то сродни динамической типизации (в плане того, что есть дескриптор: "тут мы играем, а тут пятно - мы рыбу заворачивали" )... Но это скорее - в область шуток и баек ;)
В то время как инженеры-строители иногда говорят о разных типах цемента, программисты, похоже, используют слово ежедневно.
Один только ГОСТ 31108-2003 описывает больше марок цемента, чем типов данных во всем С ;)
В физике размерность используется повсюду. Нельзя складывать метры с килограммами, хоть обе величины выражаются числами.
А потом приходят настоящие физики™ и первым делом всё обезразмеривают. Именно чтобы спокойно складывать метры с килограммами.
А потом приходят математики и ещё раз обезразмеривают. Уже из-за особенностей вычислений с плавающей точкой.
Потом приходит ученик начальной школы и вычисляет 1.5 землекопа.
У Маши было 2 пачки (п) по 3 карандаша (к) в каждой. Сколько всего карандашей?
В начальной школе умножение выводят через сложение и учат умножать карандаши на пачки, чтобы получить карандаши. 3к + 3к = 3к * 2 = 6к. А делать наоборот - 2п + 2п + 2п = 2п * 3 - это не логично. Но потом детям рассказывают про коммутативность умножения.
а почему "3к + 3к = 3к * 2" а не "3к + 3к = 2 * 3к" ?
"две кучки по 3 карандаша" - оно же и в речи так же.
У вас ошибка размерности.
Не 3 к, а 3 к/п. Три карандаша в пачке, а не какие-то абстрактные три карандаша. По аналогии с тремя километрами в час.
Соответственно, (3 к/п) * 2 п = 6 к. Никакой мистики. И с коммутативностью умножения всё прекрасно.
1.5 курицы за 1.5 дня сносят 1.5 яйца. Сколько снесут 2 курицы за 3 дня?
Ну вот такие единицы, чтобы не таскать скучные коэффициенты, это и есть обезразмеривание. Массы мы измеряем в единицах m0, заряды в q0 и т.д.
Формула существования горизонта событий чёрной дыры в форме Q² + J² < M² намного понятнее той же формулы, но в любых "нормальных" единицах измерения, пусть даже для которых c = G = 1. Хотя здесь к квадрату заряда добавляют квадрат момента импульса и сравнивают с квадратом массы, зато она очевидна чисто геометрически.
В случае с размерными величинами, лучше считать типом не каждую размерность саму по себе, а вводить один тип - "размерная величина". Состоящий из поля значения величины и вектора степеней основных единиц измерения (их в каждой системе фиксированное небольшое количество).
Такой тип без ограничений поддерживает умножение, в том числе возведение в степень числа. Складывается только при условии равенства векторов метрики, в качестве аргумента какой-то функции, не сводящейся к вышеперечисленному, может выступать только при нулевом оном векторе (все степени - ноль; размерность - единица).
Тут, ведь, в чём проблема концептуальная? Для вычислений нам нужны циклы, то есть, рекурсия, то есть, комбинатор неподвижной точки, а его выразить в терминах теории типов нельзя. Его можно встроить в язык как специальную конструкцию, или же отдельно формировать для каждого индуктивного типа "магическим" образом. Но это означает, что статически типизированные языки менее выразительны. То, что в них можно написать тип всех возможных значений и программировать потом с ним, обеспечено тем, что fix-комбинатор уже встроен в язык.
При этом, можно взять бестиповый язык, в котором fix выражается, и завернуть его в конверт Каруби, и получить типы. Собственно, поверх процессора, который различий между битами не видит, статические системы типов так и строятся.
Но всё ещё запутанее Потому что для денотационной интерпретации бестиповых вычислений, ну, то есть, для определения математических функций по коду программ, приходится сначала строить типизированное исчисление и искать в нём предельный рефлексивный объект.
Логики активно спорили о том, что первично, и о том, что вообще это всё значит, где-то до конца 90-ых, но так ни к чему и не пришли. Статическая типизация очевиднее с логической точки зрения, поэтому, видимо, стала более популярным направлением. Но небольшие группы пытаются до сих пор развивать теории, свободные от типов. Результаты у них так себе, но история с самоприменимостью требует какого-то более пристального внимания, а не просто отказа от неё через синтаксические ограничения...
Комбинатор неподвижной точки прекрасно выражается в терминах теории типов: (a -> a) -> (a -> a), если я ничего не напутал.
Почему не означает? Мы не можем в языке выразить fix, нужна специальная константа, семантика которой задаётся внешним образом: внутри языка мы просто верим, что fix - это fix, а технически это бестиповый fix - специальная конфигурация битов в памяти.
Но Тьюринг полнота, конечно, так обеспечивается.
Общая рекурсия нужна для описания процессов (pi-исчисление), одними функциями не обойтись на практике.
Но все же примитивную рекурсию (которая делает n шагов) можно выразить, как минимум, в System F и более богатых системах типов.
Предполагаю что часть типов (к примеру, i32 в Rust) отображена на способ хранения значений намеренно, чтоб наиболее эффективно работать с аппаратурой, на которой будет выполняться финальный код. В то же время, более сложные типы - всякие перечисления, пересечения и объединения - прямой связи с представлением в памяти вроде как не имеют. (Возможно, что такая связь была в языке Си, из-за недостаточно сильной системы типов, но я не знаю Си, могу ошибаться.)
Возможно, вы имели в виду другое - что, к примеру, температура по Цельсию и Файренгейту - это тот же набор значений и те же операции, но сами типы разные. Тут да, согласен, но тогда и определение типа должно звучать как-то так:
Тип — подразумеваемая суть того, что описывается типом, множество допустимых значений и набор операций, которые можно применять на данных значениях.
Но тут уже какая-то рекуррентность и звучит все слишком абстрактно...
https://en.m.wikipedia.org/wiki/Data_type пишет, что значение этого термина зависит от контекста.
Забавная статья. Никогда не видел споров по поводу типизации. Очень много очевидного в статье и она ориентирована не на программистов, а на кодеров. Программисты обычно мыслят шире, 'out-of-box' и такими очевидным вещами не заморачиваются. Для хорошего программиста нет особой разницы на чем писать: C++, C, C#, VB, F#, Cobol, Lisp... Главное - алгоритмика, а во что завернуть по большому счету не важно. А синтаксис, типы, ошибки компиляции - учите матчасть.
Я больше или меньше программировал на разных языках: бейсик, паскаль, асм, ява, перл, С и т.д. Всего - десятка полтора. Примерно в 2002 году я "подсел" на PHP и проблем с типизацией данных за эти годы больше не встречал.
Теория типов - относительно новое напрвление в CS. С весьма интересными штуками, как-то алгебраические типы данных, зависимые типы или полнота системы типов по Тьюрингу. Теория типов стоит внимания; мощная система типов позволяет устранить ряд ошибок на корню (к примеру, null pointer exception), частично заменяет тесты и документацию. Есть отдельная книжка по данной теме - Бенджамин Пирс, "Типы в языках программирования".
Что касается PHP, Python или JavaScript (то есть динамических языков, без тайп-хинтинга), то в них с точки зрения системы типов всего один тип, который есть объединение (множество) всех возможных значений, которые можно поместить в переменную языка. Так что проблем с типизацией там изначально нет.
Почему типы так много значат для программистов?